[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Constraints for Argument Filterings

  • Conference paper
SOFSEM 2007: Theory and Practice of Computer Science (SOFSEM 2007)

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

  • 1735 Accesses

Abstract

The dependency pair method is a powerful method for automatically proving termination of rewrite systems. When used with traditional simplification orders like LPO and KBO, argument filterings play a key role. In this paper we propose an encoding of argument filterings in propositional logic. By incorporating propositional encodings of simplification orders, the search for suitable argument filterings is turned into a satisfiability problem. Preliminary experimental results show that our logic-based approach is significantly faster than existing implementations.

This research is supported by FWF (Austrian Science Fund) project P18763. Some of the results in this paper were first announced in [14].

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. Arts, T., Giesl, J.: Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science 236, 133–178 (2000)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  3. Codish, M., Lagoon, V., Stuckey, P.J.: 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 

  4. Codish, M., Schneider-Kamp, P., Lagoon, V., Thiemann, R., Giesl, J.: Automating Dependency Pairs Using SAT Solvers. In: Proc. of the 8th International Workshop on Termination (2006), Extended version to appear in Proc. of the 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LNCS

    Google Scholar 

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

  6. Giesl, J., Arts, T., Ohlebusch, E.: Modular Termination Proofs for Rewriting Using Dependency Pairs. Journal of Symbolic Computation 34(1), 21–58 (2002)

    Article  MathSciNet  Google Scholar 

  7. Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  8. Hirokawa, N., Middeldorp, A.: Dependency Pairs Revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 249–268. Springer, Heidelberg (2004)

    Google Scholar 

  9. Hirokawa, N., Middeldorp, A.: Automating the Dependency Pair Method. Information and Computation 199(1-2), 172–199 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  10. Hirokawa, N., Middeldorp, A.: Tyrolean Termination Tool. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 175–184. Springer, Heidelberg (2005)

    Google Scholar 

  11. Kurihara, M., Kondo, H.: Efficient BDD Encodings for Partial Order Constraints with Application to Expert Systems in Software Verification. In: Orchard, B., Yang, C., Ali, M. (eds.) IEA/AIE 2004. LNCS (LNAI), vol. 3029, pp. 827–837. Springer, Heidelberg (2004)

    Google Scholar 

  12. Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved Modular Termination Proofs Using Dependency Pairs. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 75–90. Springer, Heidelberg (2004)

    Google Scholar 

  13. Zankl, H.: BDD and SAT Techniques for Precedence Based Orders. Master’s Thesis, University of Innsbruck (2006), Available at http://cl-informatik.uibk.ac.at/HZ.pdf

  14. Zankl, H., Hirokawa, N., Middeldorp, A.: Constraints for Argument Filterings. In: Proc. of the 8th International Workshop on Termination, pp. 50–54 (2006)

    Google Scholar 

  15. Zankl, H., Middeldorp, A.: KBO as a Satisfaction Problem. In: Proc. of the 8th International Workshop on Termination, pp. 55–59 (2006), Full version available at http://arxiv.org/abs/cs.SC/0608032

Download references

Author information

Authors and Affiliations

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

    Harald Zankl, Nao Hirokawa & Aart Middeldorp

Authors
  1. Harald Zankl
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nao Hirokawa
    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

Editor information

Jan van Leeuwen Giuseppe F. Italiano Wiebe van der Hoek Christoph Meinel Harald Sack František Plášil

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer Berlin Heidelberg

About this paper

Cite this paper

Zankl, H., Hirokawa, N., Middeldorp, A. (2007). Constraints for Argument Filterings. In: van Leeuwen, J., Italiano, G.F., van der Hoek, W., Meinel, C., Sack, H., Plášil, F. (eds) SOFSEM 2007: Theory and Practice of Computer Science. SOFSEM 2007. Lecture Notes in Computer Science, vol 4362. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69507-3_50

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-69507-3_50

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-69506-6

  • Online ISBN: 978-3-540-69507-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation