Home
EuroProofNet is the European research network on digital proofs. EuroProofNet aims at boosting the interoperability and usability of proof systems. EuroProofNet is a COST action started on November 2021 gathering more than 220 researchers from 30 different countries.
The aim of working group 2 (WG 2) 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.
The main purpose of this wiki is to provide
-
an inventory of automated theorem provers producing proofs
-
description of proof formats
-
an inventory of checking tools for these proof formats.
The inventory of provers and proof formats is open, freely accessible, and community-driven. For its build-up we depend on contributions from everybody building or using ATP systems, input and output formats, or related tools. Please help to complete the inventory by adding an entry for a theorem proving system.
Please see How to contribute for step-by-step instructions.
See list of systems for a collection of solvers/provers.
See list of formats for a collection of input/output formats.
See list of tools for a collection of auxiliary tools for formats and/or systems.
