SpringerLink
Log in

Superposition for Higher-Order Logic

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

Abstract

We recently designed two calculi as step** stones towards superposition for full higher-order logic: Boolean-free \(\lambda \)-superposition and superposition for first-order logic with interpreted Booleans. Step** 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.

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
EUR 32.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

Similar content being viewed by others

Notes

  1. https://github.com/sneeuwballen/zipperposition.

  2. https://doi.org/10.5281/zenodo.4534759.

References

  1. Andrews, P.B.: On connections and higher-order logic. J. Autom. Reason. 5(3), 257–291 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  2. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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. Blanqui, F., Jouannaud, J.P., Rubio, A.: The computability path ordering. Log. Meth. Comput. Sci. 11(4), 15 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  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. Cervesato, I., Pfenning, F.: A linear spine calculus. J. Log. Comput. 13(5), 639–688 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

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

  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. Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theor. Comput. Sci. 192(1), 3–29 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  30. Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning, pp. 335–367. Elsevier and MIT Press (2001)

  31. Nummelin, V., Bentkamp, A., Tourret, S., Vukmirović, P.: Superposition with first-class Booleans and inprocessing clausification (technical report). https://matryoshka-project.github.io/pubs/boolsup_report.pdf

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

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

Download references

Acknowledgements

Uwe Waldmann provided advice and carefully checked the completeness proof. Visa Nummelin led the design of the \(\hbox {o}\)Sup calculus, which was a crucial step** stone for this work. Simon Cruanes helped us with the implementation. Martin Desharnais generated (and regenerated) the Sledgehammer benchmarks. Ahmed Bhayat explained the higher-order Vampire schedule and suggested textual improvements. Christoph Benzmüller provided us insight into the pitfalls of higher-order reasoning. Alexander Steen explained the details of Leo-III scheduling. Geoff Sutcliffe let us use StarExec Miami for our experiments. Simon Cruanes, Herman Geuvers, Mathias Fleury, Nicolas Peltier, Giles Reger, Mark Summerfield, and the anonymous reviewers suggested textual improvements. We thank them all.

Bentkamp, Blanchette, and Vukmirović’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). Bentkamp’s research has received funding from a Chinese Academy of Sciences President’s International Fellowship for Postdoctoral Researchers (grant No. 2021PT0015). Blanchette’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. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, No. 4, South Fourth Street, Zhong Guan Cun, Bei**g, 100190, China

    Alexander Bentkamp

  2. Department of Computer Science, Section of Theoretical Computer Science, Vrije Universiteit Amsterdam, De Boelelaan 1111, 1081 HV, Amsterdam, The Netherlands

    Alexander Bentkamp, Jasmin Blanchette & Petar Vukmirović

  3. Université de Lorraine, CNRS, Inria, LORIA, 615, rue du Jardin Botanique, 54600, Villers-lès-Nancy, France

    Sophie Tourret

  4. Max-Planck-Institut für Informatik, Saarland Informatics Campus E1 4, 66123, Saarbrücken, Germany

    Jasmin Blanchette & Sophie Tourret

Authors
  1. Alexander Bentkamp
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jasmin Blanchette
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sophie Tourret
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Petar Vukmirović
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexander Bentkamp.

Additional information

Publisher's Note

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

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Bentkamp, A., Blanchette, J., Tourret, S. et al. Superposition for Higher-Order Logic. J Autom Reasoning 67, 10 (2023). https://doi.org/10.1007/s10817-022-09649-9

Download citation

  • Received:

  • Accepted:

  • Published:

  • DOI: https://doi.org/10.1007/s10817-022-09649-9

Keywords

Search

Navigation