Abstract
This article presents three new approaches to prove termination of rewrite systems with the Knuth–Bendix order efficiently. The constraints for the weight function and for the precedence are encoded in (pseudo-)propositional logic or linear arithmetic and the resulting formula is tested for satisfiability using dedicated solvers. Any satisfying assignment represents a weight function and a precedence such that the induced Knuth–Bendix order orients the rules of the encoded rewrite system from left to right. This means that in contrast to the dedicated methods our approach does not directly solve the problem but transforms it to equivalent formulations for which sophisticated back-ends exist. In order to make all approaches complete we present a method to compute upper bounds on the weights. Furthermore, our encodings take dependency pairs into account to increase the applicability of the order.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Codish, M., Lagoon, V., Stuckey, P.: Solving partial order constraints for LPO termination. In: Proc. 17th International Conference on Rewriting Techniques and Applications. LNCS, vol. 4098, pp. 4–18 (2006)
Codish, M., Schneider-Kamp, P., Lagoon, V., Thiemann, R., Giesl, J.: SAT solving for argument filterings. In: Proc. 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. LNAI, vol. 4246, pp. 30–44 (2006)
Danzig, G.: Linear Programming and Extensions. Princeton University Press, Princeton (1963)
Dershowitz, N.: Termination by abstraction. In: Proc. 20th International Conference on Logic Programming. LNCS, vol. 3132, pp. 1–18 (2004)
Dick, J., Kalmus, J., Martin, U.: Automating the Knuth–Bendix ordering. Acta Inform. 28, 95–119 (1990)
Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Proc. 18th International Conference on Computer Aided Verification. LNCS, vol. 4144, pp. 81–94 (2006)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Proc. 6th International Conference on Theory and Applications of Satisfiability Testing. LNCS, vol. 2919, pp. 502–518 (2004)
Eén, N., Sörensson, N.: Translating pseudo-boolean constraints into SAT. J. Satisfiab Boolean Model Comput. 2, 1–26 (2006)
Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reason. 40(2–3), 195–220 (2008)
Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Proc. 10th International Conference on Theory and Applications of Satisfiability Testing. LNCS, vol. 4501, pp. 340–354 (2007)
Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: Maximal termination. In: Proc. 19th International Conference on Rewriting Techniques and Applications. LNCS, vol. 5117, pp. 110–125 (2008)
Fuhs, C., Navarro-Marset, R., Otto, C., Giesl, J., Lucas, S., Schneider-Kamp, P.: Search techniques for rational polynomial orders. In: Proc. 9th International Conference on Artificial Intelligence and Symbolic Computation. LNAI, vol. 5144, pp. 109–124 (2008)
Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Proc. 3rd International Joint Conference on Automated Reasoning. LNAI, vol. 4130, pp. 281–286 (2006)
Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: combining techniques for automated termination proofs. In: Proc. 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. LNAI, vol. 3452, pp. 301–331 (2005)
Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Proc. 5th International Workshop on Frontiers of Combining Systems. LNAI, vol. 3717, pp. 216–231 (2005)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reason. 37(3), 155–203 (2006)
Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Inf. Comput. 199(1–2), 172–199 (2005)
Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: techniques and features. Inf. Comput. 205(4), 474–511 (2007)
Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations (preliminary version). In: Proc. 3rd International Conference on Rewriting Techniques and Applications. LNCS, vol. 355, pp. 167–177 (1989)
Karmarkar, N.: A new polynomial-time algorithm for linear programming. Combinatorica 4, 373–395 (1984)
Khachiyan, L.: A polynomial algorithm in linear programming. Dokl. Akad. Nauk SSSR 244, 1093–1096 (1979)
Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon, Oxford (1970)
Koprowski, A., Middeldorp, A.: Predictive labeling with dependency pairs using SAT. In: Proc. 21st International Conference on Automated Deduction. LNAI, vol. 4603, pp. 410–425 (2004)
Koprowski, A., Waldmann, J.: Arctic termination ... below zero. In: Proc. 19th International Conference on Rewriting Techniques and Applications. LNCS, vol. 5117, pp. 202–216 (2008)
Korovin, K., Voronkov., A.: Orienting rewrite rules with the Knuth–Bendix order. Inf. Comput. 183, 165–186 (2003)
Kurihara, M., Kondo, H.: Efficient BDD encodings for partial order constraints with application to expert systems in software verification. In: Proc. 17th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems. LNAI, vol. 3029, pp. 827–837 (2004)
Lankford, D.: On proving term rewrite systems are noetherian. Tech. Rep. MTP-3, Louisiana Technical University, Ruston, LA, USA (1979)
Lepper, I.: Derivation lengths and order types of Knuth–Bendix orders. Theor. Comput. Sci. 269(1–2), 433–450 (2001)
Marché, C.: Termination problems data base (TPDB), version 4.0. http://www.lri.fr/~marche/tpdb (2007)
Moser, G.: Derivational complexity of Knuth–Bendix orders revisited. In: Proc. 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. LNAI, vol. 4246, pp. 75–89 (2006)
Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293–304 (1986)
Sato, H., Kurihara, M.: Implementation and performance evaluation of multi-completion procedures for term rewriting systems with recursive path orderings with status. IEICE Trans. Inf. Syst. J89-D(4), 624–631 (2006) (in Japanese)
Schneider-Kamp, P., Thiemann, R., Annov, E., Codish, M., Giesl, J.: Proving termination using recursive path orders and SAT solving. In: Proc. 6th International Symposium on Frontiers of Combining Systems. LNAI, vol. 4720, pp. 267–282 (2007)
Steinbach, J.: Extensions and comparison of simplification orders. In: Proc. 3rd International Conference on Rewriting Techniques and Applications. LNCS, vol. 355, pp. 434–448 (1989)
Tseitin, G.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, Part 2, pp. 115–125 (1968)
Weiermann, A.: Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths. Theor. Comput. Sci. 139(1–2), 355–362 (1995)
Zankl, H.: BDD and SAT techniques for precedence based orders. Master’s thesis, University of Innsbruck (2006)
Zankl, H., Hirokawa, N., Middeldorp, A.: Constraints for argument filterings. In: Proc. 33rd International Conference on Current Trends in Theory and Practice of Computer Science. LNCS, vol. 4362, pp. 579–590 (2007)
Zankl, H., Middeldorp, A.: Satisfying KBO constraints. In: Proc. 18th International Conference on Rewriting Techniques and Applications. LNCS, vol. 4533, pp. 389–403 (2007)
Zankl, H., Middeldorp, A.: Increasing interpretations. In: Proc. 9th International Conference on Artificial Intelligence and Symbolic Computation. LNAI, vol. 5144, pp. 191–205 (2008)
Zantema, H., Waldmann, J.: Termination by quasi-periodic interpretations. In: Proc. 18th International Conference on Rewriting Techniques and Applications. LNCS, vol. 4533, pp. 404–418 (2007)
Author information
Authors and Affiliations
Corresponding author
Additional information
The first and third authors are supported by FWF (Austrian Science Fund) project P18763 and the second author is supported by the Grant-in-Aid for Young Scientists 20800022 of the Ministry of Education, Culture, Sports, Science and Technology of Japan.
Rights and permissions
About this article
Cite this article
Zankl, H., Hirokawa, N. & Middeldorp, A. KBO Orientability. J Autom Reasoning 43, 173–201 (2009). https://doi.org/10.1007/s10817-009-9131-z
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-009-9131-z