[FOM] Talk on Formal Verification

[Mario Carneiro]

On Thu, Jan 28, 2016 at 10:02 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> A more skilled and capable user will naturally find more direct and
> simpler proofs. The software is also critically important, because the
> length of a proof in terms of primitive inferences really is unbearable;
> the software has to provide plenty of automation so that only the creative
> steps are visible.
>

I would like to amend this statement, as someone who works with the
Metamath theorem verification software, which has almost no automation and
yet still can produce reasonably sized proofs. The key is that it is
possible to write and reuse theorems, including new inference rules, based
on the primitive rules (of propositional and predicate logic and ZFC). Even
showing all these "non-creative" propositional manipulation steps (and I
don't know if it is even fair to categorize these as non-creative) the
proof blowup factor is no more than 2 to 5 over something which handles the
FOL component by automation like Mizar or Isabelle.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160129/541347dc/attachment.html>