Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:unification [2008/04/02 20:28] vkuncak |
sav08:unification [2008/04/02 20:31] vkuncak |
||
---|---|---|---|
Line 9: | Line 9: | ||
* equation $x \doteq t(x)$ where $t$ is a term containing $x$ but not identical to $x$ ++| is contradictory++ | * equation $x \doteq t(x)$ where $t$ is a term containing $x$ but not identical to $x$ ++| is contradictory++ | ||
- | ===== Unification Examples ===== | + | ===== Examples ===== |
First-order language: | First-order language: | ||
Line 39: | Line 39: | ||
**Definition:** Composition $\circ$ of substitutions. | **Definition:** Composition $\circ$ of substitutions. | ||
- | **Definition:** A //renaming// is a substitution which, viewed as function, is a bijection on the set of all variables. | + | **Definition:** A //renaming// is a substitution which is (a total function and) a bijection on the set of all variables. |
**Lemma:** If $\sigma$ is a unifier for $E$ and $\tau$ is a substitution, then $\tau \circ \sigma$ is also a unifier. | **Lemma:** If $\sigma$ is a unifier for $E$ and $\tau$ is a substitution, then $\tau \circ \sigma$ is also a unifier. | ||
Line 84: | Line 84: | ||
===== References ===== | ===== References ===== | ||
- | * [[http://www.cs.bu.edu/fac/snyder/publications/UnifChapter.pdf|Unification Theory Chapter in Handbook of Automated Reasoning]] (also {{sav08:unification-handbook.pdf|pdf file}}) | + | * [[http://www.cs.bu.edu/fac/snyder/publications/UnifChapter.pdf|Unification Theory Chapter in Handbook of Automated Reasoning]] (also {{sav08:unification-handbook.pdf|pdf file}}, see pdf page 10, Rule based approach) |
* [[http://doi.acm.org/10.1145/357162.357169|An Efficient Unification Algorithm]] (also {{sav08:unification-p258-martelli.pdf|pdf file}}) | * [[http://doi.acm.org/10.1145/357162.357169|An Efficient Unification Algorithm]] (also {{sav08:unification-p258-martelli.pdf|pdf file}}) | ||
* [[http://www.mpi-inf.mpg.de/~uwe/lehre/eqlogic/v5.pdf|Course at MPI]] | * [[http://www.mpi-inf.mpg.de/~uwe/lehre/eqlogic/v5.pdf|Course at MPI]] | ||