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.
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.
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!
Accepted at 7th Workshop on Practical Aspects of Automated Reasoning (PAAR-2020), 2020
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
In Fontaine, P. (ed.) 27th International Conference on Automated Deduction (CADE-27), LNCS 11716, pp. 495–507, Springer, 2019
In Fontaine, P. (ed.) 27th International Conference on Automated Deduction (CADE-27), LNCS 11716, pp. 55–73, Springer, 2019
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