Incremental construction of unification algorithms in equational theories

  • Jean -Pierre Jouannaud
  • Claude Kirchner
  • Helene Kirchner
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 154)


Equational Theory Unification Algorithm Derivation Tree Equational Term Incremental Construction 
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. [DER,79]
    DERSHOWITZ N.: “Orderings for term-rewriting systems” Proc 20th Symposium on Foundations of Computer Science, pp 123–131 (1979). also Theorical Computer Science 17-3 (1982).Google Scholar
  2. [DER,82]
    DERSHOWITZ N.: “Computing with rewrite systems” Preliminary draft (1982)Google Scholar
  3. [FAY,79]
    FAY M.: “First order unification in equational theory” Proc. 4th Workshop on Automata Deduction Texas (1979).Google Scholar
  4. [HUE,80]
    HUET G.: “Confluent reductions: abstract properties and applications to term rewriting systems” J. Assoc. Comp. Mach. 27-4, pp 797–821 (1980).Google Scholar
  5. [HUL,80]
    HULLOT J. M.: “Canonical forms and unification” Proc. 5th Workshop on Automated Deduction Les Arcs (1980).Google Scholar
  6. [JKK,82]
    JOUANNAUD J.P. KIRCHNER C. KIRCHNER H.: “Incremental unification in equational theories”. Proc. of the Allerton conference (1982).Google Scholar
  7. [JKK,83]
    JOUANNAUD J.P. KIRCHNER C. KIRCHNER H.: “Incremental construction of unification algorithms in equationnal theories”. Internal report 83-R-008. Centre de Recherche en Informatique de Nancy (1983).Google Scholar
  8. [JLR,82]
    JOUANNAUD J.P., LESCANNE P., REINIG F.: “Recursive decomposition ordering” in “Formal description of programming concepts 2”. Ed. BJORNER D., North Holland (1982).Google Scholar
  9. [JOU,83]
    JOUANNAUD J.P.: “Confluent and Coherent sets of reductions with equations. Application to proofs in data types”. Proc. of the 8th Colloquium on Trees in algebra and programming. To appear in LNCS (1983).Google Scholar
  10. [K&B,70]
    KNUTH D. BEND IX P.: “Simple word problems in universal algebras” in “Computational problems in abstract algebra” Leech J. ed. Pergamon Press, pp 263–297 (1970).Google Scholar
  11. [K&K,82]
    KIRCHNER C, KIRCHNER H.: “Contribution à la résolution d'équations dans les algèbres libres et les variétés équationnelles d'algèbres”. Thèse de doctorat de spécialité, C. R. I. N., Nancy (1982).Google Scholar
  12. [KKJ,81]
    KIRCHNER C., KIRCHNER H., JOUANNAUD J.P.: “Algebraic manipulations as a unification and matching strategy for linear equations in signed binary trees”. Proc. IJCAI 81 Vancouver (1981).Google Scholar
  13. [K&L,82]
    KAMIN, LEVY J.J.: “Attempts for generalizing the recursive path ordering”. To be published.Google Scholar
  14. [LAN,75]
    LANKFORD D.S.: “Canonical inference”. Report ATP-32, dpt. Math. and comp. sciences, Univ. of Texas at Austin (1975).Google Scholar
  15. [LAN,79]
    LANKFORD D.S.: “A unification algorithm for abelian group theory” Report MTP-1. Math. dep., Louisiana Tech. U. (1979).Google Scholar
  16. [L&S,77]
    LIVESEY M. and SIEKMANN J.: “Unification of sets” Report 3/76, Institut fur Informatik 1, Univ. Karlsruhe, (1977).Google Scholar
  17. [M&M,82]
    MARTELLI A. and MONTANARI U.: “An efficient unification algorithm”. T.O.P.L.A.S., Vol. 4, No. 2, pp 258–282. (1982).Google Scholar
  18. [PLO,72]
    PLOTKIN G.: “Building in equational theories” Machine Intelligence 7, pp 73–90 (1972).Google Scholar
  19. [P&S,81]
    PETERSON G. E. and STICKEL M.E.: “Complete sets of reductions for equational theories with complete unification algorithms” J.ACM 28, no.2, pp 233–264 (1981).Google Scholar
  20. [R&S,78]
    RAULEFS P. and SIEKMANN J.:”Unification of idempotent functions” Report, Institut fur Informatik 1, Univ. Karlsruhe, (1978).Google Scholar
  21. [S&S,82]
    SIEKMANN J. and SZABO P.:”Universal unification” Report, Institut fur Informatik 1, Univ. Karlsruhe, (1982).Google Scholar
  22. [STI,81]
    STICKEL M.E.: “A unification algorithm for associative-commutative functions”. J.ACM 28, no.3, pp 423–434 (1981).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • Jean -Pierre Jouannaud
    • 1
  • Claude Kirchner
    • 1
  • Helene Kirchner
    • 1
  1. 1.Centre de Recherche en Informatique de Nancy et GRECO Programmation Campus scientifiqueVandoeuvre-les-Nancy CedexFrance

Personalised recommendations