Proof Outlines as Proof Certificates: A System Description
Roberto Blanco (Inria, LIX), Dale Miller (Inria, LIX)

TL;DR
This paper introduces a framework for designing and verifying high-level proof outlines using proof certificates, enabling automated expansion into detailed proofs with a specialized proof checker system.
Contribution
It applies the foundational proof certificate framework to proof outlining and demonstrates proof reconstruction through a dedicated proof checker system.
Findings
Successfully designed proof outlines that can be expanded into full proofs
Validated the approach with the ACheck system for theorem sequences
Showed the feasibility of proof reconstruction from outlines
Abstract
We apply the foundational proof certificate (FPC) framework to the problem of designing high-level outlines of proofs. The FPC framework provides a means to formally define and check a wide range of proof evidence. A focused proof system is central to this framework and such a proof system provides an interesting approach to proof reconstruction during the process of proof checking (relying on an underlying logic programming implementation). Here, we illustrate how the FPC framework can be used to design proof outlines and then to exploit proof checkers as a means for expanding outlines into fully detailed proofs. In order to validate this approach to proof outlines, we have built the ACheck system that allows us to take a sequence of theorems and apply the proof outline "do the obvious induction and close the proof using previously proved lemmas".
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
