Abstract
This paper describes two advancements of SAT-based Knuth-Bendix completion as implemented in Maxcomp. (1) Termination techniques using the dependency pair framework are encoded as satisfiability problems, including dependency graph and reduction pair processors. (2) Instead of relying on pure maximal completion, different SAT-encoded control strategies are exploited.
Experiments show that these developments let Maxcomp improve over other automatic completion tools, and produce novel complete systems.
This research was supported by the Austrian Science Fund project I963.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. JAR 40(2–3), 195–220 (2008)
Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair 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)
Klein, D., Hirokawa, N.: Maximal completion. In: RTA, vol. 10 of LIPIcs, pp. 71–80 (2011)
Korovin, K.: Inst-Gen – a modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 239–270. Springer, Heidelberg (2013)
Sato, H., Winkler, S.: A satisfiability encoding of dependency pair techniques for maximal completion. In: WST (2014)
Schneider-Kamp, P., Thiemann, R., Annov, E., Codish, M., Giesl, J.: Proving termination using recursive path orders and SAT solving. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 267–282. Springer, Heidelberg (2007)
Sternagel, T., Zankl, H.: KBCV – Knuth-Bendix Completion Visualizer. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 530–536. Springer, Heidelberg (2012)
Stump, A., Löchner, B.: Knuth-Bendix completion of theories of commuting group endomorphisms. IPL 98(5), 195–198 (2006)
Wehrman, I., Stump, A., Westbrook, E.: Slothrop: knuth-bendix completion with a modern termination checker. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 287–296. Springer, Heidelberg (2006)
Winkler, S., Sato, H., Middeldorp, A., Kurihara, M.: Multi-completion with termination tools. JAR 50(3), 317–354 (2013)
Yamada, A., Kusakari, K., Sakabe, T.: A unified ordering for termination proving. Science of Computer Programming (2014). doi:10.1016/j.scico.2014.07.009
Zankl, H., Hirokawa, N., Middeldorp, A.: 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. LNCS, vol. 4362, pp. 579–590. Springer, Heidelberg (2007)
Zankl, H., Hirokawa, N., Middeldorp, A.: KBO orientability. JAR 43(2), 173–201 (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Sato, H., Winkler, S. (2015). Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion. In: Felty, A., Middeldorp, A. (eds) Automated Deduction - CADE-25. CADE 2015. Lecture Notes in Computer Science(), vol 9195. Springer, Cham. https://doi.org/10.1007/978-3-319-21401-6_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-21401-6_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-21400-9
Online ISBN: 978-3-319-21401-6
eBook Packages: Computer ScienceComputer Science (R0)