A New Equational Unification Method: A Generalisation of Martelli-Montanari’s Algorithm

  • Claude Kirchner
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


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.


Equational Theory Unification Algorithm Minus Theory Decomposable Theory Reflexive Transitive Closure 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [C&B,83]
    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).zbMATHGoogle Scholar
  2. [DER,82]
    DERSHOWITZ N.: “Orderings for term-rewriting systems”. Theorical Computer Science 17–3. (1982).Google Scholar
  3. [FAG,83]
    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).Google Scholar
  4. [FAG,84]
    FAGES F.: “Associative-Commutative Unification” Proceedings 7th CADE, Napa Valley, 1984.Google Scholar
  5. [FAY,79]
    FAY M.: “First order unification in equational theory” Proc. 4th Workshop on Automata Deduction Texas. (1979).Google Scholar
  6. [H&O,80]
    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).Google Scholar
  7. [HUE,76]
    HUET G.: “Resolution d’equation dans les langages d’ordre 1,2...,” These d’etat, Universite Paris VII. (1976).Google Scholar
  8. [HUL,80]
    HULLOT J. M.: “Canonical forms and unification” Proc. 5th Workshop on Automated Deduction Les Arcs. (1980).Google Scholar
  9. [JKK,83]
    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).Google Scholar
  10. [J&K,84]
    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).Google Scholar
  11. [KIR,83]
    KIRCHNER.: ‘A new unification method in equational theories and its application to the MINUS theories”. Internal report CRIN 83-R-xxx. (1983).Google Scholar
  12. [KIR,84]
    KIRCHNER.: “A general inductive completion algorithm and application to abstract data types”. Proceedings 7th CADE, Napa Valley, 1984.Google Scholar
  13. [K&B,70]
    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).Google Scholar
  14. [KKJ,81]
    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).Google Scholar
  15. [K&K,82]
    KIRCHNER C. KIRCHNER H.: “Resolution d’equations dans les algebres libres et les varietes eq1ationnelles”. These de 3eme cycle, Universite NANCY 1. (1982)Google Scholar
  16. [LAN,75]
    LANKFORD D.S.: “Canonical inference”. Report ATP-32. University of Texas. (1975).Google Scholar
  17. [LAN,79]
    LANKFORD D.S.: “A unification algorithm for abelian group theory” Report MTP-1. Math. dep., Louisiana Tech. U. (1979).Google Scholar
  18. [LES.
    83] LESCANNE P.: “Computer experiments with the REVE term rewriting system generator”. Proc. of the 10th POPL conference. (1983).Google Scholar
  19. [L&B,77]
    LIVESEY M. and SIEKMANN J.: “Unification of sets” Report 3/76, Institut fur Informatik 1, Univ. Karlsruhe. (1977).Google Scholar
  20. [M&M,82]
    MARTELLI A. and MONTANARI U.: “An efficient unification algorithm” Transactions on Programming Langaages and Systems Vol. 4, Number 2. p 258. (1992).CrossRefzbMATHGoogle Scholar
  21. [PLO,72]
    PLOTKIN G.: “Building in equational theories” Machine Intelligence 7, pp 73–90. (1972).zbMATHGoogle Scholar
  22. [P&W,78]
    PATERSON M.S. and WEGMAN M.N.: “Linear unification” J. of Computer and Systems Sciences 16 pp 158–167. (1978).MathSciNetCrossRefzbMATHGoogle Scholar
  23. [ROB,65]
    ROBINSON J.A.: “A machine oriented logic based on the resolution principle” J.ACM 12, pp 32–41. (1965).MathSciNetCrossRefzbMATHGoogle Scholar
  24. [ROB,71]
    ROBINSON J.A.: “computational logic: the unification computation”. Machine Intelligence 6. (1971).Google Scholar
  25. [R&S,78]
    RAULEFS P. and SIEKMANN J.: “Unification of idempotent functions” Report, Institut fur Informatik 1, Univ. Karlsruhe. (1978).Google Scholar
  26. [S&S,82]
    SIEKMANN J. and SZABO P.: “Universal unification and a classification of equational theories”. Proc. of the 6th CADE. LNCS 138, p 369. (1992).Google Scholar
  27. [STI,81]
    STICKEL M.E.: “A unification algorithm for associative-commutative functions” J.ACM 28, no.3, pp 423–434. (1981).MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Claude Kirchner
    • 1
    • 2
  1. 1.Centre de Recherche en Informatique de NANCYVandoeuvre les Nancy CedexFrance
  2. 2.GRECO-ProgrammationUSA

Personalised recommendations