Davis, Jared Curran.
A self-verifying theorem prover.
Degree: PhD, Computer Sciences, 2009, University of Texas – Austin
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 written more concisely 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.
To establish that the Level 11 proof checker can be trusted, we first use it, without trusting it, to prove the fidelity of every Level n to Level 1: whenever Level n accepts a proof of some phi, there exists a Level 1 proof of phi. 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 Level 2's fidelity, a Level 2 proof of Level 3's fidelity, and so on. This layering shows that each level can be trusted, and allows us to manage the sizes of these proofs.
In this way, our system proves its own fidelity, and trusting Level 11 only requires us to trust Level 1.
Advisors/Committee Members: Moore, J Strother, 1947- (advisor), Emerson, E. Allen (committee member), Harrison, John (committee member), Hunt, Jr., Warren A. (committee member), Kaufmann, Matt (committee member), Lifschitz, Vladimir (committee member).
Subjects/Keywords: Milawa; mathematical logic; formal verification; Lisp; proof checking; theorem proving; automated reasoning; reflection; soundness; fidelity; faithfulness; rewriting; proof building; tactics; first-order logic; verified verifier
…Milawa Functions as Programs .
Supporting Abbreviations . . .
The History… …trusted?
Our theorem prover is named Milawa, and it is probably best regarded as an
“academic… …are not reimplemented in Milawa, including its primitive
type-reasoning, arithmetic… …hypotheses, etc., and overall, The Method is the same.
The Milawa logic is a simple, first… …programming, so it is straightforward to
run Milawa-logic functions as Common Lisp programs. To…
to Zotero / EndNote / Reference
APA (6th Edition):
Davis, J. C. (2009). A self-verifying theorem prover. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/ETD-UT-2009-12-435
Chicago Manual of Style (16th Edition):
Davis, Jared Curran. “A self-verifying theorem prover.” 2009. Doctoral Dissertation, University of Texas – Austin. Accessed February 26, 2021.
MLA Handbook (7th Edition):
Davis, Jared Curran. “A self-verifying theorem prover.” 2009. Web. 26 Feb 2021.
Davis JC. A self-verifying theorem prover. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2009. [cited 2021 Feb 26].
Available from: http://hdl.handle.net/2152/ETD-UT-2009-12-435.
Council of Science Editors:
Davis JC. A self-verifying theorem prover. [Doctoral Dissertation]. University of Texas – Austin; 2009. Available from: http://hdl.handle.net/2152/ETD-UT-2009-12-435