Completion for unification

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.

Authors

• Narjes Doggaz
• Claude Kirchner

Keywords

No keywords are indexed for this paper.