Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

Making Higher-Order Superposition Work

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. https://doi.org/10.5281/zenodo.5007440.

References

  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. Backes, J., Brown, C.E.: Analytic tableaux for higher-order logic with choice. J. Autom. Reason. 47(4), 451–479 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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. Brown, C.E.: Reducing higher-order theorem proving to a sequence of SAT problems. J. Autom. Reason. 51(1), 57–77 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  14. Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT—a distributed and learning equational prover. J. Autom. Reason. 18(2), 189–198 (1997)

    Article  Google Scholar 

  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. Henkin, L.: Completeness in the theory of types. J. Symb. Log. 15(2), 81–91 (1950)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  24. Jensen, D.C., Pietrzykowski, T.: Mechanizing omega-order type theory through unification. Theor. Comput. Sci. 3(2), 123–171 (1976)

    Article  MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  32. Murray, N.V.: Completely non-clausal theorem proving. Artif. Intell. 18(1), 67–85 (1982)

    Article  MATH  Google Scholar 

  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  Google Scholar 

  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. Steen, A., Benzmüller, C.: Extensional higher-order paramodulation in Leo-III. J. Autom. Reason. 65(6), 775–807 (2021)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  47. Sutcliffe, G.: The CADE ATP system competition-CASC. AI Mag. 37(2), 99–101 (2016)

    MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  49. Sutcliffe, G.: The CADE-27 automated theorem proving system competition—CASC-27. AI Commun. 32(5–6), 373–389 (2019)

    MathSciNet  MATH  Google Scholar 

  50. Sutcliffe, G.: The 10th IJCAR automated theorem proving system competition—CASC-J10. AI Commun. (2021)

  51. Turner, D.A.: Another algorithm for bracket abstraction. J. Symb. Log. 44(2), 267–270 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  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)

Download references

Acknowledgements

We are grateful to the maintainers of StarExec for letting us use their service. Ahmed Bhayat and Giles Reger guided us through details of Vampire 4.5. Ahmed Bhayat, Michael Färber, Mathias Fleury, Predrag Janičić, Mark Summerfield, and the anonymous reviewers suggested content, textual, and typesetting improvements. We thank them all. Vukmirović, Bentkamp, and Blanchette’s research has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (Grant Agreement No. 713999, Matryoshka). Blanchette and Nummelin’s research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (Project No. 016.Vidi.189.037, Lean Forward).

Author information

Authors and Affiliations

  1. Vrije Universiteit Amsterdam, Amsterdam, The Netherlands

    Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette & Visa Nummelin

  2. CNRS, Inria, LORIA, Université de Lorraine, Nancy, France

    Jasmin Blanchette & Sophie Tourret

  3. Max-Planck-Institut für Informatik, Saarbrücken, Germany

    Jasmin Blanchette & Sophie Tourret

  4. Imandra, Austin, TX, USA

    Simon Cruanes

Authors
  1. Petar Vukmirović
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexander Bentkamp
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jasmin Blanchette
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Simon Cruanes
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Visa Nummelin
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Sophie Tourret
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Petar Vukmirović.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Vukmirović, P., Bentkamp, A., Blanchette, J. et al. Making Higher-Order Superposition Work. J Autom Reasoning 66, 541–564 (2022). https://doi.org/10.1007/s10817-021-09613-z

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-021-09613-z

Keywords

Search

Navigation