A proof theory for general unification (Q1189467)

The topic of this book is \(E\)-unification and higher-order unification as extensions of the Martelli-Monanari method. First, a survey of the method for standard unification using transformations on systems of equations is presented, as well as soundness and completeness results. Then, \(\S 4\) outlines basic results on \(E\)-unification and proves the completeness of the narrowing method. \(\S 5\) defines a new representation of equational proofs as certain sets of trees. These trees are used to prove soundness and completeness of certain sets of transformations. In \(\S 6\) soundness and completeness results for an improved set of transformations are shown using the concept of unfailing completion. \(\S 7\) provides a proof of soundness and completeness of a method for higher-order unification and completeness of the strategy of eager variable elemination.