europroofnet / atp

Repository of EuroProofNet WG 2 on ATPs

EuroProofNet WG2 on Automated Theorem Provers

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.

This repository collects material and documentation of project deliverables related to WG2. The contents are listed below.

Wiki on ATPs

The working group maintains an inventory of theorem provers, which can be found at the GitHub Wiki of this repository.

The wiki is ongoing work towards deliverable D3 see the MoU of COST action CA20111.

License

The contents of this repository are licensed under a Creative Commons Attribution 4.0 International License. Please observe the respective author(s) of the individual page(s).