Re: [isabelle] Proof by analogy and proof stability in Isabelle



What is the correct invocation to produce such a proof object?

-----Original Message-----
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.


 	Makarius







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