Abstract
Commutative rings are very common both in mathematics and in computer science, as they encompass the basic algebraic properties of addition, subtraction and multiplication for numbers like the integers or the reals. The problem with commutative rings and similar algebraic theories is that their axioms create large search spaces for theorem provers. We address this problem by systematically developing a superposition calculus for first-order problems that contain the theory of commutative rings. The calculus combines certain uses of the axioms into macro inferences, and it restricts inferences to the maximal term within a sum. Thereby it promises to make theorem proving with respect to commutative rings more efficient.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bachmair, L. and H. Ganzinger: 1994, `Associative-Commutative Superposition’. In: N. Dershowitz and N. Lindenstrauss (eds.): Proc. 4th Int. Workshop on Conditional and Typed Rewriting, Vol. 968 of Lecture Notes in Computer Science. Jerusalem, pp. 1–14, Springer. Revised version of TR MPI-I-93–267, 1993.
Boyer, R. S. and J. S. Moore: 1988, `Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic’. In: J. E. Hayes, D. Michie, and J. Richards (eds.): Machine Intelligence 11. Oxford: Clarendon Press, Chapt. 5, pp. 83–124.
Buchberger, B. and R. Loos: 1983, `Algebraic Simplification’. In: Computer Algebra: Symbolic and Algebraic Computation. Springer, 2nd edition, pp. 11–43.
Bündgen, R.: 1996, `Buchberger’s algorithm: The term rewriter’s point of view’. Theoretical Computer Science 159, 143–190.
Contejean, E. and C. Marché: 1996, ‘CiME: Completion Modulo E’. In: H. Ganzinger (ed.): Proc. 7th Int. Conf on Rewriting Techniques and Applications, Vol. 1103 of Lecture Notes in Computer Science. New Brunswick, NJ, USA, pp. 18–32, Springer.
Delor, C. and L. Puel: 1993, `Extension of the associative path ordering to a chain of associative commutative symbols’. In: Proc. 5th Int. Conf. on Rewriting Techniques and Applications, Vol. 690 of Lecture Notes in Computer Science. Montreal, pp. 389–404, Springer.
Dershowitz, N.: 1987, `Termination of Rewriting’. Journal of Symbolic Computation 3, 69–116.
Ganzinger, H. and U. Waldmann: 1996, `Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)’. In: M. A. McRobbie and J. K. Slaney (eds.): 13th Int. Conf. on Automated Deduction, Vol. 1104 of Lecture Notes in Artificial Intelligence. New Brunswick, NJ, USA, pp. 388–402, Springer.
Greendlinger, M.: 1960, `Dehn’s algorithm for the word problem’. Communications on Pure and Applied Mathematics 13, 67–83.
Jouannaud, J.-P. and H. Kirchner: 1986, `Completion of a set of rules modulo a set of equations’. SIAM Journal on Computing 15 (4), 1155–1194.
Le Chenadec, P.: 1986, Canonical Forms in Finitely Presented Algebras. London: Pitman.
Marché, C.: 1996, `Normalised Rewriting: an Alternative to Rewriting modulo a Set of Equations’. Journal of Symbolic Computation 21, 253–288.
Peterson, G. E. and M. E. Stickel: 1981, `Complete Sets of Reductions for Some Equational Theories’. Journal of the ACM 28 (2), 233–264.
Rubio, A. and R. Nieuwenhuis: 1993, `A precedence-based total AC-compatible ordering’. In: C. Kirchner (ed.): Proc. 5th Int. Conf. on Rewriting Techniques and Applications, Vol. 690 of Lecture Notes in Computer Science. Montreal, pp. 374–388, Springer.
Stickel, M. E.: 1985, `Automated Deduction by Theory Resolution’. Journal of Automated Reasoning 1 (4), 333–355.
Stuber, J.: 1996, `Superposition Theorem Proving for Abelian Groups Represented as Integer Modules’. In: H. Ganzinger (ed.): Proc. 7th Int. Conf. on Rewriting Techniques and Applications, Vol. 1103 of Lecture Notes in Computer Science. New Brunswick, NJ, USA, pp. 33–47, Springer.
Waldmann, U.: 1997, `A Superposition Calculus for Divisible Torsion-Free Abelian Groups’. In: M. P. Bonacina and U. Furbach (eds.): Int. Workshop on First-Order Theorem Proving. Schloß Hagenberg, Linz, Austria, pp. 130–134, Johannes Kepler Universität, Linz, Austria.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Stuber, J. (1998). Superposition Theorem Proving for Commutative Rings. In: Bibel, W., Schmitt, P.H. (eds) Automated Deduction — A Basis for Applications. Applied Logic Series, vol 10. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0437-3_2
Download citation
DOI: https://doi.org/10.1007/978-94-017-0437-3_2
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5052-6
Online ISBN: 978-94-017-0437-3
eBook Packages: Springer Book Archive