*To*: Mark Adams <mark at proof-technologies.com>*Subject*: Re: [isabelle] A small proof checker (String => Bool)*From*: mukesh tiwari <mukeshtiwari.iiitm at gmail.com>*Date*: Tue, 29 Oct 2019 11:01:42 +1100*Cc*: isabelle-users at cl.cam.ac.uk, Makarius <makarius at sketis.net>, Juho Kupiainen <juho.kupiainen.general.ai.group at gmail.com>*In-reply-to*: <8c5043f0e7fa4d5b578ffb5e3aad6158@proof-technologies.com>*References*: <CADnKKmJX6c2SK-aOTm6aLYMMyjk94U+0_btp1HTEth4ENpozBw@mail.gmail.com> <c023779c-0068-c89c-5a29-6d807c97f9de@sketis.net> <8c5043f0e7fa4d5b578ffb5e3aad6158@proof-technologies.com>

Hi Everyone, I was also looking for answer for this question and ended up finding a couple of proof checker HOL-Zero [1], Coqchk [2] (I believe it's the extracted code from [3], but I am not sure), and reference Lean checker [4]. [1] http://www.proof-technologies.com/holzero/ [2] https://coq.inria.fr/refman/practical-tools/coq-commands.html#compiled-libraries-checker-coqchk [3] https://github.com/coq-contribs/coq-in-coq [4] https://github.com/leanprover/tc On Tue, Oct 29, 2019 at 6:09 AM Mark Adams <mark at proof-technologies.com> wrote: > > 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. > > Mark. > > 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. > > > > > > Makarius >

**References**:**[isabelle] A small proof checker (String => Bool)***From:*Juho Kupiainen

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

**Re: [isabelle] A small proof checker (String => Bool)***From:*Mark Adams

- Previous by Date: Re: [isabelle] A small proof checker (String => Bool)
- Next by Date: [isabelle] Isabelle under NetBSD Linux emulation
- Previous by Thread: Re: [isabelle] A small proof checker (String => Bool)
- Next by Thread: [isabelle] Unfortunate duplicate name
- Cl-isabelle-users October 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list