Skip to main content
SpringerLink
Log in

SAT Solving for Termination Analysis with Polynomial Interpretations

  • Conference paper
Theory and Applications of Satisfiability Testing – SAT 2007 (SAT 2007)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4501))

Abstract

Polynomial interpretations are one of the most popular techniques for automated termination analysis and the search for such interpretations is a main bottleneck in most termination provers. We show that one can obtain speedups in orders of magnitude by encoding this task as a SAT problem and by applying modern SAT solvers.

Supported by the DFG (Deutsche Forschungsgemeinschaft) grant GI 274/5-1 and the FWF (Austrian Science Fund) project P18763.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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. Annov, E., et al.: A SAT-based implementation for RPO termination. In: Short Papers of LPAR ’06 (2006)

    Google Scholar 

  2. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  3. Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using dependency pairs. Technical Report AIB-2001-09, RWTH Aachen (2001)

    Google Scholar 

  4. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge (1998)

    Google Scholar 

  5. Codish, M., Lagoon, V., Stuckey, P.: Solving partial order constraints for LPO termination. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 4–18. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  6. Codish, M., et al.: SAT solving for argument filterings. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 30–44. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  7. Contejean, E., et al.: CiME, http://cime.lri.fr

  8. Contejean, E., et al.: Mechanically proving termination using polynomial interpretations. J. Aut. Reason. 34(4), 325–363 (2005)

    Article  MATH  Google Scholar 

  9. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Google Scholar 

  10. Empirical evaluation of “SAT solving for termination analysis with polynomial interpretations”, http://aprove.informatik.rwth-aachen.de/eval/SATPOLO

  11. Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 574–588. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  12. Giesl, J., Thiemann, R., Schneider-Kamp, P.: The DP framework: Combining Techniques for Automated Termination Proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 301–331. Springer, Heidelberg (2005)

    Google Scholar 

  13. Giesl, J., et al.: Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 297–312. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the DP framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  15. Giesl, J., et al.: Mechanizing and improv- ing dependency pairs. Journal of Automated Reasoning 37(3), 155–203 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  16. Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Information and Computation 199(1-2), 172–199 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  17. Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: Techniques and features. Information and Computation 205(4), 474–511 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  18. Hofbauer, D., Waldmann, J.: Termination of string rewriting with matrix interpretations. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 328–342. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Hong, H., Jakuš, D.: Testing positiveness of polynomials. JAR 21(1), 23–38 (1998)

    Article  Google Scholar 

  20. Lankford, D.: On proving term rewriting systems are Noetherian. Technical Report MTP-3, Louisiana Technical University, Ruston, LA, USA (1979)

    Google Scholar 

  21. Le Berre, D., et al.: SAT4J satisfiability library for Java, http://www.sat4j.org

  22. Giesl, J., et al.: Automated Termination Analysis for Logic Programs by Term Rewriting. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 177–193. Springer, Heidelberg (2007)

    Google Scholar 

  23. Sheini, H.M., Sakallah, K.A.: Pueblo: A hybrid pseudo-boolean SAT solver. Journal on Satisfiability, Boolean Modeling and Computation 2, 61–96 (2006)

    Google Scholar 

  24. Tseitin, G.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, pp. 115–125 (1968)

    Google Scholar 

  25. Zankl, H., Hirokawa, N., Middeldorp, A.: Constraints for argument filterings. In: van Leeuwen, J., et al. (eds.) SOFSEM 2007. LNCS, vol. 4362, pp. 579–590. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  26. Zankl, H., Middeldorp, A.: KBO as a satisfaction problem. In: Proc. WST’06 (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LuFG Informatik 2, RWTH Aachen, Germany

    Carsten Fuhs, Jürgen Giesl, Peter Schneider-Kamp & René Thiemann

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

    Aart Middeldorp & Harald Zankl

Authors
  1. Carsten Fuhs
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jürgen Giesl
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Aart Middeldorp
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Peter Schneider-Kamp
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. René Thiemann
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Harald Zankl
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

João Marques-Silva Karem A. Sakallah

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer Berlin Heidelberg

About this paper

Cite this paper

Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H. (2007). SAT Solving for Termination Analysis with Polynomial Interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds) Theory and Applications of Satisfiability Testing – SAT 2007. SAT 2007. Lecture Notes in Computer Science, vol 4501. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72788-0_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-72788-0_33

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-72787-3

  • Online ISBN: 978-3-540-72788-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation