Skip to main content
SpringerLink
Log in

Associative-commutative superposition

  • Conference paper
  • First Online:
Book cover Conditional and Typed Rewriting Systems (CTRS 1994)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 968))

Included in the following conference series:

Abstract

We present an associative-commutative paramodulation calculus that generalizes the associative-commutative completion procedure to first-order clauses. The calculus is parametrized by a selection function (on negative literals) and a well-founded ordering on terms. It is compatible with an abstract notion of redundancy that covers such simplification techniques as tautology deletion, subsumption, and simplification by (associative-commutative) rewriting. The proof of refutational completeness of the calculus is comparatively simple, and the techniques employed may be of independent interest.

The research described in this paper was supported in part by the NSF under research grant INT-9314412, by the German Science Foundation (Deutsche Forschungsgemeinschaft) under grant Ga 261/4-1, by the German Ministry for Research and Technology (Bundesministerium für Forschung und Technologie) under graut ITS 9102/ITS 9103 and by the ESPRIT Basic Research Working Group 6028 (Construction of Computational Logics). The first author was also supported by the Alexander von Humboldt Foundation.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • L. Bachmair, N. Dershowitz and D. Plaisted, 1989. Completion without failure. In H. Ait-Kaci, M. Nivat, editors, Resolution of Equations in Algebraic Structures, vol. 2, pp. 1–30. Academic Press.

    Google Scholar 

  • L. Bachmair and H. Ganzinger, 1990. On Restrictions of Ordered Paramodulation with Simplification. In M. Stickel, editor, Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, Lecture Notes in Computer Science, vol. 449, pp. 427–441, Berlin, Springer-Verlag.

    Google Scholar 

  • L. Bachmair and H. Ganzinger, 1993. Rewrite Techniques for Transitive Relations. Technical Report MPI-I-93-249, Max-Planck-Institut für Informatik, Saarbrücken. Short version in Proc. LICS'94, pp. 384–393, 1994.

    Google Scholar 

  • L. Bachmair and H. Ganzinger, 1994. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, Vol. 4, No. 3, pp. 217–247. Revised version of Technical Report MPI-I-91-208, 1991.

    Google Scholar 

  • L. Bachmair, H. Ganzinger, Chr. Lynch and W. Snyder, 1992. Basic Paramodulation and Superposition. In D. Kapur, editor, Automated Deduction — CADE'11, Lecture Notes in Computer Science, vol. 607, pp. 462–476, Berlin, Springer-Verlag.

    Google Scholar 

  • Leo Bachmair, Harald Ganzinger and Uwe Waldmann, 1994. Refutational Theorem Proving for Hierarchic First-Order Theories. Applicable Algebra in Engineering, Communication and Computing, Vol. 5, No. 3/4, pp. 193–212. Earlier version: Theorem Proving for Hierarchic First-Order Theories, in Giorgio Levi and Hélène Kirchner, editors, Algebraic and Logic Programming, Third International Conference, LNCS 632, pages 420–434, Volterra, Italy, September 2–4, 1992, Springer-Verlag.

    Google Scholar 

  • Timothy Baird, Gerald Peterson and Ralph Wilkerson, 1989. Complete sets of reductions modulo associativity, commutativity and identity. In Proc. 3rd Int. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 355, pp. 29–44, Berlin, Springer-Verlag.

    Google Scholar 

  • N. Dershowitz and J.-P. Jouannaud, 1990. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6, pp. 243–309. North-Holland, Amsterdam.

    Google Scholar 

  • J. Hsiang and M. Rusinowitch, 1991. Proving refutational completeness of theorem proving strategies: The transfinite semantic Tree method. Journal of the ACM, Vol. 38, No. 3, pp. 559–587.

    Article  Google Scholar 

  • Jieh Hsiang and Michael Rusinowitch, 1987. On Word Problems in Equational Theories. In Proc. 14th ICALP, Lecture Notes in Computer Science, vol. 267, pp. 54–71, Berlin, Springer-Verlag.

    Google Scholar 

  • Jean-Pierre Jouannaud and Claude Marché, 1992. Termination and completion modulo associativity, commutativity and identity. Theoretical Computer Science, Vol. 104, pp. 29–51.

    Article  Google Scholar 

  • Paliath Narendran and Michaël Rusinowitch, 1991. Any Ground Associative-Commutative Theory has a Finite Canonical System. In Ronald V. Book, editor, Proc. 4th Rewriting Techniques and Applications 91, Como, Italy, Springer-Verlag.

    Google Scholar 

  • R. Nieuwenhuis and A. Rubio, 1992. Basic superposition is complete. In ESOP'92, Lecture Notes in Computer Science, vol. 582, pp. 371–389, Berlin, Springer-Verlag.

    Google Scholar 

  • R. Nieuwenhuis and A. Rubio, 1994. AC-superposition with constraints: No AC-unifiers needed. In Proc. 12th International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 814, pp. 545–559, Berlin, Springer-Verlag.

    Google Scholar 

  • John Pais and G.E. Peterson, 1991. Using Forcing to Prove Completeness of resolution and Paramodulation. Journal of Symbolic Computation, Vol. 11, pp. 3–19.

    Google Scholar 

  • E. Paul, 1992. A general refutational completeness result for an inference procedure based on associative-commutative unification. Journal of Symbolic Computation, Vol. 14, pp. 577–618.

    Google Scholar 

  • G. Peterson and M. Stickel, 1981. Complete sets of reductions for some equational theories. Journal of the ACM, Vol. 28, pp. 233–264.

    Article  Google Scholar 

  • A. Rubio and R. Nieuwenhuis, 1993. A precedence-based total AC-compatible ordering. In Proc. 5th Int. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 690, pp. 374–388, Berlin, Springer-Verlag.

    Google Scholar 

  • M. Rusinowitch, 1991. Theorem proving with resolution and superposition: An extension of the Knuth and Bendix completion procedure as a complete set of inference rules. J. Symbolic Computation, Vol. 11, pp. 21–49.

    Google Scholar 

  • M. Rusinowitch and L. Vigneron, 1991. Automated deduction with associative-commutative operators. In Proc. Int. Workshop on Fundamentals of Artificial Intelligence Research, Lecture Notes in Artificial Intelligence, vol. 535, pp. 185–199, Berlin, Springer-Verlag.

    Google Scholar 

  • L. Vigneron, 1994. Associative-commutative dedution with constraints. In Proc. 12th International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 814, pp. 530–544, Berlin, Springer-Verlag.

    Google Scholar 

  • U. Wertz, 1992. First-Order Theorem Proving Modulo Equations. Technical Report MPI-I-92-216, Max-Planck-Institut für Informatik, Saarbrücken.

    Google Scholar 

  • H. Zhang, 1988. Reduction, superposition and induction: Automated reasoning in an equational logic. PhD thesis, Rensselaer Polytechnic Institute, Schenectady, New York.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, SUNY at Stony Brook, 11794, Stony Brook, NY, USA

    Leo Bachmair

  2. Max-Planck-Institut für Informatik, Im Stadtwald, D-66123, Saarbrücken, Germany

    Harald Ganzinger

Authors
  1. Leo Bachmair
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Harald Ganzinger
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Nachum Dershowitz Naomi Lindenstrauss

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bachmair, L., Ganzinger, H. (1995). Associative-commutative superposition. In: Dershowitz, N., Lindenstrauss, N. (eds) Conditional and Typed Rewriting Systems. CTRS 1994. Lecture Notes in Computer Science, vol 968. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60381-6_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-60381-6_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60381-8

  • Online ISBN: 978-3-540-45513-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation