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 4/2022

17.01.2022

Making Higher-Order Superposition Work

verfasst von: Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2022

Einloggen, um Zugang zu erhalten
share
TEILEN

Abstract

Superposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about Booleans, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.
Vorheriger Artikel A Comprehensive Framework for Saturation Theorem Proving
Nächster Artikel A Wos Challenge Met

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.
Bachmair, L., Ganzinger, H.: Non-clausal resolution and superposition with selection and redundancy criteria. In: Voronkov, A. (ed.) LPAR ’92, LNCS, vol. 624, pp. 273–284. Springer (1992)
2.
3.
Barbosa, H., Reynolds, A., El Ouraoui, D., Tinelli, C., Barrett, C.W.: Extending SMT solvers to higher-order logic. In: Fontaine, P. (ed.) CADE-27, LNCS, vol. 11716, pp. 35–54. Springer (2019)
4.
Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011, LNCS, vol. 6806, pp. 171–177. Springer (2011)
5.
Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P.: Superposition for full higher-order logic. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28, LNCS, vol. 12699, pp. 396–412. Springer (2021)
6.
Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P., Waldmann, U.: Superposition with lambdas. J. Autom. Reason. 65(7), 893–940 (2021) MathSciNetCrossRefMATH
7.
Bentkamp, A., Blanchette, J.C., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018, LNCS, vol. 10900, pp. 28–46. Springer (2018)
8.
Benzmüller, C., Sorge, V., Jamnik, M., Kerber, M.: Can a higher-order and a first-order theorem prover cooperate? In: Baader, F., Voronkov, A. (eds.) LPAR 2004, LNCS, vol. 3452, pp. 415–431. Springer (2004)
9.
Bhayat, A., Reger, G.: Restricted combinatory unification. In: Fontaine, P. (ed.) CADE-27, LNCS, vol. 11716, pp. 74–93. Springer (2019)
10.
Bhayat, A., Reger, G.: A combinator-based superposition calculus for higher-order logic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020, Part I, LNCS, vol. 12166, pp. 278–296. Springer (2020)
11.
12.
Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. Ph.D. thesis, École polytechnique (2015)
13.
Czajka, L., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reason. 61(1–4), 423–453 (2018) MathSciNetCrossRefMATH
14.
Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT—a distributed and learning equational prover. J. Autom. Reason. 18(2), 189–198 (1997) CrossRef
15.
Ebner, G., Blanchette, J., Tourret, S.: Unifying splitting. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28, LNCS, vol. 12699, pp. 344–360. Springer (2021)
16.
Färber, M., Brown, C.E.: Internal guidance for Satallax. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNCS, vol. 9706, pp. 349–361. Springer (2016)
17.
Filliâtre, J., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013, LNCS, vol. 7792, pp. 125–128. Springer (2013)
18.
Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. In: Baader, F. (ed.) CADE-19, LNCS, vol. 2741, pp. 335–349. Springer (2003)
19.
Gleiss, B., Suda, M.: Layered clause selection for theory reasoning (short paper). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020, Part I, LNCS, vol. 12166, pp. 402–409. Springer (2020)
20.
21.
Hoder, K., Reger, G., Suda, M., Voronkov, A.: Selecting the selection. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNCS, vol. 9706, pp. 313–329. Springer (2016)
22.
Hoder, K., Voronkov, A.: Comparing unification algorithms in first-order theorem proving. In: Mertsching, B., Hund, M., Aziz, M.Z. (eds.) KI 2009, LNCS, vol. 5803, pp. 435–443. Springer (2009)
23.
Huet, G.P.: A unification algorithm for typed lambda-calculus. Theor. Comput. Sci. 1(1), 27–57 (1975) CrossRefMATH
24.
Jensen, D.C., Pietrzykowski, T.: Mechanizing omega-order type theory through unification. Theor. Comput. Sci. 3(2), 123–171 (1976) CrossRefMATH
25.
Johnsson, T.: Lambda lifting: transforming programs to recursive equations. In: Jouannaud, J. (ed.) FPCA 1985, LNCS, vol. 201, pp. 190–203. Springer (1985)
26.
Kaliszyk, C., Urban, J.: HOL(y)Hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5–22 (2015) CrossRefMATH
27.
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 (1970)
28.
Kohlhase, M.: A mechanization of sorted higher-order logic based on the resolution principle. Ph.D. thesis, Universität des Saarlandes, Saarbrücken, Germany (1994)
29.
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 (2013)
30.
Manna, Z., Waldinger, R.: A deductive approach to program synthesis. In: Buchanan, B.G. (ed.) IJCAI-79, pp. 542–551. William Kaufmann (1979)
31.
McCune, W., Wos, L.: Otter—the CADE-13 competition incarnations. J. Autom. Reason. 18(2), 211–220 (1997) CrossRef
32.
Murray, N.V.: Completely non-clausal theorem proving. Artif. Intell. 18(1), 67–85 (1982) CrossRefMATH
33.
Nipkow, T.: Functional unification of higher-order patterns. In: Best, E. (ed.) LICS 1993, pp. 64–74. IEEE Computer Society (1993)
34.
Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 335–367. Elsevier and MIT Press (2001)
35.
Nummelin, V., Bentkamp, A., Tourret, S., Vukmirović, P.: Superposition with first-class Booleans and inprocessing clausification. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28, LNCS. Springer (2021)
36.
Okasaki, C.: Purely Functional Data Structures. Cambridge University Press (1999)
37.
Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL-2010, EPiC Series in Computing, vol. 2, pp. 1–11. EasyChair (2010)
38.
Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Felty, A.P., Middeldorp, A. (eds.) CADE-25, LNCS, vol. 9195, pp. 399–415. Springer (2015)
39.
Schulz, S.: E—a brainiac theorem prover. AI Commun. 15(2–3), 111–126 (2002) MATH
40.
Schulz, S., Cruanes, S., Vukmirović, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE-27, LNCS, vol. 11716, pp. 495–507. Springer (2019)
41.
Schulz, S., Möhrmann, M.: Performance of clause selection heuristics for saturation-based theorem proving. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNCS, vol. 9706, pp. 330–345. Springer (2016)
42.
Steen, A.: Extensional paramodulation for higher-order logic and its effective implementation Leo-III. Ph.D. thesis, Free University of Berlin, Dahlem, Germany (2018)
43.
Steen, A., Benzmüller, C.: There is no best \(\beta \)-normalization strategy for higher-order reasoners. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20, LNCS, vol. 9450, pp. 329–339. Springer (2015)
44.
45.
Stump, A., Sutcliffe, G., Tinelli, C.: Starexec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014, LNCS, vol. 8562, pp. 367–373. Springer (2014)
46.
Sultana, N., Blanchette, J.C., Paulson, L.C.: LEO-II and Satallax on the Sledgehammer test bench. J. Appl. Log. 11(1), 91–102 (2013) MathSciNetCrossRefMATH
47.
Sutcliffe, G.: The CADE ATP system competition-CASC. AI Mag. 37(2), 99–101 (2016) MATH
48.
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
49.
Sutcliffe, G.: The CADE-27 automated theorem proving system competition—CASC-27. AI Commun. 32(5–6), 373–389 (2019) MathSciNetMATH
50.
Sutcliffe, G.: The 10th IJCAR automated theorem proving system competition—CASC-J10. AI Commun. (2021)
51.
52.
Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014, LNCS, vol. 8559, pp. 696–710. Springer (2014)
53.
Vukmirović, P., Bentkamp, A., Nummelin, V.: Efficient full higher-order unification. In: Ariola, Z.M. (ed.) FSCD, LIPIcs, vol. 167, p. 5:1-5:17. Schloss Dagstuhl—Leibniz-Zentrum für Informatik (2020)
54.
Vukmirović, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28, LNCS, vol. 12699, pp. 415–432. Springer (2021)
55.
Vukmirović, P., Blanchette, J.C., Cruanes, S., Schulz, S.: Extending a brainiac prover to lambda-free higher-order logic. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019, Part I, LNCS, vol. 11427, pp. 192–210. Springer (2019)
56.
Vukmirović, P., Nummelin, V.: Boolean reasoning in a higher-order superposition prover. In: Fontaine, P., Korovin, K., Kotsireas, I. S., Rümmer, P., Tourret, S. (eds.) PAAR-2020, CEUR Workshop Proceedings, vol. 2752, pp. 148–166. CEUR-WS.org (2020)
57.
Waldmann, U., Tourret, S., Robillard, S., Blanchette, J.: A comprehensive framework for saturation theorem proving. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020, Part I, LNCS, vol. 12166, pp. 316–334. Springer (2020)
58.
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 (2016)
Metadaten
Titel
Making Higher-Order Superposition Work
verfasst von
Petar Vukmirović
Alexander Bentkamp
Jasmin Blanchette
Simon Cruanes
Visa Nummelin
Sophie Tourret
Publikationsdatum
17.01.2022
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 4/2022
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-021-09613-z

Weitere Artikel der Ausgabe 4/2022

Journal of Automated Reasoning 4/2022 Zur Ausgabe

OriginalPaper

Tuple Interpretations for Termination of Term Rewriting

OriginalPaper

Larry Wos: Visions of Automated Reasoning

Correction

Correction to: Local is Best: Efficient Reductions to Modal Logic K

Correction

Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic

OriginalPaper

A Formalization of the Smith Normal Form in Higher-Order Logic

OriginalPaper

A Wos Challenge Met

Premium Partner