Differences
This shows you the differences between two versions of the page.
sav08:proof_rule_for_equality [2008/04/02 20:11] vkuncak |
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'\}$. | ||
- | |||
- | === 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]] | ||