New paper draft

Draft of the paper New Techniques for Higher-Order Superposition that I coauthored with Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Sophie Tourret, and Visa Nummelin is available.

Zipperposition 2 won CASC-J10 THF divison

I am very proud to announce that at the latest installment of annual CASC automatic theorem prover competition, Zipperposition 2 won the first place in THF (higher-order theorem) division. I was the lead developer of Zipperposition in the last two years, and prepared Zipperposition 2 CASC submission, but Zipperposition owes it performance to outstanding work of many other people. Some of those include: Alexander Bentkamp who is the main author of superposition with lambdas calculus; Sophie Tourret who implemented infinite stream management; Visa Nummelin who helped improve Boolean reasoning support; Jasmin Blanchette who supervised work of Alexander, Visa and me; Simon Cruanes who is the creator of Zipperposition and who guided us through its ins and outs. We have also implemented combinator-based calculus by Bhayat and Reger; we have further been inspired by many advanced ideas implemented in Satallax, and by Hilbert choice treatment of Leo-III. Many of the advanced heuristic schemes from E have been reimplemented (and lifted to higher-order logic) in Zipperposition. Many thanks to Stephan Schulz.
If you are interested in using Zipperposition in your own project, send me an email and I will gladly help you.

Best paper by junior researchers award at FSCD 2020

Paper Efficient Full Higher-Order Unification that I coauthored with Alexander Bentkamp and Visa Nummelin won the Best paper by junior researchers award at FSCD 2020. FSCD 2020 presentation is available at the link. Thanks to everyone who contributed to this paper with their comments!


Boolean reasoning in a higher-order superposition prover

Petar Vukmirović and Visa Nummelin

Accepted at 7th Workshop on 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



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


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