Petar Vukmirović's Zipperposition 2 wins CASC-J10 THF divison

At the latest installment of annual CASC automatic theorem prover competition, Zipperposition 2, won the first place in THF (higher-order theorem) division. Petar 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 Turret who implemented infinite stream management; Visa Nummelin who helped improve Boolean reasoning support; Jasmin Blanchette who supervised work of Alexander, Visa and me.

07/17/2020 | 10:21 AM

Click here or here to read more.