Petar Vukmirović

SAT-inspired eliminations for superposition

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

FMCAD, 2021

Conference proceedings (pg. 231-240) ⋅ Submission-paper (PDF) ⋅ Submission-report (PDF)

Efficient full higher-order unification

Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin.

LMCS, 2021

Accepted arXiv article (PDF)

Making higher-order superposition work — extended journal version

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

Accepted at JAR Larry Wos Special Issue, 2021

Draft article (PDF)

Making higher-order superposition work

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

CADE-28, 2021

Publisher's PDF

Superposition for full higher-order logic

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

CADE-28, 2021

Publisher's PDF ⋅ Submission (PDF) ⋅ Report (PDF)

Superposition with first-class Booleans and inprocessing clausification

Visa Nummelin, Alexander Bentkamp, Sophie Tourret, and Petar Vukmirović

CADE-28, 2021

Publisher's PDF ⋅ Submission (PDF) ⋅ Report (PDF)

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

Draft article

Boolean reasoning in a higher-order superposition prover

Petar Vukmirović and Visa Nummelin

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

Publisher's page (PDF) ⋅ Presentation (YouTube) ⋅ Slides

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

Publisher's page ⋅ Postprint (PDF) ⋅ Technical report (PDF) ⋅ Presentation (YouTube) ⋅ Slides

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

Publisher's page ⋅ Postprint (PDF)

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

Publisher's page ⋅ Postprint (PDF) ⋅ Report (PDF)

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

Publisher's page ⋅ Postprint (PDF) ⋅ Report (PDF) ⋅ Slides

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