Abstract
In divisible torsion-free abelian groups, the efficiency of the cancellative superposition calculus can be greatly increased by combining it with a variable elimination algorithm that transforms every clause into an equivalent clause without unshielded variables. We show that the resulting calculus is not only refutationally complete (even in the presence of arbitrary free function symbols), but that it is also a decision procedure for the theory of divisible torsion-free abelian groups.
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
Leo Bachmair and Harald Ganzinger. Associative-commutative superposition. In Nachum Dershowitz and Naomi Lindenstrauss, eds., Conditional and Typed Rewriting Systems, 4th International Workshop, CTRS-94, Jerusalem, Israel, July 13–15, 1994, LNCS 968, pp. 1–14. Springer-Verlag.
Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.
Leo Bachmair, Harald Ganzinger, and Uwe Waldmann. Superposition with simplification as a decision procedure for the monadic class with equality. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, eds., Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, Brno, Czech Republic, August 24–27, 1993, LNCS 713, pp. 83–96. Springer-Verlag.
Leo Bachmair, Harald Ganzinger, and Uwe Waldmann. Refutational theorem proving for hierarchic first-order theories. Applicable Algebra in Engineering, Communication and Computing, 5(3/4):193–212, April 1994.
E[dward] Cardoza, R[ichard] Lipton, and A[lbert] R. Meyer. Exponential space complete problems for petri nets and commutative semigroups: Preliminary report. In Eighth Annual ACM Symposium on Theory of Computing, Hershey, PA, USA, May 3–5, 1976, pp. 50–54.
C[hristian] Fermüller, A[lexander] Leitsch, Tanel Tammet, and Nail Zamov. Resolution Methods for the Decision Problem. LNAI 679. Springer-Verlag, Berlin, Heidelberg, New York, 1993.
Christian Fermüller and Gernot Salzer. Ordered paramodulation and resolution as decision procedure. In Andrei Voronkov, ed., Logic Programming and Automated Reasoning, 4th International Conference, LPAR’93, St. Petersburg, Russia, July 13–20, 1993, LNCS 698, pp. 122–133. Springer-Verlag.
Harald Ganzinger and Hans de Nivelle. A superposition decision procedure for the guarded fragment with equality. In Fourteenth Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2–5, 1999, pp. 295–303. IEEE Computer Society Press.
Harald Ganzinger, Ullrich Hustadt, Christoph Meyer, and Renate Schmidt. A resolution-based decision procedure for extensions of K4. In Advances in Modal Logic’ 98, 1998. To appear.
Harald Ganzinger and Uwe Waldmann. Theorem proving in cancellative abelian monoids (extended abstract). In Michael A. McRobbie and John K. Slaney, eds., Automated Deduction — CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30–August 3, 1996, LNAI 1104, pp. 388–402. Springer-Verlag.
William H. Joyner Jr. Resolution strategies as decision procedures. Journal of the ACM, 23(3):398–417, July 1976.
Ernst W. Mayr and Albert R. Meyer. The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in Mathematics, 46(3):305–329, December 1982.
Etienne Paul. A general refutational completeness result for an inference procedure based on associative-commutative unification. Journal of Symbolic Computation, 14(6):577–618, December 1992.
Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28(2):233–264, April 1981.
Gordon D. Plotkin. Building-in equational theories. In Bernard Meltzer and Donald Michie, eds., Machine Intelligence 7, ch. 4, pp. 73–90. American Elsevier, New York, NY, USA, 1972.
Michaël Rusinowitch and Laurent Vigneron. Automated deduction with associative-commutative operators. Applicable Algebra in Engineering, Communication and Computing, 6(1):23–56, January 1995.
James R. Slagle. Automated theorem-proving for theories with simplifiers, commutativity, and associativity. Journal of the ACM, 21(4):622–642, October 1974.
Uwe Waldmann. Cancellative Abelian Monoids in Refutational Theorem Proving. Dissertation, Universität des Saarlandes, Saarbrücken, Germany, 1997. http://www.mpi-sb.mpg.de/~uwe/paper/PhD.ps.gz.
Uwe Waldmann. Extending reduction orderings to ACU-compatible reduction orderings. Information Processing Letters, 67(1):43–49, July 16, 1998.
Uwe Waldmann. Superposition for divisible torsion-free abelian groups. In Claude Kirchner and Hélène Kirchner, eds., Automated Deduction — CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5–10, 1998, LNAI 1421, pp. 144–159. Springer-Verlag.
Ulrich Wertz. First-order theorem proving modulo equations. Technical Report MPI-I-92-216, Max-Planck-Institut für Informatik, Saarbrücken, Germany, April 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Waldmann, U. (1999). Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds) Logic for Programming and Automated Reasoning. LPAR 1999. Lecture Notes in Computer Science(), vol 1705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48242-3_9
Download citation
DOI: https://doi.org/10.1007/3-540-48242-3_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66492-5
Online ISBN: 978-3-540-48242-0
eBook Packages: Springer Book Archive