Drafts

SAT-inspired eliminations for superposition

Petar Vukmirović, Jasmin Blanchette, and Marijn J.H. Heule.

Publications

Making higher-order superposition work

Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret

Accepted at CADE-28, 2021

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

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

Accepted in International Journal on Software Tools for Technology Transfer, 20xy

Boolean reasoning in a higher-order superposition prover

Petar Vukmirović and Visa Nummelin

Practical Aspects of Automated Reasoning (PAAR-2020), 2020

Efficient full higher-order unification

Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin

In Ariola, Z.M. (ed.), 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), LIPIcs 167, pp. 5:1–5:17, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2020

Faster, higher, stronger: E 2.3

Stephan Schulz, Simon Cruanes, and Petar Vukmirović

In Fontaine, P. (ed.) 27th International Conference on Automated Deduction (CADE-27), LNCS 11716, pp. 495–507, Springer, 2019

Superposition with lambdas

Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann

In Fontaine, P. (ed.) 27th International Conference on Automated Deduction (CADE-27), LNCS 11716, pp. 55–73, Springer, 2019

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

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

In Vojnar, T., Zhang, L. (eds.) 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), LNCS 11427, pp. 192–210, Springer, 2019

Software

Zipperposition

In the last two years I have been the main developer of the Zipperposition theorem prover. It is a well-performing polymorphic higher-order theorem prover. Unlike other provers like E or Vampire, Zipperposition does not have an auto mode. Therefore, if you would like to use it in your projects let me know and I will provide you with a reasonable configuration to use in your domain.

You can find Zipperposition at the following link

E

I am also the main developer behind Ehoh, an extension of E to a fragment of higher-order logic. An extension to full higher-order logic is planned.

You can find E at the following link