Skip to main content

2017 | OriginalPaper | Buchkapitel

A Transfinite Knuth–Bendix Order for Lambda-Free Higher-Order Terms

verfasst von : Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand

Erschienen in: Automated Deduction – CADE 26

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We generalize the Knuth–Bendix order (KBO) to higher-order terms without \(\lambda \)-abstraction. The restriction of this new order to first-order terms coincides with the traditional KBO. The order has many useful properties, including transitivity, the subterm property, compatibility with contexts (monotonicity), stability under substitution, and well-foundedness. Transfinite weights and argument coefficients can also be supported. The order appears promising as the basis of a higher-order superposition calculus.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literatur
1.
Zurück zum Zitat Andrews, P.B., Cohen, E.L.: Theorem proving in type theory. In: Reddy, R. (ed.) IJCAI 1977, p. 566. William Kaufmann (1977) Andrews, P.B., Cohen, E.L.: Theorem proving in type theory. In: Reddy, R. (ed.) IJCAI 1977, p. 566. William Kaufmann (1977)
2.
Zurück zum Zitat Aoto, T., Yamada, T.: Termination of simply typed term rewriting by translation and labelling. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 380–394. Springer, Heidelberg (2003). doi:10.1007/3-540-44881-0_27 CrossRef Aoto, T., Yamada, T.: Termination of simply typed term rewriting by translation and labelling. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 380–394. Springer, Heidelberg (2003). doi:10.​1007/​3-540-44881-0_​27 CrossRef
3.
Zurück zum Zitat Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)CrossRefMATH Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)CrossRefMATH
4.
5.
Zurück zum Zitat Banâtre, J.-P., Fradet, P., Radenac, Y.: Generalised multisets for chemical programming. Math. Struct. Comput. Sci. 16(4), 557–580 (2006)MathSciNetCrossRefMATH Banâtre, J.-P., Fradet, P., Radenac, Y.: Generalised multisets for chemical programming. Math. Struct. Comput. Sci. 16(4), 557–580 (2006)MathSciNetCrossRefMATH
9.
Zurück zum Zitat Benzmüller, C., Kohlhase, M.: Extensional higher-order resolution. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS, vol. 1421, pp. 56–71. Springer, Heidelberg (1998). doi:10.1007/BFb0054248 CrossRef Benzmüller, C., Kohlhase, M.: Extensional higher-order resolution. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS, vol. 1421, pp. 56–71. Springer, Heidelberg (1998). doi:10.​1007/​BFb0054248 CrossRef
10.
Zurück zum Zitat Benzmüller, C., Miller, D.: Automation of higher-order logic. In: Siekmann, J.H. (ed.) Computational Logic. Handbook of the History of Logic, vol. 9, pp. 215–254. Elsevier (2014) Benzmüller, C., Miller, D.: Automation of higher-order logic. In: Siekmann, J.H. (ed.) Computational Logic. Handbook of the History of Logic, vol. 9, pp. 215–254. Elsevier (2014)
12.
Zurück zum Zitat Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (Co)datatypes for Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93–110. Springer, Cham (2014). doi:10.1007/978-3-319-08970-6_7 Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (Co)datatypes for Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93–110. Springer, Cham (2014). doi:10.​1007/​978-3-319-08970-6_​7
13.
Zurück zum Zitat Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning 9(1), 101–148 (2016)MathSciNet Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning 9(1), 101–148 (2016)MathSciNet
14.
Zurück zum Zitat Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14052-5_11 CrossRef Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-14052-5_​11 CrossRef
16.
Zurück zum Zitat Blanchette, J.C., Waldmann, U., Wand, D.: A lambda-free higher-order recursive path order. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 461–479. Springer, Heidelberg (2017). doi:10.1007/978-3-662-54458-7_27 CrossRef Blanchette, J.C., Waldmann, U., Wand, D.: A lambda-free higher-order recursive path order. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 461–479. Springer, Heidelberg (2017). doi:10.​1007/​978-3-662-54458-7_​27 CrossRef
17.
Zurück zum Zitat Blanqui, F., Jouannaud, J.-P., Rubio, A.: The computability path ordering. Log. Meth. Comput. Sci. 11(4) (2015) Blanqui, F., Jouannaud, J.-P., Rubio, A.: The computability path ordering. Log. Meth. Comput. Sci. 11(4) (2015)
18.
Zurück zum Zitat Bofill, M., Borralleras, C., Rodríguez-Carbonell, E., Rubio, A.: The recursive path and polynomial ordering for first-order and higher-order terms. J. Log. Comput. 23(1), 263–305 (2013)MathSciNetCrossRefMATH Bofill, M., Borralleras, C., Rodríguez-Carbonell, E., Rubio, A.: The recursive path and polynomial ordering for first-order and higher-order terms. J. Log. Comput. 23(1), 263–305 (2013)MathSciNetCrossRefMATH
19.
Zurück zum Zitat Bofill, M., Rubio, A.: Paramodulation with non-monotonic orderings and simplification. J. Autom. Reasoning 50(1), 51–98 (2013)MathSciNetCrossRefMATH Bofill, M., Rubio, A.: Paramodulation with non-monotonic orderings and simplification. J. Autom. Reasoning 50(1), 51–98 (2013)MathSciNetCrossRefMATH
21.
Zurück zum Zitat Ferreira, M.C.F., Zantema, H.: Well-foundedness of term orderings. In: Dershowitz, N., Lindenstrauss, N. (eds.) CTRS 1994. LNCS, vol. 968, pp. 106–123. Springer, Heidelberg (1995). doi:10.1007/3-540-60381-6_7 CrossRef Ferreira, M.C.F., Zantema, H.: Well-foundedness of term orderings. In: Dershowitz, N., Lindenstrauss, N. (eds.) CTRS 1994. LNCS, vol. 968, pp. 106–123. Springer, Heidelberg (1995). doi:10.​1007/​3-540-60381-6_​7 CrossRef
22.
Zurück zum Zitat Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCoS 2005. LNCS, vol. 3717, pp. 216–231. Springer, Heidelberg (2005). doi:10.1007/11559306_12 CrossRef Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCoS 2005. LNCS, vol. 3717, pp. 216–231. Springer, Heidelberg (2005). doi:10.​1007/​11559306_​12 CrossRef
24.
Zurück zum Zitat Hirokawa, N., Middeldorp, A., Zankl, H.: Uncurrying for termination and complexity. J. Autom. Reasoning 50(3), 279–315 (2013)MathSciNetCrossRefMATH Hirokawa, N., Middeldorp, A., Zankl, H.: Uncurrying for termination and complexity. J. Autom. Reasoning 50(3), 279–315 (2013)MathSciNetCrossRefMATH
25.
Zurück zum Zitat Huet, G., Oppen, D.C.: Equations and rewrite rules: a survey. In: Book, R.V. (ed.) Formal Language Theory: Perspectives and Open Problems, pp. 349–405. Academic Press (1980) Huet, G., Oppen, D.C.: Equations and rewrite rules: a survey. In: Book, R.V. (ed.) Formal Language Theory: Perspectives and Open Problems, pp. 349–405. Academic Press (1980)
26.
Zurück zum Zitat Huet, G.P.: A mechanization of type theory. In: Nilsson, N.J. (ed.) International Joint Conference on Artificial Intelligence (IJCAI 1973), pp. 139–146. William Kaufmann (1973) Huet, G.P.: A mechanization of type theory. In: Nilsson, N.J. (ed.) International Joint Conference on Artificial Intelligence (IJCAI 1973), pp. 139–146. William Kaufmann (1973)
27.
Zurück zum Zitat Hughes, R.J.M.: Super-combinators: a new implementation method for applicative languages. In: LFP 1982, pp. 1–10. ACM Press (1982) Hughes, R.J.M.: Super-combinators: a new implementation method for applicative languages. In: LFP 1982, pp. 1–10. ACM Press (1982)
29.
Zurück zum Zitat Kennaway, R., Klop, J.W., Sleep, M.R., de Vries, F.: Comparing curried and uncurried rewriting. J. Symbolic Comput. 21(1), 15–39 (1996)MathSciNetCrossRefMATH Kennaway, R., Klop, J.W., Sleep, M.R., de Vries, F.: Comparing curried and uncurried rewriting. J. Symbolic Comput. 21(1), 15–39 (1996)MathSciNetCrossRefMATH
30.
Zurück zum Zitat 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 (1970) 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 (1970)
31.
Zurück zum Zitat Kop, C.: Higher Order Termination. Ph.D. thesis, Vrije Universiteit Amsterdam (2012) Kop, C.: Higher Order Termination. Ph.D. thesis, Vrije Universiteit Amsterdam (2012)
32.
33.
Zurück zum Zitat Kovács, L., Moser, G., Voronkov, A.: On transfinite Knuth-Bendix orders. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 384–399. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22438-6_29 CrossRef Kovács, L., Moser, G., Voronkov, A.: On transfinite Knuth-Bendix orders. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 384–399. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22438-6_​29 CrossRef
35.
Zurück zum Zitat Lifantsev, M., Bachmair, L.: An LPO-based termination ordering for higher-order terms without \(\lambda \)-abstraction. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 277–293. Springer, Heidelberg (1998). doi:10.1007/BFb0055142 CrossRef Lifantsev, M., Bachmair, L.: An LPO-based termination ordering for higher-order terms without \(\lambda \)-abstraction. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 277–293. Springer, Heidelberg (1998). doi:10.​1007/​BFb0055142 CrossRef
37.
Zurück zum Zitat Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with LPO-like properties. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS, vol. 4790, pp. 348–362. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75560-9_26 CrossRef Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with LPO-like properties. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS, vol. 4790, pp. 348–362. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-75560-9_​26 CrossRef
38.
Zurück zum Zitat McCune, W.: Otter 3.3 reference manual. Technical. Report 263 (2003) McCune, W.: Otter 3.3 reference manual. Technical. Report 263 (2003)
39.
Zurück zum Zitat Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 371–443. Elsevier and MIT Press (2001) Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 371–443. Elsevier and MIT Press (2001)
40.
Zurück zum Zitat Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). doi:10.1007/3-540-45949-9 MATH Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). doi:10.​1007/​3-540-45949-9 MATH
43.
44.
Zurück zum Zitat Sternagel, C., Thiemann, R.: Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In: van Raamsdonk, F. (ed.) RTA 2013, vol. 21. LIPIcs, pp. 287–302. Schloss Dagstuhl (2013) Sternagel, C., Thiemann, R.: Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In: van Raamsdonk, F. (ed.) RTA 2013, vol. 21. LIPIcs, pp. 287–302. Schloss Dagstuhl (2013)
45.
Zurück zum Zitat Sultana, N., Blanchette, J.C., Paulson, L.C.: LEO-II and Satallax on the Sledgehammer test bench. J. Applied Logic 11(1), 91–102 (2013)MathSciNetCrossRefMATH Sultana, N., Blanchette, J.C., Paulson, L.C.: LEO-II and Satallax on the Sledgehammer test bench. J. Applied Logic 11(1), 91–102 (2013)MathSciNetCrossRefMATH
46.
Zurück zum Zitat Toyama, Y.: Termination of S-expression rewriting systems: lexicographic path ordering for higher-order terms. In: Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 40–54. Springer, Heidelberg (2004). doi:10.1007/978-3-540-25979-4_3 CrossRef Toyama, Y.: Termination of S-expression rewriting systems: lexicographic path ordering for higher-order terms. In: Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 40–54. Springer, Heidelberg (2004). doi:10.​1007/​978-3-540-25979-4_​3 CrossRef
47.
Zurück zum Zitat Turner, D.A.: A new implementation technique for applicative languages. Softw. Pract. Experience 9(1), 31–49 (1979)CrossRefMATH Turner, D.A.: A new implementation technique for applicative languages. Softw. Pract. Experience 9(1), 31–49 (1979)CrossRefMATH
48.
Zurück zum Zitat Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02959-2_10 CrossRef Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-02959-2_​10 CrossRef
49.
Zurück zum Zitat Wisniewski, M., Steen, A., Kern, K., Benzmüller, C.: Effective normalization techniques for HOL. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 362–370. Springer, Cham (2016). doi:10.1007/978-3-319-40229-1_25 Wisniewski, M., Steen, A., Kern, K., Benzmüller, C.: Effective normalization techniques for HOL. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 362–370. Springer, Cham (2016). doi:10.​1007/​978-3-319-40229-1_​25
50.
Zurück zum Zitat Zankl, H., Winkler, S., Middeldorp, A.: Beyond polynomials and Peano arithmetic–automation of elementary and ordinal interpretations. J. Symb. Comput. 69, 129–158 (2015)MathSciNetCrossRefMATH Zankl, H., Winkler, S., Middeldorp, A.: Beyond polynomials and Peano arithmetic–automation of elementary and ordinal interpretations. J. Symb. Comput. 69, 129–158 (2015)MathSciNetCrossRefMATH
51.
Zurück zum Zitat Zantema, H.: Termination. In: Bezem, M., Klop, J.W., de Vrijer, R. (eds.) Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55, pp. 181–259. Cambridge University Press, Cambridge (2003) Zantema, H.: Termination. In: Bezem, M., Klop, J.W., de Vrijer, R. (eds.) Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55, pp. 181–259. Cambridge University Press, Cambridge (2003)
Metadaten
Titel
A Transfinite Knuth–Bendix Order for Lambda-Free Higher-Order Terms
verfasst von
Heiko Becker
Jasmin Christian Blanchette
Uwe Waldmann
Daniel Wand
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-63046-5_27