The meeting will take place at LRI, in the PCRI building (650), room 465. Warning: the room has changed!
Program:
- 13:30: welcome coffee
- 14:00: Mathias Fleury (Johannes Kepler Universität Linz, Austria), « Reconstructing veriT proofs in Isabelle/HOL »
Automated theorem provers are now commonly used within interactive theorem provers to discharge an increasingly large number of proof obligations. In this talk I present a framework for processing formulas in automatic theorem provers, in order to generate detailed proofs. The main components are a generic contextual recursion algorithm and an extensible set of inference rules. Clausification, skolemization, theory-specific simplifications, and expansion of `let’ expressions are instances of this framework. With suitable data structures, proof generation adds only a linear-time overhead.
This framework has been implemented in the satisfiability modulo theories solver (SMT) solver veriT. Implementing it made it possible to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced, which is important for independent checking and reconstruction in proof assistants. After that I present a reconstruction procedure in the proof assistant Isabelle/HOL for proofs generated by veriT as part of the smt tactic. I describe the reconstruction method and the challenges faced while designing it.
The work presented here is joint work with Haniel Barbosa, Jasmin Blanchette, Pascal Fontaine, and Hans-Jörg Schurr.
- 15:00: coffee break
- 15:15: Yacine El Haddad (LSV), « ekstrakto, a tool to reconstruct Dedukti proofs from TSTP files »
Proof assistants often call automated theorem provers to prove subgoals. However, each prover has its own proof calculus and the proof traces that it produces often lack many details to build a complete proof. Hence these traces are hard to check and reuse in proof assistants. Dedukti is a proof checker whose proofs can be translated to various proof assistants: Coq, HOL, Lean, Matita, PVS. We implemented a tool that extracts TPTP subproblems from a TSTP file and reconstructs complete proofs in Dedukti using automated provers able to generate Dedukti proofs like ZenonModulo or ArchSAT. This tool is generic: it assumes nothing about the proof calculus of the prover producing the trace, and it can use different provers to produce the Dedukti proof. We applied our tool on traces produced by automated theorem provers on the CNF problems of the TPTP library and we were able to reconstruct a proof for a large proportion of them, significantly increasing the number of Dedukti proofs that could be obtained for those problems.
- 15:45: Lutz Strassburger (LIX & Inria), « Introduction to Combinatorial Proofs » (work based on three papers: FSCD’17, RR-9203, LICS’19)
In this talk I will give an introduction to combinatorial proofs, explain the motivation behind, and discuss what it means for a proof to be « without syntax ». The main emphasis will be on combinatorial proofs for classical and intuitionistic propositional logic.
- 16:30: discussion and future of the working group