Skip to main content
Top

2018 | OriginalPaper | Chapter

Superposition for Lambda-Free Higher-Order Logic

Authors : Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann

Published in: Automated Reasoning

Publisher: Springer International Publishing

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

search-config
loading …

Abstract

We introduce refutationally complete superposition calculi for intentional and extensional \(\lambda \)-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the \(\lambda \)-free higher-order lexicographic path and Knuth–Bendix orders. We implemented the calculi in the Zipperposition prover and evaluated them on TPTP benchmarks. They appear promising as a stepping stone towards complete, efficient automatic theorem provers for full higher-order logic.

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!

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!

Literature
1.
go back to reference Andrews, P.B.: Classical type theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, pp. 965–1007. Elsevier and MIT Press (2001)CrossRef Andrews, P.B.: Classical type theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, pp. 965–1007. Elsevier and MIT Press (2001)CrossRef
2.
go back to reference Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994)MathSciNetCrossRef Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994)MathSciNetCrossRef
6.
go back to reference 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, Amsterdam (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, Amsterdam (2014)
7.
go back to reference Benzmüller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II—a cooperative automatic theorem prover for classical higher-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162–170. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71070-7_14CrossRef Benzmüller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II—a cooperative automatic theorem prover for classical higher-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162–170. Springer, Heidelberg (2008). https://​doi.​org/​10.​1007/​978-3-540-71070-7_​14CrossRef
8.
go back to reference Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Log. Methods Comput. Sci. 12(4:13), 1–52 (2016)MathSciNetMATH Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Log. Methods Comput. Sci. 12(4:13), 1–52 (2016)MathSciNetMATH
9.
go back to reference Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101–148 (2016)MathSciNet Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101–148 (2016)MathSciNet
13.
go back to reference Bofill, M., Rubio, A.: Paramodulation with non-monotonic orderings and simplification. J. Autom. Reason. 50(1), 51–98 (2013)MathSciNetCrossRef Bofill, M., Rubio, A.: Paramodulation with non-monotonic orderings and simplification. J. Autom. Reason. 50(1), 51–98 (2013)MathSciNetCrossRef
16.
go back to reference Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. Ph.D. thesis, École polytechnique (2015) Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. Ph.D. thesis, École polytechnique (2015)
18.
go back to reference Czajka, Ł.: Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions. In: Avigad, J., Chlipala, A. (eds.) CPP 2016, pp. 49–57. ACM (2016) Czajka, Ł.: Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions. In: Avigad, J., Chlipala, A. (eds.) CPP 2016, pp. 49–57. ACM (2016)
19.
go back to reference Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions (extended abstract). In: LICS 1995, pp. 366–374. IEEE (1995) Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions (extended abstract). In: LICS 1995, pp. 366–374. IEEE (1995)
20.
23.
go back to reference Huet, G.P.: A mechanization of type theory. In: Nilsson, N.J. (ed.) IJCAI 1973, pp. 139–146. William Kaufmann, Burlington (1973) Huet, G.P.: A mechanization of type theory. In: Nilsson, N.J. (ed.) IJCAI 1973, pp. 139–146. William Kaufmann, Burlington (1973)
24.
go back to reference Kerber, M.: How to prove higher order theorems in first order logic. In: Mylopoulos, J., Reiter, R. (eds.) IJCAI 1991, pp. 137–142. Morgan Kaufmann, Burlington (1991) Kerber, M.: How to prove higher order theorems in first order logic. In: Mylopoulos, J., Reiter, R. (eds.) IJCAI 1991, pp. 137–142. Morgan Kaufmann, Burlington (1991)
27.
go back to reference Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reason. 40(1), 35–60 (2008)MathSciNetCrossRef Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reason. 40(1), 35–60 (2008)MathSciNetCrossRef
31.
go back to reference Robinson, J.: Mechanizing higher order logic. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 4, pp. 151–170. Edinburgh University Press, Edinburgh (1969) Robinson, J.: Mechanizing higher order logic. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 4, pp. 151–170. Edinburgh University Press, Edinburgh (1969)
32.
go back to reference Robinson, J.: A note on mechanizing higher order logic. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 5, pp. 121–135. Edinburgh University Press, Edinburgh (1970) Robinson, J.: A note on mechanizing higher order logic. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 5, pp. 121–135. Edinburgh University Press, Edinburgh (1970)
36.
go back to reference Steen, A., Benzmüller, C.: The higher-order prover Leo-III. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNAI, vol. 10900, pp. 108–116. Springer, Cham (2018) Steen, A., Benzmüller, C.: The higher-order prover Leo-III. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNAI, vol. 10900, pp. 108–116. Springer, Cham (2018)
38.
go back to reference Sutcliffe, G.: The CADE-26 automated theorem proving system competition–CASC-26. AI Commun. 30(6), 419–432 (2017)MathSciNetCrossRef Sutcliffe, G.: The CADE-26 automated theorem proving system competition–CASC-26. AI Commun. 30(6), 419–432 (2017)MathSciNetCrossRef
41.
go back to reference Vukmirović, P.: Implementation of lambda-free higher-order superposition. M.Sc. thesis, Vrije Universiteit Amsterdam (2018) Vukmirović, P.: Implementation of lambda-free higher-order superposition. M.Sc. thesis, Vrije Universiteit Amsterdam (2018)
43.
go back to reference Wand, D.: Superposition: types and polymorphism. Ph.D. thesis, Universität des Saarlandes (2017) Wand, D.: Superposition: types and polymorphism. Ph.D. thesis, Universität des Saarlandes (2017)
Metadata
Title
Superposition for Lambda-Free Higher-Order Logic
Authors
Alexander Bentkamp
Jasmin Christian Blanchette
Simon Cruanes
Uwe Waldmann
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-319-94205-6_3

Premium Partner