Skip to main content
SpringerLink
Log in

Deriving Theory Superposition Calculi from Convergent Term Rewriting Systems

  • Conference paper
Rewriting Techniques and Applications (RTA 2000)

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

Included in the following conference series:

Abstract

We show how to derive refutationally complete ground superposition calculi systematically from convergent term rewriting systems for equational theories, in order to make automated theorem proving in these theories more effective. In particular we consider abelian groups and commutative rings. These are difficult for automated theorem provers, since their axioms of associativity, commutativity, distributivity and the inverse law can generate many variations of the same equation. For these theories ordering restrictions can be strengthened so that inferences apply only to maximal summands, and superpositions into the inverse law that move summands from one side of an equation to the other can be replaced by an isolation rule that isolates the maximal terms on one side. Additional inferences arise from superpositions of extended clauses, but we can show that most of these are redundant. In particular, none are needed in the case of abelian groups, and at most one for any pair of ground clauses in the case of commutative rings.

Complete proofs can be found in http://www.mpi-sb.mpg.de/~juergen/publications/Stuber1999Diss.html .

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, Cambridge (1998)

    Google Scholar 

  • Bachmair, L., Ganzinger, H.: Associative-commutative superposition. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol. 968, pp. 1–14. Springer, Heidelberg (1995)

    Google Scholar 

  • Bachmair, L., Ganzinger, H.: Buchberger’s algorithm: A constraintbased completion procedure. In: Jouannaud, J.-P. (ed.) CCL 1994. LNCS, vol. 845, pp. 285–301. Springer, Heidelberg (1994b)

    Chapter  Google Scholar 

  • Bachmair, L., Ganzinger, H.: Equational reasoning in saturation-based theorem proving. In: Automated Deduction - A Basis for Applications. ch. 11, vol. I, pp. 353–397. Kluwer, Dordrecht (1998)

    Google Scholar 

  • Bachmair, L., Tiwari, A.: D-bases for polynomial ideals over commutative noetherian rings. In: Comon, H.(ed.) RTA 1997. LNCS, vol. 1103, pp. 113–127. Springer, Heidelberg (1997)

    Google Scholar 

  • Bachmair, L., Ganzinger, H., Stuber, J.: Combining algebra and universal algebra in first-order theorem proving: The case of commutative rings. In: Reggio, G., Astesiano, E., Tarlecki, A. (eds.) Abstract Data Types 1994 and COMPASS 1994. LNCS, vol. 906, pp. 1–29. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  • Becker, T., Weispfenning, V.: Gröbner Bases: A Computational Approach to Commutative Algebra. Springer, Heidelberg (1993)

    MATH  Google Scholar 

  • Buchberger, B., Loos, R.: Algebraic simplification. Computer Algebra: Symbolic and Algebraic Computation, 2nd edn., pp. 11–43. Springer, Heidelberg (1983)

    Google Scholar 

  • Buchberger, B.: Ein algorithmisches Kriterium für die Lösbarkeit eines algebraischen Gleichungssystems. Aequationes Mathematicae 4, 374–383 (1970)

    Article  MATH  MathSciNet  Google Scholar 

  • Buchberger, B.: History and basic features of the critical pair/completion procedure. Journal of Symbolic Computation 3, 3–38 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  • Bündgen, R.: Buchberger’s algorithm: The term rewriter’s point of view. Theoretical Computer Science 159, 143–190 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  • Contejean, E., Marché, C.: CiME: Completion modulo E. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 18–32. Springer, Heidelberg (1996)

    Google Scholar 

  • Delor, C., Puel, L.: Extension of the associative path ordering to a chain of associative commutative symbols. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690, pp. 389–404. Springer, Heidelberg (1993)

    Google Scholar 

  • Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science: Formal Models and Semantics, ch. 6, vol. B, pp. 243–320. Elsevier/MIT Press (1990)

    Google Scholar 

  • Ganzinger, H., Waldmann, U.: Theorem proving in cancellative abelian monoids (extended abstract). In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol. 1104, pp. 388–402. Springer, Heidelberg (1996)

    Google Scholar 

  • Godoy, G., Nieuwenhuis, R.: Paramodulation with built-in abelian groups. To appear in LICS (2000)

    Google Scholar 

  • Greendlinger, M.: Dehn’s algorithm for the word problem. Communications on Pure and Applied Mathematics 13, 67–83 (1960)

    Article  MATH  MathSciNet  Google Scholar 

  • Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM Journal on Computing 15(4), 1155–1194 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  • Kandri-Rody, A., Kapur, D.: Computing a Gröbner basis of a polynomial ideal over a Euclidean domain. Journal of Symbolic Computation 6, 19–36 (1988)

    Article  MathSciNet  Google Scholar 

  • Le Chenadec, P.: Canonical Forms in Finitely Presented Algebras. Pitman, London (1986)

    MATH  Google Scholar 

  • Marché, C.: Normalised rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation 21, 253–288 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  • Nieuwenhuis, R., Rubio, A.: Paramodulation with built-in AC-theories and symbolic constraints. Journal of Symbolic Computation 23, 1–21 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  • Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. Journal of the ACM 28(2), 233–264 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  • Stuber, J.: Superposition theorem proving for abelian groups represented as integer modules. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 33–47. Springer, Heidelberg (1996)

    Google Scholar 

  • Stuber, J.: Strong symmetrization, semi-compatibility of normalized rewriting and first-order theorem proving. In: Bonacina, M.P., Furbach, U. (eds.) Proc. Int. Workshop on First-Order Theorem Proving. RISC-Linz Report 97-50, Research Institute for Symbolic Computation, Linz, Austria, pp. 125–129 (1997)

    Google Scholar 

  • Stuber, J.: Superposition theorem proving for abelian groups represented as integer modules. Theoretical Computer Science 208(1-2), 149–177 (1998a)

    Article  MATH  MathSciNet  Google Scholar 

  • Stuber, J.: Superposition theorem proving for commutative rings. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction - A Basis for Applications. ch. 2, Applications, vol. III, pp. 31–55. Kluwer, Dordrecht (1998b)

    Google Scholar 

  • Stuber, J.: Superposition Theorem Proving for Commutative Algebraic Theories. Dissertation, Technische Fakultät, Universität des Saarlandes, Saarbrücken. (1999a) (submitted)

    Google Scholar 

  • Stuber, J.: Theory path orderings. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 148–162. Springer, Heidelberg (1999b)

    Chapter  Google Scholar 

  • Vigneron, L.: Associative-commutative deduction with constraints. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 530–544. Springer, Heidelberg (1994)

    Google Scholar 

  • Waldmann, U.: Cancellative Abelian Monoids in Refutational Theorem Proving. Dissertation, Universität des Saarlandes, Saarbrücken (1997)

    Google Scholar 

  • Waldmann, U.: Superposition for divisible torsion-free abelian groups. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 144–159. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  • Wertz, U.: First-order theorem proving modulo equations. Technical Report MPI-I-92-216, Max-Planck-Institut für Informatik, Saarbrücken (1992)

    Google Scholar 

  • Zhang, H.: A case study of completion modulo distributivity and abelian groups. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690, pp. 32–46. Springer, Heidelberg (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Jürgen Stuber

Authors
  1. Jürgen Stuber
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Stony Brook University, Stony Brook, P.O. Box, New York

    Leo Bachmair

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Stuber, J. (2000). Deriving Theory Superposition Calculi from Convergent Term Rewriting Systems. In: Bachmair, L. (eds) Rewriting Techniques and Applications. RTA 2000. Lecture Notes in Computer Science, vol 1833. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721975_16

Download citation

  • DOI: https://doi.org/10.1007/10721975_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67778-9

  • Online ISBN: 978-3-540-44980-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation