Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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 === 
 
sav08/proof_rule_for_equality.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice