Re: [isabelle] A small proof checker (String => Bool)

Hi Juho,

The problem is that something that would correctly process an Isabelle theory file and reliably check it would need to be almost as big and complicated as Isabelle itself. The solution is to tweak Isabelle so that, after it processes the theory file, it somehow captures it internally so that it can exported in a much simpler form (a "proof object") that a simple proof checker could process. This simple proof checker would ideally also print out the statements of the theorems it has checked, so that there is no need to trust anything about the original exporting system.

There are various projects that have worked on this idea, including Open Theory, Dedukti and Common HOL (anyone know of any other ones?). I don't know whether anyone got something working reliably for Isabelle theory files, but I don't see any fundamental reason why it couldn't be done.


On 26/10/2019 11:22, Makarius wrote:
On 25/10/2019 17:07, Juho Kupiainen wrote:
How could I go about obtaining a small proof checker for Isabelle HOL, that
takes a theory file and checks that it's valid? I would like it to be
simple to understand and as few lines of code as possible, yet it should include the axioms of the system and be able to check the whole archive of
formal proofs.

It sound like you ask for an "uninformative green light" for your
theories, but that is neither realistic nor useful.

You need to be more specific about what you mean, and what the
application actually context is. So many things can go wrong. You need
to think about what you want to get right in which way.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.