Top

Published in:

2017 | OriginalPaper | Chapter

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

Authors : Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand

Published in: Automated Deduction – CADE 26

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems

next chapter Certifying Safety and Termination Proofs for Integer Transition Systems

Andrews, P.B., Cohen, E.L.: Theorem proving in type theory. In: Reddy, R. (ed.) IJCAI 1977, p. 566. William Kaufmann (1977)

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

Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)CrossRefMATH

Backes, J., Brown, C.E.: Analytic tableaux for higher-order logic with choice. J. Autom. Reasoning 47(4), 451–479 (2011)MathSciNetCrossRefMATH

Banâtre, J.-P., Fradet, P., Radenac, Y.: Generalised multisets for chemical programming. Math. Struct. Comput. Sci. 16(4), 557–580 (2006)MathSciNetCrossRefMATH

Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: Formalization of Knuth-Bendix orders for lambda-free higher-order terms. Archive of Formal Proofs (2016). Formal proof development, https://isa-afp.org/entries/Lambda_Free_KBOs.shtml

Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: Transfinite Knuth-Bendix orders for lambda-free higher-order terms. Tech. report (2017), http://cs.vu.nl/~jbe248/lambda_free_kbo_rep.pdf

Beeson, M.: Lambda logic. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS, vol. 3097, pp. 460–474. Springer, Heidelberg (2004). doi:10.1007/978-3-540-25984-8_34 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.

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)

11.

Blanchette, J.C., Fleury, M., Traytel, D.: Formalization of nested multisets, hereditary multisets, and syntactic ordinals. Archive of Formal Proofs (2016). Formal proof development, https://isa-afp.org/entries/Nested_Multisets_Ordinals.shtml

12.

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.

Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning 9(1), 101–148 (2016)MathSciNet

14.

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

15.

Blanchette, J.C., Waldmann, U., Wand, D.: Formalization of recursive path orders for lambda-free higher-order terms. Archive of Formal Proofs (2016). Formal proof development, https://isa-afp.org/entries/Lambda_Free_RPOs.shtml

16.

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.

Blanqui, F., Jouannaud, J.-P., Rubio, A.: The computability path ordering. Log. Meth. Comput. Sci. 11(4) (2015)

18.

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.

Bofill, M., Rubio, A.: Paramodulation with non-monotonic orderings and simplification. J. Autom. Reasoning 50(1), 51–98 (2013)MathSciNetCrossRefMATH

20.

Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM 22(8), 465–476 (1979)MathSciNetCrossRefMATH

21.

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.

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

23.

Henkin, L.: Completeness in the theory of types. J. Symb. Log. 15(2), 81–91 (1950)MathSciNetCrossRefMATH

24.

Hirokawa, N., Middeldorp, A., Zankl, H.: Uncurrying for termination and complexity. J. Autom. Reasoning 50(3), 279–315 (2013)MathSciNetCrossRefMATH

25.

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.

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.

Hughes, R.J.M.: Super-combinators: a new implementation method for applicative languages. In: LFP 1982, pp. 1–10. ACM Press (1982)

28.

Jouannaud, J.-P., Rubio, A.: Polymorphic higher-order recursive path orderings. J. ACM 54(1), 2:1–2:48 (2007)MathSciNetCrossRefMATH

29.

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.

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.

Kop, C.: Higher Order Termination. Ph.D. thesis, Vrije Universiteit Amsterdam (2012)

32.

Kop, C., Raamsdonk, F.: A higher-order iterative path ordering. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS, vol. 5330, pp. 697–711. Springer, Heidelberg (2008). doi:10.1007/978-3-540-89439-1_48 CrossRef

33.

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

34.

Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_1 CrossRef

35.

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

36.

Löchner, B.: Things to know when implementing KBO. J. Autom. Reasoning 36(4), 289–310 (2006)MathSciNetCrossRefMATH

37.

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.

McCune, W.: Otter 3.3 reference manual. Technical. Report 263 (2003)

39.

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.

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

41.

Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013). doi:10.1007/978-3-642-45221-5_49 CrossRef

42.

Sternagel, C., Thiemann, R.: Executable multivariate polynomials. Archive of Formal Proofs (2010). Formal proof development, https://isa-afp.org/entries/Polynomials.shtml

43.

Sternagel, C., Thiemann, R.: Generalized and formalized uncurrying. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 243–258. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24364-6_17 CrossRef

44.

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.

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.

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.

Turner, D.A.: A new implementation technique for applicative languages. Softw. Pract. Experience 9(1), 31–49 (1979)CrossRefMATH

48.

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.

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.

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.

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)

Title: A Transfinite Knuth–Bendix Order for Lambda-Free Higher-Order Terms
Authors: Heiko Becker
Jasmin Christian Blanchette
Uwe Waldmann
Daniel Wand
Publisher: Springer International Publishing
Book: Automated Deduction – CADE 26
Print ISBN: 978-3-319-63045-8

Electronic ISBN: 978-3-319-63046-5

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-63046-5_27

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner