*To*: Makarius <makarius at sketis.net>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Proof by analogy and proof stability in Isabelle*From*: Dave Thayer <dathayer at microsoft.com>*Date*: Fri, 30 Apr 2010 20:19:10 +0000*Accept-language*: en-US*In-reply-to*: <alpine.LNX.1.10.1004302152410.9376@atbroy100.informatik.tu-muenchen.de>*References*: <6031272389962@web71.yandex.ru> <4BD91699.8020401@in.tum.de> <1272538820.2300.49.camel@weber> <4BD978ED.2000106@in.tum.de> <1272589168.2326.211.camel@weber> <E5D672ED-0FFC-4290-BD8D-E3320379C58E@cam.ac.uk> <l2ucc2478ab1004300745z7f1220c4qbe673b3bad7e61ed@mail.gmail.com> <alpine.LNX.1.10.1004301658460.1774@atbroy100.informatik.tu-muenchen.de> <717F714B587F944C88837A99AA4D00813349CDAF@TK5EX14MBXC116.redmond.corp.microsoft.com> <alpine.LNX.1.10.1004302152410.9376@atbroy100.informatik.tu-muenchen.de>*Thread-index*: AQHK5qNmvmfQ/jOcIkGc86lZh0DtEZI5XtGAgABfkgCAABWmgIAA1M0AgADPc4CAABd1gIAABq6A//+l3LCAAKuIAP//j3/w*Thread-topic*: [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

**References**:**[isabelle] Proof by analogy and proof stability in Isabelle***From:*grechukbogdan

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Tobias Nipkow

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Tjark Weber

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Tobias Nipkow

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Tjark Weber

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Lawrence Paulson

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Brian Huffman

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

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Dave Thayer

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

- Previous by Date: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Next by Date: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Previous by Thread: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Next by Thread: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Cl-isabelle-users April 2010 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