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



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
>




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