Skip to main content
SpringerLink
Log in

Termination Tools in Ordered Completion

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

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

Included in the following conference series:

Abstract

Ordered completion is one of the most frequently used calculi in equational theorem proving. The performance of an ordered completion run strongly depends on the reduction order supplied as input. This paper describes how termination tools can replace fixed reduction orders in ordered completion procedures, thus allowing for a novel degree of automation. Our method can be combined with the multi-completion approach proposed by Kondo and Kurihara. We present experimental results obtained with our ordered completion tool omkb TT for both ordered completion and equational theorem proving.

This research is supported by FWF (Austrian Science Fund) project P18763. The first author is supported by a DOC-fFORTE fellowship of the Austrian Academy of Sciences.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

  1. Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. Journal of the ACM 41(2), 236–276 (1994)

    Article  MathSciNet  Google Scholar 

  2. Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Aït-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures. Rewriting Techniques of Progress in Theoretical Computer Science, vol. 2, pp. 1–30. Academic Press, London (1989)

    Google Scholar 

  3. Bofill, M., Godoy, G., Nieuwenhuis, R., Rubio, A.: Paramodulation and Knuth–Bendix completion with nontotal and nonmonotonic orderings. Journal of Automated Reasoning 30(1), 99–120 (2003)

    Article  MathSciNet  Google Scholar 

  4. Dershowitz, N.: Orderings for term rewriting systems. Theoretical Computer Science 17(3), 279–301 (1982)

    Article  MathSciNet  Google Scholar 

  5. Hillenbrand, T., Löchner, B.: The next Waldmeister loop. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 486–500. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  6. Kamin, S., Lévy, J.J.: Two generalizations of the recursive path ordering. University of Illinois, US (1980) (unpublished manuscript)

    Google Scholar 

  7. Knuth, D.E., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)

    Google Scholar 

  8. Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295–304. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  9. Kurihara, M., Kondo, H.: Completion for multiple reduction orderings. Journal of Automated Reasoning 23(1), 25–42 (1999)

    Article  MathSciNet  Google Scholar 

  10. Lankford, D.: On proving term rewrite systems are noetherian. Technical Report MTP-3, Louisiana Technical University (1979)

    Google Scholar 

  11. Sato, H., Winkler, S., Kurihara, M., Middeldorp, A.: Multi-completion with termination tools (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 306–312. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Sato, H., Winkler, S., Kurihara, M., Middeldorp, A.: Constraint-based multi-completion procedures for term rewriting systems. IEICE Transactions on Electronics, Information and Communication Engineers E92-D(2), 220–234 (2009)

    Google Scholar 

  13. Schulz, S.: The E Equational Theorem Prover (2009), http://www.eprover.org

  14. Sutcliffe, G.: The TPTP problem library and associated infrastructure. Journal of Automated Reasoning 43(4), 337–362 (2009)

    Article  Google Scholar 

  15. Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  16. Wehrman, I., Stump, A., Westbrook, E.M.: Slothrop: Knuth-Bendix completion with a modern termination checker. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 287–296. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  17. Winkler, S., Sato, H., Middeldorp, A., Kurihara, M.: Optimizing mkbTT (System description). In: Lynch, C. (ed.) Proc. 21st RTA. LIPIcs (to appear, 2010)

    Google Scholar 

  18. Zantema, H.: Total termination of term rewriting is undecidable. Journal of Symbolic Computation 20(1), 43–60 (1995)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, University of Innsbruck, Austria

    Sarah Winkler & Aart Middeldorp

Authors
  1. Sarah Winkler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Aart Middeldorp
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. RWTH Aachen, LuFG Informatik, 2, Ahornstr. 55, 52074, Aachen, Germany

    Jürgen Giesl

  2. Department of Computer Science, Chalmers University of Technology, 41296, Gothenburg, Sweden

    Reiner Hähnle

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Winkler, S., Middeldorp, A. (2010). Termination Tools in Ordered Completion. In: Giesl, J., Hähnle, R. (eds) Automated Reasoning. IJCAR 2010. Lecture Notes in Computer Science(), vol 6173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14203-1_43

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14203-1_43

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14202-4

  • Online ISBN: 978-3-642-14203-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation