*To*: "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*: Makarius <makarius at sketis.net>*Date*: Fri, 30 Apr 2010 22:01:08 +0200 (CEST)*In-reply-to*: <717F714B587F944C88837A99AA4D00813349CDAF@TK5EX14MBXC116.redmond.corp.microsoft.com>*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>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Fri, 30 Apr 2010, Dave Thayer wrote:

I think an important aspect of this topic is the issue of legalliability. If you use a theorem prover to prove a theorem, that is usedto create a query into a medical ontology, which is then used in thediagnostic train for determining a patients treatment protocol youbetter be able to stand up in court and defend it. I would not want totell a judge: "at this step we invoke the magic word 'auto' which does'something unknown' and then we went on from there'.

Makarius

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

**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

- 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