Re: [isabelle] Proof by analogy and proof stability in Isabelle
What is the correct invocation to produce such a proof object?
From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Makarius
Sent: Friday, April 30, 2010 1:01 PM
To: isabelle-users at cl.cam.ac.uk
Subject: Re: [isabelle] Proof by analogy and proof stability in Isabelle
On Fri, 30 Apr 2010, Dave Thayer wrote:
> I think an important aspect of this topic is the issue of legal
> liability. If you use a theorem prover to prove a theorem, that is used
> to create a query into a medical ontology, which is then used in the
> diagnostic train for determining a patients treatment protocol you
> better be able to stand up in court and defend it. I would not want to
> tell a judge: "at this step we invoke the magic word 'auto' which does
> 'something unknown' and then we went on from there'.
While Isabelle is a very complex system, internally everything is reduced
to basic principles, and run through an LCF-style inference kernel. The
kernel can also produce explicit proof objects as a backup, although this
degrades performance greatly. Even without proof terms, the type-safety
of Standard ML gives certain static guarantees (in contrast to OCaml, or
other much less rigid languages).
This does not mean that the system only produces ethernally true results
-- there are other influences beyond a certain architecture and properties
of the implementation languages.
Nonetheless, I would characterize our tradition of theorem proving as
"fundamentalist" in the sense that everything is based on proper
definitions and proofs.
This archive was generated by a fusion of
Pipermail (Mailman edition) and