References

[Bil96]

Jean-Paul Billon. The disconnection method --- a confluent integration of unification in the analytic framework. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, pages 110--126, Terrasini, Palermo, Italy, May 1996. Springer Verlag Lecture Notes in Artifical Intelligence 1071.

[CL73]

Chin-Liang Chang and Richard Char-Tung Lee. Symbolic Logic and Mechanical Theorem Proving. Computer Science Classics. Academic Press, 1973.

[DJ90]

Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 6, pages 243--320. Elsevier Science Publishers b.v., 1990.

[JK90]

Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: a rule-based survey of unification. Technical report, LRI, CNRS UA 410: Al Khowarizmi, March 1990.

[LP92]

Shie-Jue Lee and David A. Plaisted. Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning, 9(1):25--42, August 1992.

[MM82]

Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258--282, April 1982.

[Vor94]

Andrei Voronkov. Implementing bottom-up procedures with code trees: a case study of forward subsumption. UPMAIL Technical Report 88, Uppsala University, Computing Science Department, 1994. Available at ftp://ftp.csd.uu.se/pub/papers/reports/0088.ps.gz.