Automated deduction with associative commutative operators

1. Siva Anantharaman, Jieh Hsiang, and Jalel Mzali. Sbreve2: A term rewriting laboratory with (AC-)unfailing completion. In N. Dershowitz, editor, Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill, (North Carolina, USA), volume 355 of Lecture Notes in Computer Science, pages 533–537. Springer-Verlag, April 1989.

   Google Scholar 

2. H.-J. Bürckert, A. Herold, D. Kapur, J. Siekmann, M. Stickel, M. Tepp, and H. Zhang. Opening the AC-unification race. Journal of Automated Reasoning, 4(1):465–474, 1988.

   Google Scholar 

3. L. Bachmair and D. Plaisted. Associative path orderings. In Proceedings 1st Conference on Rewriting Techniques and Applications, Dijon (France), volume 202 of Lecture Notes in Computer Science. Springer-Verlag, 1985.

   Google Scholar 

4. D. Brand. Proving theorems with the modification method. SIAM J. of Computing, 4:412–430, 1975.

   Google Scholar 

5. A. Ben Cherifa and P. Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9(2):137–160, October 1987.

   Google Scholar 

6. N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17:279–301, 1982.

   Google Scholar 

7. J. Hsiang and M. Rusinowitch. A new method for establishing refutational completeness in theorem proving. In J. Siekmann, editor, Proceedings 8th International Conference on Automated Deduction, Oxford (UK), volume 230 of Lecture Notes in Computer Science, pages 141–152. Springer-Verlag, 1986.

   Google Scholar 

8. J. Hsiang and M. Rusinowitch. On word problem in equational theories. In Th. Ottmann, editor, Proceedings of 14th International Colloquium on Automata, Languages and Programming, Karlsruhe (Germany), volume 267 of Lecture Notes in Computer Science, pages 54–71. Springer-Verlag, 1987.

   Google Scholar 

9. J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal of Computing, 15(4):1155–1194, 1986. Preliminary version in Proceedings 11th ACM Symposium on Principles of Programming Languages, Salt Lake City, 1984.

   Google Scholar 

10. D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, 1970.

    Google Scholar 

11. E. Kounalis and M. Rusinowitch. On word problem in Horn logic. In J.-P. Jouannaud and S. Kaplan, editors, Proceedings 1st International Workshop on Conditional Term Rewriting Systems, Orsay (France), volume 308 of Lecture Notes in Computer Science, pages 144–160. Springer-Verlag, 1987. See also the extended version published in Journal of Symbolic Computation, number 1 & 2, 1991.

    Google Scholar 

12. D.S. Lankford. A unification algorithm for abelian group theory. Technical report, Louisiana Tech. University, 1979.

    Google Scholar 

13. D.S. Lankford and A. Ballantyne. Decision procedures for simple equational theories with associative commutative axioms: complete sets of associative commutative reductions. Technical report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977.

    Google Scholar 

14. P. Narendran and M. Rusinowitch. Any ground associative-commutative theory has a finite canonical system. In R. Book, editor, Proceedings 4th Conference on Rewriting Techniques and Applications, Como, (Italy). Springer-Verlag, 1991.

    Google Scholar 

15. G. Peterson. A technique for establishing completeness results in theorem proving with equality. SIAM Journal of Computing, 12(1):82–100, 1983.

    Google Scholar 

16. G. Plotkin. Building-in equational theories. Machine Intelligence, 7:73–90, 1972.

    Google Scholar 

17. G. Peterson and M. Stickel. Complete sets of reductions for some equational theories. Journal of the Association for Computing Machinery, 28:233–264, 1981.

    Google Scholar 

18. M. Rusinowitch. Démonstration automatique-Techniques de réécriture. InterEditions, 1989.

    Google Scholar 

19. G. Robinson and L.T. Wos. Paramodulation and first-order theorem proving. In B. Meltzer and D. Mitchie, editors, Machine Intelligence 4, pages 135–150. Edinburgh University Press, 1969.

    Google Scholar 

20. J. Steinbach. Ac-termination of rewrite systems — A modified Knuth-Bendix ordering. In H. Kirchner and W. Wechler, editors, Proceedings 2nd International Conference on Algebraic and Logic Programming, Nancy (France), volume 463 of Lecture Notes in Computer Science, pages 372–386. Springer-Verlag, 1990.

    Google Scholar 

21. M. Stickel. A unification algorithm for associative-commutative functions. Journal of the Association for Computing Machinery, 28:423–434, 1981.

    Google Scholar 

22. M. Stickel. A case study of theorem proving by the knuth-bendix method Discovering that x ³=x implies ring commutativity. In Proceedings 7th International Conference on Automated Deduction, volume 170 of Lecture Notes in Computer Science. Springer-Verlag, 1984.

    Google Scholar 

23. L. Vigneron. Deduction automatique dans des théories associatives-commutatives. Rapport interne, Centre de Recherche en Informatique de Nancy, Vandœuvre-lès-Nancy, 1990.

    Google Scholar 

Download references