Superposition for Higher-Order Logic | springerprofessional.de
Skip to main content
Registrieren
Springer Professional
SUCHE
MENÜ 1 2 3 4
nach oben

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Erschienen in: Journal of Automated Reasoning 1/2023

01.03.2023

Superposition for Higher-Order Logic

verfasst von: Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović

Erschienen in: Journal of Automated Reasoning | Ausgabe 1/2023

Einloggen, um Zugang zu erhalten
share
TEILEN

Abstract

We recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free \(\lambda \)-superposition and superposition for first-order logic with interpreted Booleans. Stepping on these stones, we finally reach a sound and refutationally complete calculus for higher-order logic with polymorphism, extensionality, Hilbert choice, and Henkin semantics. In addition to the complexity of combining the calculus’s two predecessors, new challenges arise from the interplay between \(\lambda \)-terms and Booleans. Our implementation in Zipperposition outperforms all other higher-order theorem provers and is on a par with an earlier, pragmatic prototype of Booleans in Zipperposition.
Vorheriger Artikel Correction: Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL
Nächster Artikel Finding Normal Binary Floating-Point Factors Efficiently

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 69.000 Bücher
  • über 500 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 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

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





Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

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



 


Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren
Fußnoten
Literatur
1.
2.
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994) MathSciNetCrossRefMATH
3.
Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 19–99. MIT Press, Cambridge (2001) CrossRef
4.
Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation and superposition. In: D. Kapur (ed.) CADE-11, LNCS, vol. 607, pp. 462–476. Springer (1992)
5.
Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV, LNCS, vol. 6806, pp. 171–177. Springer (2011)
6.
Benanav, D.: Simultaneous paramodulation. In: M.E. Stickel (ed.) CADE-10, LNCS, vol. 449, pp. 442–455. Springer (1990)
7.
Bentkamp, A.: Superposition for higher-order logic. Ph.D. thesis, Vrije Universiteit Amsterdam (2021)
8.
Bentkamp, A., Blanchette, J., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic. Log. Meth. Comput. Sci. 17(2), 1:1-1:38 (2021) MathSciNetMATH
9.
Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovic, P.: Superposition for full higher-order logic. In: A. Platzer, G. Sutcliffe (eds.) CADE-28, LNCS, vol. 12699, pp. 396–412. Springer (2021)
10.
Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P., Waldmann, U.: Superposition with lambdas. J. Autom. Reason. 65, 893–940 (2021) MathSciNetCrossRefMATH
11.
Benzmüller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II—A cooperative automatic theorem prover for higher-order logic. In: A. Armando, P. Baumgartner, G. Dowek (eds.) IJCAR 2008, LNCS, vol. 5195, pp. 162–170. Springer (2008)
12.
Bhayat, A., Reger, G.: Set of support for higher-order reasoning. In: B. Konev, J. Urban, P. Rümmer (eds.) PAAR-2018, CEUR Workshop Proceedings, vol. 2162, pp. 2–16. CEUR-WS.org (2018)
13.
Bhayat, A., Reger, G.: A combinator-based superposition calculus for higher-order logic. In: N. Peltier, V. Sofronie-Stokkermans (eds.) IJCAR 2020, Part I, LNCS, vol. 12166, pp. 278–296. Springer (2020)
14.
15.
Böhme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: J. Giesl, R. Hähnle (eds.) IJCAR 2010, LNCS, vol. 6173, pp. 107–121. Springer (2010)
16.
Brown, C.E.: Satallax: An automatic higher-order prover. In: B. Gramlich, D. Miller, U. Sattler (eds.) IJCAR 2012, LNCS, vol. 7364, pp. 111–117. Springer (2012)
17.
18.
Fitting, M.: Types, Tableaus, and Gödel’s God. Kluwer (2002)
19.
Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. Inform. Comput. 199(1–2), 3–23 (2005) MathSciNetCrossRefMATH
20.
Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press (1993)
21.
Huet, G.P.: A mechanization of type theory. In: N.J. Nilsson (ed.) IJCAI-73, pp. 139–146. William Kaufmann (1973)
22.
Huet, G.P.: A unification algorithm for typed lambda-calculus. Theor. Comput. Sci. 1(1), 27–57 (1975) CrossRefMATH
23.
Jensen, D.C., Pietrzykowski, T.: Mechanizing \(\omega \)-order type theory through unification. Theor. Comput. Sci. 3(2), 123–171 (1976) MathSciNetCrossRefMATH
24.
Jouannaud, J.P., Rubio, A.: Rewrite orderings for higher-order terms in eta-long beta-normal form and recursive path ordering. Theor. Comput. Sci. 208(1–2), 33–58 (1998) CrossRefMATH
25.
Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: The TPTP typed higher-order form with rank-1 polymorphism. In: P. Fontaine, S. Schulz, J. Urban (eds.) PAAR-2016, CEUR Workshop Proceedings, vol. 1635, pp. 41–55. CEUR-WS.org (2016)
26.
Kőnig, D.: Über eine Schlussweise aus dem Endlichen ins Unendliche. Acta Sci. Math. (Szeged) 3499/2009(3:2–3), 121–130 (1927) MATH
27.
Kotelnikov, E., Kovács, L., Suda, M., Voronkov, A.: A clausal normal form translation for FOOL. In: C. Benzmüller, G. Sutcliffe, R. Rojas (eds.) GCAI 2016, EPiC, vol. 41, pp. 53–71. EasyChair (2016)
28.
Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with LPO-like properties. In: N. Dershowitz, A. Voronkov (eds.) LPAR-14, LNCS, vol. 4790, pp. 348–362. Springer (2007)
29.
30.
Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning, pp. 335–367. Elsevier and MIT Press (2001)
31.
32.
Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: G. Sutcliffe, S. Schulz, E. Ternovska (eds.) IWIL-2010, EPiC, vol. 2, pp. 1–11. EasyChair (2012)
33.
Schulz, S.: E-a Brainiac theorem prover. AI Commun. 15(2–3), 111–126 (2002) MATH
34.
Steen, A., Benzmüller, C.: The higher-order prover Leo-III. In: D. Galmiche, S. Schulz, R. Sebastiani (eds.) IJCAR 2018, LNCS, vol. 10900, pp. 108–116. Springer (2018)
35.
Sutcliffe, G.: The TPTP problem library and associated infrastructure—from CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483–502 (2017) MathSciNetCrossRefMATH
36.
Tseitin, G.: On the complexity of derivation in propositional calculus. In: Automation of reasoning: Classical Papers on Computational Logic, vol. 2, pp. 466–483. Springer (1983)
37.
Vukmirović, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. In: A. Platzer, G. Sutcliffe (eds.) CADE-28, LNCS. Springer (2021)
38.
Vukmirović, P., Bentkamp, A., Nummelin, V.: Efficient full higher-order unification. In: Z.M. Ariola (ed.) FSCD 2020, LIPIcs, vol. 167, pp. 5:1–5:17. Schloss Dagstuhl—Leibniz-Zentrum für Informatik (2020)
39.
Vukmirović, P., Nummelin, V.: Boolean reasoning in a higher-order superposition prover. In: PAAR-2020, CEUR Workshop Proceedings, vol. 2752, pp. 148–166. CEUR-WS.org (2020)
40.
Waldmann, U., Tourret, S., Robillard, S., Blanchette, J.: A comprehensive framework for saturation theorem proving. In: N. Peltier, V. Sofronie-Stokkermans (eds.) IJCAR 2020, Part I, LNCS, vol. 12166, pp. 316–334. Springer (2020)
Metadaten
Titel
Superposition for Higher-Order Logic
verfasst von
Alexander Bentkamp
Jasmin Blanchette
Sophie Tourret
Petar Vukmirović
Publikationsdatum
01.03.2023
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 1/2023
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-022-09649-9

Weitere Artikel der Ausgabe 1/2023

Journal of Automated Reasoning 1/2023 Zur Ausgabe

OriginalPaper

Finding Normal Binary Floating-Point Factors Efficiently

OriginalPaper

Efficient Extensional Binary Tries

OriginalPaper

Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic

OriginalPaper

Optimal Deterministic Controller Synthesis from Steady-State Distributions

Correction

Correction: Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL

OriginalPaper

A Formalization and Proof Checker for Isabelle’s Metalogic

Premium Partner