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.