Abstract
We address here the problem of unification in equational theories. A new unification method for some equational theories is given. It is a generalization of the Martelli and Montanari’s algorithm and is based on a decomposition-merging-normalization process. We prove that for the class of decomposable theories this method gives a complete set of unifiers for any equation.
We apply the general results to the MINUS theories that contain axioms like −(−x) =x and −(f(x, y))=f(−y,−x) and we give an original unification algorithm for this type of theory.
This research was supported in part by Anence pour le Developpement de l’Informatique, under contract 82/767.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
CORBIN J. and BIDOIT M. “Pour une rehabilitation de l’algorithme d’unification de Robinson”. Note a l’academie de sciences de Paris. T.296, Serie I, p 279. (1983).
DERSHOWITZ N.: “Orderings for term-rewriting systems”. Theorical Computer Science 17–3. (1982).
FAGES F.: “Formes canoniques dans les algebres booleennes, et application a la demonstration automatique en logique de premier ordre”. These de 3ieme cycle. Unlversite Paris 6. (1983).
FAGES F.: “Associative-Commutative Unification” Proceedings 7th CADE, Napa Valley, 1984.
FAY M.: “First order unification in equational theory” Proc. 4th Workshop on Automata Deduction Texas. (1979).
HUET G. and OPPEN D.C.: “Equations and rewrite rules: a survey” in “Formal Languages: Perspectives and open problems” Ed. Book R., Academic Press. (1980).
HUET G.: “Resolution d’equation dans les langages d’ordre 1,2...,” These d’etat, Universite Paris VII. (1976).
HULLOT J. M.: “Canonical forms and unification” Proc. 5th Workshop on Automated Deduction Les Arcs. (1980).
JOUANNAUD J.P. KIRCHNER C. KIRCHNER H.: “Incremental construction of unification algorithms in equationnal theories”. Proc. of the 10th ICALP. LNCS 154, p 361. (1983).
JOUANNAUD J.P. KIRCHNER H.: “Completion of a set of rules modulo a set of equations”. Proc. of the 11th ACM conference on principles of programming languages, Salt Lake City. (1984).
KIRCHNER.: ‘A new unification method in equational theories and its application to the MINUS theories”. Internal report CRIN 83-R-xxx. (1983).
KIRCHNER.: “A general inductive completion algorithm and application to abstract data types”. Proceedings 7th CADE, Napa Valley, 1984.
KNUTH D. BENDIX P.: “Simple word problems in universal algebras” in “Computational problems in abstract algebra” Leech J. ed. Pergamon Press, pp 263–297 (1970).
KIRCHNER C., KIRCHNER H., JOUANNAUD J.P.: “Algebraic mauipulations as a unification and matching strategy for linear equations in signed binary trees”. Proc. IJCAI 81 Vancouver. (1981).
KIRCHNER C. KIRCHNER H.: “Resolution d’equations dans les algebres libres et les varietes eq1ationnelles”. These de 3eme cycle, Universite NANCY 1. (1982)
LANKFORD D.S.: “Canonical inference”. Report ATP-32. University of Texas. (1975).
LANKFORD D.S.: “A unification algorithm for abelian group theory” Report MTP-1. Math. dep., Louisiana Tech. U. (1979).
83] LESCANNE P.: “Computer experiments with the REVE term rewriting system generator”. Proc. of the 10th POPL conference. (1983).
LIVESEY M. and SIEKMANN J.: “Unification of sets” Report 3/76, Institut fur Informatik 1, Univ. Karlsruhe. (1977).
MARTELLI A. and MONTANARI U.: “An efficient unification algorithm” Transactions on Programming Langaages and Systems Vol. 4, Number 2. p 258. (1992).
PLOTKIN G.: “Building in equational theories” Machine Intelligence 7, pp 73–90. (1972).
PATERSON M.S. and WEGMAN M.N.: “Linear unification” J. of Computer and Systems Sciences 16 pp 158–167. (1978).
ROBINSON J.A.: “A machine oriented logic based on the resolution principle” J.ACM 12, pp 32–41. (1965).
ROBINSON J.A.: “computational logic: the unification computation”. Machine Intelligence 6. (1971).
RAULEFS P. and SIEKMANN J.: “Unification of idempotent functions” Report, Institut fur Informatik 1, Univ. Karlsruhe. (1978).
SIEKMANN J. and SZABO P.: “Universal unification and a classification of equational theories”. Proc. of the 6th CADE. LNCS 138, p 369. (1992).
STICKEL M.E.: “A unification algorithm for associative-commutative functions” J.ACM 28, no.3, pp 423–434. (1981).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kirchner, C. (1984). A New Equational Unification Method: A Generalisation of Martelli-Montanari’s Algorithm. In: Shostak, R.E. (eds) 7th International Conference on Automated Deduction. CADE 1984. Lecture Notes in Computer Science, vol 170. Springer, New York, NY. https://doi.org/10.1007/978-0-387-34768-4_14
Download citation
DOI: https://doi.org/10.1007/978-0-387-34768-4_14
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-96022-7
Online ISBN: 978-0-387-34768-4
eBook Packages: Springer Book Archive