WG2 Automated Theorem Provers
The aim of this WG is to promote the output of detailed, checkable proofs from automated theorem provers. Work is under way for FOL/HOL theorem provers and SMT solvers, but the expressivity of their input languages renders the task significantly more complicated than e.g., in the propositional SAT world, with a higher need of coordination.
Documents and Deliverables
We use a git repository to store all our documents and deliverables. In particular, we initiated an inventory of
- automated theorem provers producing proofs
- proof formats
- checking tools for these proof formats.
May 2023: WG2 second meeting and Dedukti tools developers meeting 3 in Liège (Belgium)
August 2022: WG2 kickoff meeting co-located with the PAAR workshop during FLOC at Haifa (Israel)
September 2022: VTSA school at Saarbrücken (Germany) with a focus on proof-generating verification systems