Extending a brainiac prover to lambda-free higher-order logic

Petar Vukmirović*, Jasmin Blanchette, Simon Cruanes, Stephan Schulz

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review


Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition prover E and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to λ-free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone toward full higher-order logic.

Original languageEnglish
Pages (from-to)67-87
Number of pages21
JournalInternational Journal on Software Tools for Technology Transfer
Issue number1
Early online date16 Aug 2021
Publication statusPublished - Feb 2022

Bibliographical note

Funding Information:
Vukmirović 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 has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (Project No. 016.Vidi.189.037, Lean Forward). He also benefited from the NWO Incidental Financial Support scheme.

Funding Information:
We are grateful to the maintainers of StarExec for letting us use their service. We thank Ahmed Bhayat, Alexander Bentkamp, Daniel El Ouraoui, Michael F?rber, Pascal Fontaine, Predrag Jani?i?, Robert Lewis, Tomer Libal, Giles Reger, Hans-J?rg Schurr, Alexander Steen, Mark Summerfield, Dmitriy Traytel, and the anonymous reviewers for suggesting many improvements to this text. We also want to thank the other members of the Matryoshka team, including Sophie Tourret and Uwe Waldmann, as well as Christoph Benzm?ller, Andrei Voronkov, Daniel Wand, and Christoph Weidenbach, for many stimulating discussions. Finally, we thank the TACAS 2019 chairs and editors of this special issue, Tom?? Vojnar and Lijun Zhang, for their patience with us.

Publisher Copyright:
© 2021, The Author(s).


  • Automatic theorem provers
  • First-order logic
  • Higher-order logic


Dive into the research topics of 'Extending a brainiac prover to lambda-free higher-order logic'. Together they form a unique fingerprint.

Cite this