Date: Mon, 14 Nov 2005 21:49:55 -0600 From: Jared Davis Hi, At this week's meeting I will present some preliminary work on developing a trustworthy and capable proof checker for an ACL2-like logic. We begin by writing a small proof checker which is so simple that we can make a strong argument for its correctness. But this program is so limited that actually using it to check proofs would be too tedious; the proofs we would have to write would be too long. In other words, this program is trustworthy but not capable. We want to keep this level of trust while adding capabilities. We create an extended proof checker which adds a new derived rule of inference as a primitive. This new checker is more complicated than the baby checker, but it is also more capable and proofs for it are shorter. Since both checkers are written in ACL2, we can prove that the only formulas which are provable in the extended checker are also provable in the baby checker. That is, if the baby checker is sound, then so is the extended checker. We can repeat this process to show, in ACL2, that a sequence of increasingly capable proof checkers are sound with respect to the simplest checker. The challenge is to do better than this; we would like to prove the extension is sound using the baby proof checker itself. Then, we only need to trust the baby checker, and not all of ACL2. Iterating this process we can perhaps construct a reasonably capable proof checker which is as trustworthy as the simplest checker. Such a checker could be soundly extended by users in arbitrary ways, and could perhaps be efficient enough to check interesting proofs. Hope to see you there, Jared