[Back]

G. Reger, M. Suda:
"Checkable Proofs for First-Order Theorem Proving";
Talk: The First International ARCADE (Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements) Workshop, Gothenburg, Sweden; 2017-08-06; in: "ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements", EasyChair EPiC Series in Computing, Volume 51 (2017), 55 - 63.

Inspired by the success of the DRAT proof format for certification of boolean satisfiability (SAT),
we argue that a similar goal of having unified automatically checkable proofs should be sought
by the developers of automated first-order theorem provers (ATPs). This would not only
help to further increase assurance about the correctness of prover results,
but would also be indispensable for tools which rely on ATPs,
such as ``hammers" employed within interactive theorem provers.
The current situation, represented by the TSTP format is unsatisfactory,
because this format does not have a standardised semantics and thus cannot be checked automatically.
Providing such semantics, however, is a challenging endeavour. One would ideally
like to have a proof format which covers only-satisfiability-preserving operations such as Skolemisation
and is versatile enough to encompass various proving methods (i.e. not just superposition)
or is perhaps even open ended towards yet to be conceived methods or at least easily extendable in principle.
Going beyond pure first-order logic to theory reasoning in the style of SMT or
beyond proofs to certification of satisfiability are further interesting challenges.
Although several projects have already provided partial solutions in this direction,
we would like to use the opportunity of ARCADE to further promote the idea and
gather critical mass needed for its satisfactory realisation.

theorem proving, proof checking, first-order logic

http://publik.tuwien.ac.at/files/publik_264652.pdf