Email Gateway (Aug 22 2022 at 20:49): Email Gateway (Aug 22 2022 at 20:49):From: Juho Kupiainen <juho.kupiainen.general.ai.group@gmail.com>
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.
Email Gateway (Aug 22 2022 at 20:50):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 22 2022 at 20:50):From: Mark Adams <mark@proof-technologies.com>
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.
Email Gateway (Aug 22 2022 at 20:51):From: mukesh tiwari <mukeshtiwari.iiitm@gmail.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
Last updated: Apr 30 2024 at 16:19 UTC