• English only

# Differences

This shows you the differences between two versions of the page.

 sav08:proof_rule_for_equality [2009/05/20 12:07]piskac sav08:proof_rule_for_equality [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2012/05/08 14:59 vkuncak 2009/05/20 12:07 piskac 2008/04/02 22:53 vkuncak 2008/04/02 20:11 vkuncak 2008/04/02 20:10 vkuncak 2008/04/02 19:22 vkuncak 2008/04/02 19:20 vkuncak 2008/04/02 19:08 vkuncak 2008/04/02 19:05 vkuncak 2008/04/02 11:02 vkuncak 2008/04/02 01:16 vkuncak 2008/04/02 01:15 vkuncak 2008/04/02 01:15 vkuncak 2008/04/02 01:15 vkuncak 2008/04/02 01:14 vkuncak 2008/04/02 01:13 vkuncak created Next revision Previous revision 2012/05/08 14:59 vkuncak 2009/05/20 12:07 piskac 2008/04/02 22:53 vkuncak 2008/04/02 20:11 vkuncak 2008/04/02 20:10 vkuncak 2008/04/02 19:22 vkuncak 2008/04/02 19:20 vkuncak 2008/04/02 19:08 vkuncak 2008/04/02 19:05 vkuncak 2008/04/02 11:02 vkuncak 2008/04/02 01:16 vkuncak 2008/04/02 01:15 vkuncak 2008/04/02 01:15 vkuncak 2008/04/02 01:15 vkuncak 2008/04/02 01:14 vkuncak 2008/04/02 01:13 vkuncak created Line 3: Line 3: === Paramodulation === === Paramodulation === - $+ \begin{equation*} \frac{D \cup \{ s = t \}\ \ \ \ C[s'] } \frac{D \cup \{ s = t \}\ \ \ \ C[s'] } ​{subst(\sigma)(D \cup C[t])} ​{subst(\sigma)(D \cup C[t])} -$ + \end{equation*} where $\sigma$ is [[Unification|mgu]] of $\{s,​s'​\}$. where $\sigma$ is [[Unification|mgu]] of $\{s,​s'​\}$. Line 13: Line 13: === Equality Resolution === === Equality Resolution === - $+ \begin{equation*} \frac{C \cup \{ s \neq s' \}} \frac{C \cup \{ s \neq s' \}} ​{subst(\sigma)(C)} ​{subst(\sigma)(C)} -$ + \end{equation*} where $\sigma$ is [[Unification|mgu]] of $\{s,​s'​\}$. where $\sigma$ is [[Unification|mgu]] of $\{s,​s'​\}$. + **Superposition:​** a closely related technique to paramodulation,​ also meant for dealing with equality. === Completeness of Rules === === Completeness of Rules ===