[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Superposition and Chaining for Totally Ordered Divisible Abelian Groups

Extended Abstract

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2001)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2083))

Included in the following conference series:

  • 815 Accesses

Abstract

We present a calculus for first-order theorem proving in the presence of the axioms of totally ordered divisible abelian groups. The calculus extends previous superposition or chaining calculi for divisible torsion-free abelian groups and dense total orderings without endpoints. As its predecessors, it is refutationally complete and requires neither explicit inferences with the theory axioms nor variable overlaps. It offers thus an efficient way of treating equalities and inequalities between additive terms over, e. g., the rational numbers within a first-order theorem prover.

Acknowledgments

I would like to thank the anonymous IJCAR referees for helpful comments on this paper.

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.

Similar content being viewed by others

References

  1. 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.

    Chapter  Google Scholar 

  2. Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.

    Article  MathSciNet  MATH  Google Scholar 

  3. Leo Bachmair and Harald Ganzinger. Ordered chaining calculi for first-order theories of transitive relations. Journal of the ACM, 45(6):1007–1049, November 1998.

    Article  MathSciNet  MATH  Google Scholar 

  4. 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.

    Google Scholar 

  5. Claude Marché. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 21(3):253–288, March 1996.

    Article  MathSciNet  MATH  Google Scholar 

  6. James R. Slagle. Automatic theorem proving with built-in theories including equality, partial ordering, and sets. Journal of the ACM, 19(1):120–135, January 1972.

    Article  MathSciNet  MATH  Google Scholar 

  7. Jürgen Stuber. Superposition theorem proving for abelian groups represented as integer modules. In Harald Ganzinger, ed., Rewriting Techniques and Applications, 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996, LNCS 1103, pp. 33–47. Springer-Verlag.

    Chapter  Google Scholar 

  8. 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.

    Google Scholar 

  9. Uwe Waldmann. Extending reduction orderings to ACU-compatible reduction orderings. Information Processing Letters, 67(1):43–49, July 16, 1998.

    Article  MathSciNet  Google Scholar 

  10. 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.

    Google Scholar 

  11. Uwe Waldmann. Superposition and chaining for totally ordered divisible abelian groups. Technical Report MPI-I-2001-2-001, Max-Planck-Institut für Informatik, Saarbrücken, Germany, 2001.

    Book  Google Scholar 

  12. 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.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Max-Planck-Institut für Informatik, Stuhlsatzenhausweg 85, 66123, Saarbrücken, Germany

    Uwe Waldmann

Authors
  1. Uwe Waldmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Automated Reasoning Project and Department of Computer Science, Australian National University, Canberra, ACT, 0200, Australia

    Rajeev Goré

  2. AG Theoretische Informatik und Logik, Institut für Computersprachen, Technische Universität Wien, Favoritenstr. 9, E185-2, 1040, Wien, Austria

    Alexander Leitsch

  3. Institut für Informatik, Technische Universität München, 80290, München, Germany

    Tobias Nipkow

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Waldmann, U. (2001). Superposition and Chaining for Totally Ordered Divisible Abelian Groups. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_17

Download citation

  • DOI: https://doi.org/10.1007/3-540-45744-5_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-45744-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics