TCS Journal 1991 Journal Article
Completion for unification
- Narjes Doggaz
- Claude Kirchner
Syntactic theories have the nice property that a unification algorithm may be computed directly from the form of the axioms of a specific presentation, called resolvent, of the theory. In this work we present and prove a completion algorithm that, for a given presentation, returns a resolvent set of axioms whenever it terminates.