Translating between implicit and explicit versions of proof

This page organizes the supporting materials for the paper Translating between implicit and explicit versions of proof by Roberto Blanco, Zakaria Chihani and Dale Miller. Materials are divided in three parts.

• General-purpose checkers and certificate definitions implementing the Foundational Proof Certificate framework, written in λProlog. These include FPC definitions for binary resolution, pairing, and maximally explicit elaborations, among others.

• A checker written in OCaml that does not implement backchaining search nor unification. This checker, called MaxChecker, checks certificates in only the maximally explicit FPC.

• A collection of proofs produced by the Prover9 theorem prover. Instructions are given to use the output from the prover to generate binary resolution certificates (for the λProlog kernel) and supporting declarations (for both λProlog and OCaml checkers). The λProlog checker can then check the theorem against a resolution certificate, and produce a maximally explicit elaboration that can be verified independently by the OCaml checker.

A description of each part follows.