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