Journal of Automated Reasoning

, Volume 36, Issue 4, pp 289–310 | Cite as

Things to Know when Implementing KBO



The Knuth–Bendix ordering (KBO) is one of the term orderings in widespread use. We present a new algorithm to compute KBO, which is (to our knowledge) the first asymptotically optimal one. Starting with an ‘obviously correct’ version, we use program transformation to stepwise develop an efficient version, making clear the essential ideas, while retaining correctness. By theoretical analysis we show that the worst-case behavior is thereby changed from quadratic to linear. Measurements show the practical improvements of the different variants.

Key words

Knuth–Bendix ordering program transformation 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. Journal of the ACM 24(1), 44–67 (1977)MATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Buch, A., Hillenbrand, T.: \(\textsc{Waldmeister}\): Development of a High Performance Completion-Based Theorem Prover. SEKI-Report 96-01, Universität Kaiserslautern (1996)Google Scholar
  3. 3.
    Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch. 9. Elsevier (2001)Google Scholar
  4. 4.
    Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Algebra, pp. 263–297. Pergamon (1970)Google Scholar
  5. 5.
    Löchner, B., Hillenbrand, T.: A phytography of \(\textsc{Wald\-mei\-ster}\). AI Commun. 15(2–3), 127–133 (2002). See MATHGoogle Scholar
  6. 6.
    Löchner, B.: Things to know when implementing LPO. Int. J. Artif. Intell. Tools 15(1), 53–79 (2006). A preliminary version appeared. In: Sutcliffe, G., Schulz, S., Tammet, T. (eds.) Proc. 1st Workshop on Empirically Successful First Order Reasoning (ESFOR '04) (2004)Google Scholar
  7. 7.
    Nieuwenhuis, R., Hillenbrand, T., Riazanov, A., Voronkov, A.: On the evaluation of indexing techniques for theorem proving. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) Proc. 1st International Joint Conference on Automated Reasoning, Lecture Notes in Comput. Sci. 2083, pp. 257–271. Springer, Berlin Heidelberg New York (2001)Google Scholar
  8. 8.
    Pettorossi, A., Proietti, M.: Rules and strategies for program transformation. In: Möller, B., Partsch, H., Schuman, S. (eds.) Formal Program Development, vol. 755 of Lecture Notes in Comput. Sci., pp. 263–304. Springer, Berlin Heidelberg New York (1993)Google Scholar
  9. 9.
    Riazanov, A., Voronkov, A.: The design and implementation of \(\textsc{Vampire}\). AI Commun. 15, 91–110 (2002). See MATHGoogle Scholar
  10. 10.
    Riazanov, A., Voronkov, A.: Efficient checking of term ordering constraints. In: Basin, D., Rusinowitch, M. (eds.) Proc. 2nd International Joint Conference on Automated Reasoning, LNCS 3097, pp. 60–74. Springer, Berlin Heidelberg New York (2004)Google Scholar
  11. 11.
    Schulz, S.: E – A brainiac theorem prover. AI Commun. 15, 111–126 (2002). See MATHGoogle Scholar
  12. 12.
    Sutcliffe, G., Suttner, C.B.: The TPTP problem library: CNF release v1.2.1. J. Autom. Reason. 21(2), 177–203 (1998). See MATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Steinbach, J.: Termination of Rewriting. Ph.D. thesis, Universität Kaiserslautern, 1994. See
  14. 14.
    Wadler, P.: Comprehending monads. Math. Struct. Comput. Sci. 2, 461–493 (1992)MATHMathSciNetCrossRefGoogle Scholar
  15. 15.
    Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, ch. 27. Elsevier (2001)Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2006

Authors and Affiliations

  1. 1.FB InformatikTechnische Universität KaiserslauternKaiserslauternGermany

Personalised recommendations