The Proof Certifier Checkers

Different theorem provers work within different formalisms and paradigms, and therefore produce various incompatible proof objects. Currently there is a big effort to establish

foundational proof certificates

(

fpc

), which would serve as a common “specification language” for all these formats. Such framework enables the uniform checking of proof objects from many different theorem provers while relying on a small and trusted kernel to do so.

Checkers

is an implementation of a proof checker using foundational proof certificates. By trusting a small kernel based on (focused) sequent calculus on the one hand and by supporting

fpc

specifications in a prolog-like language on the other hand, it can be used for checking proofs of a wide range of theorem provers. The focus of this paper is on the output of equational resolution theorem provers and for this end, we specify the paramodulation rule. We describe the architecture of

Checkers

and demonstrate how it can be used to check proof objects by supplying the

fpc

specification for a subset of the inferences used by

eprover

and checking proofs using these inferences.