Abstract
We consider various definitions of AC-compatible Knuth-Bendix orders. The orders of Steinbach and of Korovin and Voronkov are revisited. The former is enhanced to a more powerful AC-compatible order and we modify the latter to amend its lack of monotonicity on non-ground terms. We further present new complexity results. An extension reflecting the recent proposal of subterm coefficients in standard Knuth-Bendix orders is also given. The various orders are compared on problems in termination and completion.
The research described in this paper is supported by the Austrian Science Fund (FWF) international project I963, the bilateral programs of the Japan Society for the Promotion of Science and the KAKENHI Grant No. 25730004.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Alarcón, B., Lucas, S., Meseguer, J.: A dependency pair framework for A ∨ C-termination. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 35–51. Springer, Heidelberg (2010)
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. TCS 236(1-2), 133–178 (2000)
Bachmair, L., Plaisted, D.A.: Termination orderings for associative-commutative rewriting systems. JSC 1, 329–349 (1985)
Ben Cherifa, A., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. SCP 9(2), 137–159 (1987)
Codish, M., Giesl, J., Schneider-Kamp, P., Thiemann, R.: SAT solving for termination proofs with recursive path orders and dependency pairs. JAR 49(1), 53–93 (2012)
Dershowitz, N.: Orderings for term-rewriting systems. TCS 17(3), 279–301 (1982)
Giesl, J., Kapur, D.: Dependency pairs for equational rewriting. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 93–107. Springer, Heidelberg (2001)
Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, New York (1970)
Korovin, K., Voronkov, A.: An AC-compatible Knuth-Bendix order. In: Baader, F. (ed.) CADE-19. LNCS (LNAI), vol. 2741, pp. 47–59. Springer, Heidelberg (2003)
Korovin, K., Voronkov, A.: Orienting rewrite rules with the Knuth-Bendix order. I&C 183(2), 165–186 (2003)
Kusakari, K.: AC-Termination and Dependency Pairs of Term Rewriting Systems. PhD thesis, JAIST (2000)
Kusakari, K., Toyama, Y.: On proving AC-termination by AC-dependency pairs. IEICE Transactions on Information and Systems E84-D(5), 439–447 (2001)
Löchner, B.: Things to know when implementing KBO. JAR 36(4), 289–310 (2006)
Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with LPO-like properties. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 348–362. Springer, Heidelberg (2007)
Marché, C., Urbain, X.: Modular and incremental proofs of AC-termination. JSC 38(1), 873–897 (2004)
Rubio, A.: A fully syntactic AC-RPO. I&C 178(2), 515–533 (2002)
Steinbach, J.: AC-termination of rewrite systems: A modified Knuth-Bendix ordering. In: Kirchner, H., Wechler, W. (eds.) ALP 1990. LNCS, vol. 463, pp. 372–386. Springer, Heidelberg (1990)
Thiemann, R., Allais, G., Nagele, J.: On the formalization of termination techniques based on multiset orderings. In: Proc. RTA-23. LIPIcs, vol. 15, pp. 339–354 (2012)
Winkler, S.: Termination Tools in Automated Reasoning. PhD thesis, UIBK (2013)
Winkler, S., Zankl, H., Middeldorp, A.: Ordinals and Knuth-Bendix orders. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 420–434. Springer, Heidelberg (2012)
Yamada, A., Winkler, S., Hirokawa, N., Middeldorp, A.: AC-KBO revisited. CoRR abs/1403.0406 (2014)
Zankl, H., Hirokawa, N., Middeldorp, A.: KBO orientability. JAR 43(2), 173–201 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Yamada, A., Winkler, S., Hirokawa, N., Middeldorp, A. (2014). AC-KBO Revisited. In: Codish, M., Sumii, E. (eds) Functional and Logic Programming. FLOPS 2014. Lecture Notes in Computer Science, vol 8475. Springer, Cham. https://doi.org/10.1007/978-3-319-07151-0_20
Download citation
DOI: https://doi.org/10.1007/978-3-319-07151-0_20
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07150-3
Online ISBN: 978-3-319-07151-0
eBook Packages: Computer ScienceComputer Science (R0)