Abstract
In this paper we consider a hierarchy of three versions of Knuth-Bendix orders. (1) We show that the standard definition can be (slightly) simplified without affecting the ordering relation. (2) For the extension of transfinite Knuth-Bendix orders we show that transfinite ordinals are not needed as weights, as far as termination of finite rewrite systems is concerned. (3) Nevertheless termination proving benefits from transfinite ordinals when used in the setting of general Knuth-Bendix orders defined over a weakly monotone algebra. We investigate the relationship to polynomial interpretations and present experimental results for both termination analysis and ordered completion. For the latter it is essential that the order is totalizable on ground terms.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Bachmair, L., Dershowitz, N., Plaisted, D.: Completion without failure. In: Kaci, H.A., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures 1989. Rewriting Techniques of Progress in Theoretical Computer Science, vol. 2, pp. 1–30. Academic Press (1989)
Dershowitz, N.: Orderings for term-rewriting systems. TCS 17, 279–301 (1982)
Dershowitz, N.: Termination of rewriting. J. Symb. Comp. 3(1-2), 69–116 (1987)
Dick, J., Kalmus, J., Martin, U.: Automating the Knuth Bendix ordering. AI 28, 95–119 (1990)
Ferreira, M., Zantema, H.: Total termination of term rewriting. AAECC 7(2), 133–162 (1996)
Geser, A.: An improved general path order. AAECC 7(6), 469–511 (1996)
Goodstein, R.L.: On the restricted ordinal theorem. J. of Symb. Log. 9(2), 33–41 (1944)
Hong, H., Jakuš, D.: Testing positiveness of polynomials. JAR 21(1), 23–38 (1998)
Jech, T.: Set Theory. Springer, Heidelberg (2002)
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)
Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295–304. Springer, Heidelberg (2009)
Kovács, L., Moser, G., Voronkov, A.: On transfinite knuth-bendix orders. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 23. LNCS, vol. 6803, pp. 384–399. Springer, Heidelberg (2011)
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)
McCune, B.: Otter 3.0 reference manual and guide. Technical Report ANL-94/6, Argonne National Laboratory (1994)
Middeldorp, A., Zantema, H.: Simple termination of rewrite systems. TCS 175(1), 127–158 (1997)
Neurauter, F., Middeldorp, A., Zankl, H.: Monotonicity Criteria for Polynomial Interpretations over the Naturals. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 502–517. Springer, Heidelberg (2010)
Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2-3), 91–110 (2002)
Steinbach, J.: Extensions and Comparison of Simplification Orders. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 434–448. Springer, Heidelberg (1989)
Steinbach, J., Zehnter, M.: Vademecum of polynomial orderings. Technical Report SR-90-03, Universität Kaiserslautern (1990)
Sutcliffe, G.: The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0. JAR 43(4), 337–362 (2009)
TeReSe: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)
Winkler, S., Middeldorp, A.: Termination Tools in Ordered Completion. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 518–532. Springer, Heidelberg (2010)
Zankl, H., Hirokawa, N., Middeldorp, A.: KBO orientability. JAR 43(2), 173–201 (2009)
Zankl, H., Middeldorp, A.: Satisfiability of non-linear (Ir)rational arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16. LNCS, vol. 6355, pp. 481–500. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Winkler, S., Zankl, H., Middeldorp, A. (2012). Ordinals and Knuth-Bendix Orders. In: Bjørner, N., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2012. Lecture Notes in Computer Science, vol 7180. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28717-6_33
Download citation
DOI: https://doi.org/10.1007/978-3-642-28717-6_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28716-9
Online ISBN: 978-3-642-28717-6
eBook Packages: Computer ScienceComputer Science (R0)