Bootstrapping LCF Declarative Proofs

TL;DR

This paper explores how to efficiently build formal proofs in an LCF system by combining declarative proof styles with automated proof procedures, demonstrated through the ProofPeer theorem prover.

Contribution

It introduces a novel approach to integrating declarative proofs with automated procedures in an LCF-style theorem prover, emphasizing practical verification.

Findings

ProofPeer supports declarative proofs resembling written ones.

Automated proof procedures are effectively integrated outside the kernel.

The approach enhances proof development efficiency and clarity.

Abstract

Suppose we have been sold on the idea that formalised proofs in an LCF system should resemble their written counterparts, and so consist of formulas that only provide signposts for a fully verified proof. To be practical, most of the fully elaborated verification must then be done by way of general purpose proof procedures. Now if these are the only procedures we implement outside the kernel of logical rules, what does the theorem prover look like? We give our account, working from scratch in the ProofPeer theorem prover, making observations about this new setting along the way.