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.