Abstract
We define a superposition calculus specialized for abelian groups represented as integer modules, and show its refutational completeness. This allows to substantially reduce the number of inferences compared to a standard superposition prover which applies the axioms directly. Specifically, equational literals are simplified, so that only the maximal term of the sums is on the left-hand side. Only certain minimal superpositions need to be considered; other superpositions which a standard prover would consider become redundant. This not only reduces the number of inferences, but also reduces the size of the AC-unification problems which are generated. That is, AC-unification is not necessary at the top of a term, only below some non-AC-symbol. Further, we consider situations where the axioms give rise to variable overlaps and develop techniques to avoid these explosive cases where possible.
Proofs are available at http://www.mpi-sb.mpg.de/∼juergen/publications/RTA96/.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Bachmair, L. and Ganzinger, H. (1994a). Associative-commutative superposition. In Proc. 4th Int. Workshop on Conditional and Typed Rewriting, Jerusalem, LNCS 968, pp. 1–14. Springer.
Bachmair, L. and Ganzinger, H. (1994b). Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation4(3): 217–247.
Bachmair, L. and Ganzinger, H. (1994c). Rewrite techniques for transitive relations. In Proc. 9th Ann. IEEE Symp. on Logic in Computer Science, Paris, pp. 384–393.
Bachmair, L., Ganzinger, H. and Stuber, J. (1995). Combining algebra and universal algebra in first-order theorem proving: The case of commutative rings. In Proc. 10th Workshop on Specification of Abstract Data Types, Santa Margherita, Italy, LNCS 906.
Bachmair, L., Ganzinger, H., Lynch, C. and Snyder, W. (1993). Basic paramodulation. Technical Report MPI-I-93-236, Max-Planck-Institut für Informatik, Saarbrücken.
Boudet, A., Contejean, E. and Marché, C. (1996). AC-complete unification and its application to theorem proving. This volume.
Boyer, R. S. and Moore, J. S. (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, pp. 83–124. Clarendon Press, Oxford.
Dershowitz, N. and Jouannaud, J.-P. (1990). Rewrite systems. In J. van Leeuwen (ed.), Handbook of Theoretical Computer Science: Formal Models and Semantics, Vol. B, chapter 6, pp. 243–320. Elsevier/MIT Press.
Fitting, M. (1990). First-Order Logic and Automated Theorem Proving. Springer.
Ganzinger, H. and Waldmann, U. (1996). Theorem proving in cancellative abelian monoids. Technical Report MPI-I-96-2-001, Max-Planck-Institut für Informatik, Saarbrücken, Germany.
Jouannaud, J.-P. and Kirchner, H. (1986). Completion of a set of rules modulo a set of equations. SIAM Journal on Computing15(4): 1155–1194.
Kandri-Rody, A. and Kapur, D. (1988). Computing a Gröbner basis of a polynomial ideal over a euclidean domain. Journal of Symbolic Computation6: 19–36.
Kirchner, C., Kirchner, H. and Rusinowitch, M. (1990). Deduction with symbolic constraints. Revue Française d'Intelligence Artificielle4(3): 9–52.
Le Chenadec, P. (1984). Canonical forms in finitely presented algebras. In Proc. 7th Int. Conf. on Automated Deduction, Napa, CA, LNCS 170, pp. 142–165. Springer. Book version published by Pitman, Londons, 1986.
Marché, C. (1994). Normalised rewriting and normalised completion. In Proc. 9th Symp. on Logic in Computer Science, Paris, pp. 394–403. IEEE Computer Society Press.
Nieuwenhuis, R. and Rubio, A. (1992). Theorem proving with ordering constrained clauses. In 11th International Conference on Automated Deduction, Saratoga Springs, NY, LNCS 607, pp. 477–491. Springer.
Nieuwenhuis, R. and Rubio, A. (1994). AC-superposition with constraints: no AC-unifiers needed. In Proc. 12th Int. Conf. on Automated Deduction, Nancy, France, LNCS 814, pp. 545–559. Springer.
Vigneron, L. (1994). Associative-commutative deduction with constraints. In Proc. 12th Int. Conf. on Automated Deduction, Nancy, France, LNCS 814, pp. 530–544. Springer.
Wang, T. C. (1988). Elements of Z-module reasoning. In Proc. 9th Int. Conf. on Automated Deduction, Argonne, LNCS 310, pp. 21–40. Springer.
Wertz, U. (1992). First-order theorem proving modulo equations. Technical Report MPI-I-92-216, Max-Planck-Institut für Informatik, Saarbrücken.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stuber, J. (1996). Superposition theorem proving for abelian groups represented as integer modules. In: Ganzinger, H. (eds) Rewriting Techniques and Applications. RTA 1996. Lecture Notes in Computer Science, vol 1103. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61464-8_41
Download citation
DOI: https://doi.org/10.1007/3-540-61464-8_41
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61464-7
Online ISBN: 978-3-540-68596-8
eBook Packages: Springer Book Archive