From: "Jared C. Davis" Date: Mon, 14 Sep 2009 22:47:04 -0500 Subject: [acl2-mtg] This week in ACL2 Hi, At this week's ACL2 seminar I'll give a practice talk for my defense (which is this Friday). I've included the abstract, below. Since there will be some extra time I will be happy to answer any hard questions, but please save any easy questions for Friday. :) Hope to see you there, Jared Ph.D. Final Oral Defense: Jared Davis Date: September 18 Location: TAY 3.128 Time: 12:00 Noon Supervising Professor: J Moore Title: A Self-Verifying Theorem Prover Abstract: Programs have precise semantics, so we can use mathematical proof to establish their properties. These proofs are often too large to validate with the usual "social process" of mathematics, so instead we create and check them with theorem-proving software. This software must be advanced enough to make the proof process tractable, but this very sophistication casts doubt upon the whole enterprise: who verifies the verifier? We begin with a simple proof checker, Level 1, that only accepts proofs composed of the most primitive steps, like Instantiation and Cut. This program is so straightforward the ordinary, social process can establish its soundness and the consistency of the logical theory it implements (so we know theorems are "always true"). Next, we develop a series of increasingly capable proof checkers, Level 2, Level 3, etc. Each new proof checker accepts new kinds of proof steps which were not accepted in the previous levels. By taking advantage of these new proof steps, higher-level proofs can be more concise than lower-level proofs, and can take less time to construct and check. Our highest-level proof checker, Level 11, can be thought of as a simplified version of the ACL2 or NQTHM theorem provers. One contribution of this work is to show how such systems can be verified. We say Level n is sound if, whenever it accepts a proof of some formula, phi, there exists a Level 1 proof of phi. To establish that the Level 11 proof checker can be trusted, we first use it, without trusting it, to prove that every level is sound. We then mechanically translate the Level 11 proof for each Level n into a Level n-1 proof. That is, we create a Level 1 proof of soundness for Level 2, a Level 2 proof of soundness for Level 3, and so on. This layering shows that each level can be trusted, and allows us to manage the sizes of these soundness proofs. In this way, our system proves its own soundness, and trusting the entire system only requires us to trust Level 1.