Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 1994: Automated Deduction — CADE-12 pp 530–544Cite as

Associative-commutative deduction with constraints

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 814))

Abstract

Associative-commutative equational reasoning is known to be highly complex for theorem proving. Hence, it is very important to focus deduction by adding constraints, such as unification and ordering, and to define efficient strategies, such as the basic requirements à la Hullot. Constraints are formulas used for pruning the set of ground instances of clauses deduced by a theorem prover. We propose here an extension of AC-paramodulation and AC-superposition with these constraint mechanisms; we do not need to compute AC-unifiers anymore. The method is proved to be refutationally complete, even with simplification. The power of this approach is exemplified by a very short proof of the equational version of SAM's Lemma using DATAC, our implementation of the strategy.

This work is partially supported by the GDR Programmation and the Esprit Basic Research working group 6028, CCL.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Bachmair and H. Ganzinger. On restrictions of ordered paramodulation with simplification. In M. E. Stickel, editor, Proc. 10th CADE Conf., Kaiserslautern (Germany), volume 449 of LNCS, pages 427–441. Springer-Verlag, July 1990.

    Google Scholar 

  2. L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation and superposition. In Proc. 11th CADE Conf., Saratoga Springs (N.Y., USA), pages 462–476, 1992.

    Google Scholar 

  3. A. M. Ballantyne and D. S. Lankford. The refutation completeness of blocked permutative narrowing and resolution. In Proc. of Fourth Workshop on Automated Deduction, Austin, Texas, 1979.

    Google Scholar 

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

    Google Scholar 

  5. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. Elsevier Science Publishers B. V. (North-Holland), 1990.

    Google Scholar 

  6. J. R. Guard, F. C. Oglesby, J. H. Bennett, and Settle. Semi-automated mathematics. JACM, 16:49–62, 1969.

    Google Scholar 

  7. J. Hsiang and M. Rusinowitch. Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method. JACM, 38(3):559–587, July 1991.

    Google Scholar 

  8. J.-M. Hullot. Compilation de Formes Canoniques dans les Théories équationelles. Th. 3e cycle, Université de Paris Sud, Orsay (France), 1980.

    Google Scholar 

  9. J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: a rule-based survey of unification. In J.-L. Lassez and G. Plotkin, editors, Computational Logic. Essays in honor of Alan Robinson, chapter 8, pages 257–321. MIT Press, Cambridge (MA, USA), 1991.

    Google Scholar 

  10. C. Kirchner, H. Kirchner, and M. Rusinowitch. Deduction with symbolic constraints. Revue d'Intelligence Artificielle, 4(3):9–52, 1990. Special issue on Automatic Deduction.

    Google Scholar 

  11. D. Kapur, D. R. Musser, and P. Narendran. Only prime superpositions need be considered in the Knuth-Bendix procedure, 1985. Computer Science Branch, Corporate Research and Development, General Electric, Schenectady, New York.

    Google Scholar 

  12. W. McCune. Challenge equality problems in lattice theory. In E. Lusk and R. Overbeek, editors, Proc. 9th CADE Conf., Argonne (Ill., USA), volume 310 of LNCS, pages 704–709. Springer-Verlag, 1988.

    Google Scholar 

  13. U. Martin and T. Nipkow. Ordered rewriting and confluence. In M. E. Stickel, editor, Proc. 10th CADE Conf., Kaiserslautern (Germany), volume 449 of LNCS. Springer-Verlag, 1990.

    Google Scholar 

  14. P. Narendran and M. Rusinowitch. Any ground associative-commutative theory has a finite canonical system. In R. V. Book, editor, Proc. 4th RTA Conf., Como (Italy). Springer-Verlag, 1991.

    Google Scholar 

  15. R. Nieuwenhuis and A. Rubio. Basic superposition is complete. In B. Krieg-Brückner, editor, Proceedings of ESOP'92, volume 582 of LNCS, pages 371–389. Springer-Verlag, 1992.

    Google Scholar 

  16. R. Nieuwenhuis and A. Rubio. Theorem proving with ordering constrained clauses. In D. Kapur, editor, Proceedings of CADE-11, volume 607 of LNCS, pages 477–491. Springer-Verlag, 1992. [NR94] R. Nieuwenhuis and A. Rubio. AC-superposition with constraints: no AC-unifiers needed. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, Nancy (France), LNCS. Springer-Verlag, 1994.

    Google Scholar 

  17. E. Paul. A general refutational completeness result for an inference procedure based on associative-commutative unification. JSC, 14(6):577–618, 1992.

    Google Scholar 

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

    Google Scholar 

  19. G. E. Peterson. Complete sets of reductions with constraints. In M. E. Stickel, editor, Proc. 10th CADE Conf., Kaiserslautern (Germany), volume 449 of LNCS, pages 381–395. Springer-Verlag, 1990.

    Google Scholar 

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

    Google Scholar 

  21. G. Peterson and M. E. Stickel. Complete sets of reductions for some equational theories. JACM, 28:233–264, 1981.

    Google Scholar 

  22. A. Rubio and R. Nieuwenhuis. A precedence-based total ac-compatible ordering. In C. Kirchner, editor, Proc. 5th RTA Conf., Montreal (Canada), volume 690 of LNCS, pages 374–388. Springer-Verlag, 1993.

    Google Scholar 

  23. M. Rusinowitch. Theorem-proving with resolution and superposition. JSC, 11:21–49, 1991.

    Google Scholar 

  24. M. Rusinowitch and L. Vigneron. Automated deduction with associative commutative operators. In P. Jorrand and J. Kelemen, editors, Fundamental of Artificial Intelligence Research, volume 535 of LNCS, pages 185–199. Springer-Verlag, 1991.

    Google Scholar 

  25. M. Rusinowitch and L. Vigneron. Automated deduction with associative commutative operators. Internal rep. 1896, INRIA, May 1993. To appear in J. of Applicable Algebra in Engineering, Communication and Computation.

    Google Scholar 

  26. J. R. Slagle. Automated theorem-proving for theories with simplifiers, commutativity and associativity. JACM, 21(4):622–642, 1974.

    Google Scholar 

  27. L. Vigneron. Basic AC-paramodulation. In F. Orejas, editor, Proc. 2nd CCL Workshop, La Escala (Spain), September 1993.

    Google Scholar 

  28. U. Wertz. First-order theorem proving modulo equations. Technical Report MPI-I-92-216, MPI Informatik, April 1992.

    Google Scholar 

  29. H. Zhang and D. Kapur. First-order theorem proving using conditional rewrite rules. In E. Lusk and R. Overbeek, editors, Proc. 9th CADE Conf., Argonne (Ill., USA), volume 310 of LNCS, pages 1–20. Springer-Verlag, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CRIN-CNRS & INRIA-Lorraine, BP 239, 54506, Vandœuvre-lès-Nancy Cedex, France

    Laurent Vigneron

Authors
  1. Laurent Vigneron
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Alan Bundy

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Vigneron, L. (1994). Associative-commutative deduction with constraints. In: Bundy, A. (eds) Automated Deduction — CADE-12. CADE 1994. Lecture Notes in Computer Science, vol 814. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58156-1_39

Download citation

  • DOI: https://doi.org/10.1007/3-540-58156-1_39

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58156-7

  • Online ISBN: 978-3-540-48467-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation