• 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)
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 ===