E-unification algorithms for a class of confluent term rewriting systems

1. Fay, M.J., “First-order unification in an equational theory,” in 4th Workshop on Automated Deduction, pp. 161–167, Austin, Texas, February, 1979.

   Google Scholar 

2. Fribourg, L., “A superposition oriented theorem prover,” Tech. Report 11, L.I.T.P., 1983, To appear in Theoretical Compute Science, short version in Proc. IJCAI-83, pp. 923–925.

   Google Scholar 

3. Fribourg, L., “SLOG: A logic programming language interpreter based on clausal superposition and rewriting,” in Proc. 1985 International Symposium on Logic Programming, pp. 172–184, Boston, Mass., July, 1985.

   Google Scholar 

4. Hoffmann, C.M. and M. O'Donnell, “Programming with equations,” ACM TOPLAS, vol. 4, no. 1, pp. 83–112, January, 1982.

   Google Scholar 

5. Hullot, J.M., “Canonical forms and unification,” in Proc. 5th Conference on Automated Deduction, pp 318–334, 1980.

   Google Scholar 

6. Hussmann, H., “Unification in conditional-equational theories,” Tech. Report MIP 8502, Universitat Passau, January, 1985.

   Google Scholar 

7. Knuth, D. and P. Bendix, “Simple word problems in universal algebras,” in Computational problems in abstract algebra, ed. J. Leech, pp. 163–279, Pergamon Press, 1970.

   Google Scholar 

8. Jouannaud, J.P., C. Kirchner and H. Kirchner, “Incremental construction of unification algorithms in equational theories,” in Proc. 10th Colloquium on Automata, Languages and Programming, 1983.

   Google Scholar 

9. Lankford, D.S., “Canonical inference,” Technical Report ATP-32, Department of Mathematics and Computer Science, University of Texas at Austin, December, 1975.

   Google Scholar 

10. Plotkin, G., “Building-in equational theories,” in Machine Intelligence 7, pp. 73–90, Edinburgh University Press, 1972.

    Google Scholar 

11. O'Donnell, M., “Computing in systems described by equations,” in Lecture notes in computer science, vol. 58, Springer-Verlag, New York, 1977.

    Google Scholar 

12. Rety P, C. Kirchner, H. Kirchner and P. Lescanne, “NARROWER: a new algorithm and its application to logic programming,” in Proc. Rewriting Techniques and Applications, also in Lecture Notes in Computer Science 202, pp. 141–157, 1985.

    Google Scholar 

13. Robinson, J.A., “A machine oriented logic based on the resolution,” in Journal of ACM, vol 12, no. 1 pp. 23–41, January, 1965.

    Google Scholar 

14. Siekmann, J., “Universal unification,” in Proc. 7th International Conference on Automated Deduction, pp. 1–42, Napa, California, May, 1984.

    Google Scholar 

15. Subrahmanyam, P.A. and Jia-Huai You, “FUNLOG: a computational model integrating logic programming and functional programming,” in Logic programming: relations, functions and equations, eds. D. DeGroot and G. Lindstrom, Prentice-Hall, 1986.

    Google Scholar 

16. You, J.-H. and P.A. Subrahmanyam, “A class of term rewriting systems and unification,” unpublished manuscript, 1985.

    Google Scholar 

17. You, J.-H. and P.A. Subrahmanyam, “Equational logic programming: an extension to equational programming,” in Proc. 13th POPL, pp. 209–218, St. Petersburg, Florida, January, 1986.

    Google Scholar 

Download references