Efficient ground completion

1. Ackermann, W., Solvable Cases of the Decision Problem. North-Holland, Amsterdam (1954).

   Google Scholar 

2. Andrews, P.B., “Theorem Proving via General Matings,” JACM 28:2 (1981) 193–214.

   Google Scholar 

3. Bachmair, L. Proof Methods for Equational Theories, Ph.D thesis, University of Illinois, Urbana Champaign, Illinois (1987).

   Google Scholar 

4. Bachmair, L., Dershowitz, N., and Hsiang, J., “Orderings for Equational Proofs,” In Proc. Symp. Logic in Computer Science, Boston, Mass. (1986) 346–357.

   Google Scholar 

5. Dauchet, M., Tison, S., Heuillard, T., and Lescanne, P., “Decidability of the Confluence of Ground Term Rewriting Systems,” LICS'87, Ithaca, New York (1987) 353–359.

   Google Scholar 

6. Dershowitz, N., “Termination of Rewriting,” Journal of Symbolic Computation 3 (1987) 69–116.

   Google Scholar 

7. Dershowitz, N., “Completion and its Applications,” Proceedings of CREAS, Lakeway, Texas (May 1987).

   Google Scholar 

8. Downey, P.J., Samet, H., and Sethi, R., “Off-line and On-line Algorithms for Deducing Equalities,” POPL-5, Tucson, Arizona (1978).

   Google Scholar 

9. Downey, P.J., Sethi, R., and Tarjan, E.R., “Variations on the Common Subexpressions Problem,” JACM 27:4 (1980) 758–771.

   Google Scholar 

10. Gallier, J.H. Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper and Row, New York (1986).

    Google Scholar 

11. Gallier, J.H., Raatz, S., and Snyder, W., “Theorem Proving using Rigid E-Unification: Equational Matings,” LICS'87, Ithaca, New York (1987) 338–346.

    Google Scholar 

12. Gallier, J., Narendran, P., Raatz, S., and Snyder, W., “Theorem Proving using Equational Matings and Rigid E-Unification,” submitted to JACM (1988).

    Google Scholar 

13. Gallier, J.H., Narendran, P., Plaisted, D., and Snyder, W., “Rigid E-Unification is NP-complete,” LICS'88, Edinburgh, Scotland (July 1988)

    Google Scholar 

14. Gallier, J.H., Narendran, P., Plaisted, D., and Snyder, W., “Rigid E-Unification: NP-Completeness and Applications to Equational Matings,” submitted to Information and Computation (1988).

    Google Scholar 

15. Gallier, J.H., Narendran, P., Plaisted, D., Raatz, S., and Snyder, W., “Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time,” CADE-9, Argonne, Ill. (1988) (Journal version submitted to JACM (1988).)

    Google Scholar 

16. Huet, G., “Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems,” JACM 27:4 (1980) 797–821.

    Google Scholar 

17. Huet, G. and Oppen, D. C., “Equations and Rewrite Rules: A Survey,” in Formal Languages: Perspectives and Open Problems, R. V. Book (ed.), Academic Press, NY (1982).

    Google Scholar 

18. Huet, G., Lankford, D., “On the Uniform Halting Problem for Term Rewriting Systems,” Rapport de Recherche 283 (March 1978).

    Google Scholar 

19. Kamin, S., and Levy, J.-J., “Two Generalizations of the Recursive Path Ordering,” unpublished note, Department of Computer Science, University of Illinois, Urbana, IL.

    Google Scholar 

20. Kozen, D., “Complexity of Finitely Presented Algebras,” Technical Report TR 76-294, Department of Computer Science, Cornell University, Ithaca, NY (1976).

    Google Scholar 

21. Lankford, D.S., “Canonical Inference,” Report ATP-32, University of Texas (1975)

    Google Scholar 

22. Metivier, Y., “About the Rewriting Systems Produced by the Knuth-Bendix Completion Algorithm,” Information Processing Letters 16 (1983) 31–34.

    Google Scholar 

23. Nelson G., and Oppen, D. C., “Fast Decision Procedures Based on Congruence Closure,” JACM 27:2 (1980) 356–364.

    Google Scholar 

24. Oyamaguchi, M., “The Church-Rosser Property for Ground Term-Rewriting Systems is Decidable,” TCS 49 (1987) 43–79.

    Google Scholar 

25. Rosen, B., “Tree-Manipulating Systems and Church-Rosser Theorems,” JACM 20 (1973) 160–187.

    Google Scholar 

26. Shostak, R., “An Algorithm for Reasoning about Equality,” CACM 21:7 (July 1978) 583–585.

    Google Scholar 

Download references