CISA Seminar: Phil Scott What CISA Seminar When Apr 25, 2016 from 02:00 PM to 03:00 PM Where IF 4.31/4.33 Add event to calendar vCal iCal 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. Apr 25 2016 14.00 - 15.00 CISA Seminar: Phil Scott Bootstrapping LCF Declarative Proofs IF 4.31/4.33
CISA Seminar: Phil Scott What CISA Seminar When Apr 25, 2016 from 02:00 PM to 03:00 PM Where IF 4.31/4.33 Add event to calendar vCal iCal 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. Apr 25 2016 14.00 - 15.00 CISA Seminar: Phil Scott Bootstrapping LCF Declarative Proofs IF 4.31/4.33
