TY - GEN
T1 - Associative-Commutative Unification
AU - Fages, François
N1 - Publisher Copyright:
© 1984, Springer-Verlag New York, Inc.
PY - 1984/1/1
Y1 - 1984/1/1
N2 - Unification in equational theories, that is solving equations in varieties, is of special relevance to automated deduction. Recent results in term rewriting systems, as in [Peterson and Stickel 81] and [Hsiang 82], depend on unification in presence of associative-commutative functions. Stickel [75,81] gave an associative-commutative unification algorithm, but its termination in the general case was still questioned. Here we give an abstract framework to present unification problems, and we prove the total correctness of Stickel’s algorithm. The first part of this paper is an introduction to unification theory, The second part is devoted to the associative-commutative ease. The algorithm of Stickel is defined in ML [Gordon, Milner and Wadsworth 79] since in addition to being an effective programming language, ML is a precise and concise formalism close to the standard mathematical notations. The proof of termination and completeness is based on a relatively simple measure of complexity for associative-commutative unification problems.
AB - Unification in equational theories, that is solving equations in varieties, is of special relevance to automated deduction. Recent results in term rewriting systems, as in [Peterson and Stickel 81] and [Hsiang 82], depend on unification in presence of associative-commutative functions. Stickel [75,81] gave an associative-commutative unification algorithm, but its termination in the general case was still questioned. Here we give an abstract framework to present unification problems, and we prove the total correctness of Stickel’s algorithm. The first part of this paper is an introduction to unification theory, The second part is devoted to the associative-commutative ease. The algorithm of Stickel is defined in ML [Gordon, Milner and Wadsworth 79] since in addition to being an effective programming language, ML is a precise and concise formalism close to the standard mathematical notations. The proof of termination and completeness is based on a relatively simple measure of complexity for associative-commutative unification problems.
U2 - 10.1007/978-0-387-34768-4_12
DO - 10.1007/978-0-387-34768-4_12
M3 - Conference contribution
AN - SCOPUS:85034750377
SN - 9780387960227
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 194
EP - 208
BT - 7th International Conference on Automated Deduction - Proceedings
A2 - Shostak, R.E.
PB - Springer Verlag
T2 - 7th International Conference on Automated Deduction,CADE 1984
Y2 - 14 May 1984 through 16 May 1984
ER -