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] |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Proof Rules for Equality ====== | ||
| - | |||
| - | === Paramodulation === | ||
| - | |||
| - | \[ | ||
| - | \frac{D \cup \{ s = t \}\ \ \ \ C[s'] } | ||
| - | {subst(\sigma)(D \cup C[t])} | ||
| - | \] | ||
| - | where $\sigma$ is [[Unification|mgu]] of $\{s,s'\}$. | ||
| - | |||
| - | Here $C[s']$ means that $s'$ occurs somewhere in $C$; then $C[t]$ results from replacing that occurrence of $s'$ with $t$. | ||
| - | |||
| - | === Equality Resolution === | ||
| - | |||
| - | \[ | ||
| - | \frac{C \cup \{ s \neq s' \}} | ||
| - | {subst(\sigma)(C)} | ||
| - | \] | ||
| - | where $\sigma$ is [[Unification|mgu]] of $\{s,s'\}$. | ||
| - | |||
| - | |||
| - | === Completeness of Rules === | ||
| - | |||
| - | How would you prove these rules are complete given Herbrand-like theorem for FOL with equality? | ||
| - | ++| Derive [[axioms for equality]].++ | ||
| - | |||
| - | ===== References ===== | ||
| - | |||
| - | * {{sav08:paramodulation-handbook.ps.gz|Paramodulation Handbook Chapter}} (or from [[http://www.lsi.upc.es/~roberto/papers/handbook.ps.gz|this link]]) | ||
| - | * [[http://www.ags.uni-sb.de/~chris/lectures/fol-hol-tp/Ruzica-Piskac-I.pdf|The Saturate System - example of a theorem prover that implements paramodulation]] | ||