An Extension of the Knuth-Bendix Ordering with LPO-Like Properties

1. Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, New York (1998)

   Google Scholar 

2. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation 4(3), 217–247 (1994)

   Article  MATH  MathSciNet  Google Scholar 

3. Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Applicable Algebra in Engineering, Communication and Computing (AAECC) 5(3/4), 193–212 (1994)

   Article  MATH  MathSciNet  Google Scholar 

4. Dick, J., Kalmus, J., Martin, U.: Automating the Knuth-Bendix ordering. Acta Informatica 28(2), 95–119 (1990)

   Article  MATH  MathSciNet  Google Scholar 

5. Fernández, M.-L., Godoy, G., Rubio, A.: Recursive path orderings can also be incremental. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 230–245. Springer, Heidelberg (2005)

   Chapter  Google Scholar 

6. Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with Evans equality. Information and Computation 204, 1453–1492 (2006)

   Article  MATH  MathSciNet  Google Scholar 

7. Hessenberg, G.: Grundbegriffe der Mengenlehre. Vandenhoeck & Ruprecht, Göttingen (1906)

   Google Scholar 

8. Hillenbrand, T., Weidenbach, C.: Superposition for finite domains. Research Report MPI-I-2007-RG1-002, Max-Planck-Institut für Informatik, Stuhlsatzenhausweg 85, 66123 Saarbrücken, Germany (April 2007)

   Google Scholar 

9. Just, W., Weese, M.: Discovering modern set theory. I: The Basics, Graduate Studies in Mathematics, vol. 8. American Mathematical Society (1996)

   Google Scholar 

10. Kamin, S., Lévy, J.-J.: Attempts for generalising the recursive path orderings. Manuscript Department of Computer Science, University of Illinois, Urbana-Champaign (1980), available at http://perso.ens-lyon.fr/pierre.lescanne/not_accessible.html

11. Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)

    Google Scholar 

12. Löchner, B.: Things to know when implementing KBO. Journal of Automated Reasoning 36, 289–310 (2006)

    Article  MATH  MathSciNet  Google Scholar 

13. Ludwig, M.: Extensions of the Knuth-Bendix ordering with LPO-like properties. Diploma thesis, Universität des Saarlandes, Saarbrücken, Germany (July 2006)

    Google Scholar 

14. McCune, W.: Otter 3.3 Reference Manual. Argonne National Laboratory, Argonne, IL, USA, Technical Memorandum No. 263 (August 2003)

    Google Scholar 

15. Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) ESCoR: FLoC 2006 Workshop on Empirically Successful Computerized Reasoning, Seattle, WA, USA. CEUR Workshop Proceedings, vol. 192, pp. 18–33 (August 2006)

    Google Scholar 

16. Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Communications 15, 91–110 (2002)

    MATH  Google Scholar 

17. Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobalt, C., Topić, D.: SPASS version 2.0. In: Voronkov, A. (ed.) CADE-18. LNCS (LNAI), vol. 2392, pp. 275–279. Springer, Heidelberg (2002)

    Google Scholar 

Download references