*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 16:48:47 +0000*Accept-language*: en-US*In-reply-to*: <alpine.LNX.1.10.1004301658460.1774@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>*Thread-index*: AQHK5qNmvmfQ/jOcIkGc86lZh0DtEZI5XtGAgABfkgCAABWmgIAA1M0AgADPc4CAABd1gIAABq6A//+l3LA=*Thread-topic*: [isabelle] Proof by analogy and proof stability in Isabelle

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'. David -----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 8:10 AM To: isabelle-users at cl.cam.ac.uk Subject: Re: [isabelle] Proof by analogy and proof stability in Isabelle On Fri, 30 Apr 2010, Brian Huffman wrote: > On occasion I have had significant amounts of trouble getting old proof > scripts to work again. The process is most difficult with theories that > were developed for older versions of Isabelle: Porting a proof directly > from Isabelle 2005 to 2009 can be much more difficult than continuously > adapting the same proof to a series of development snapshots. I would > suspect that most users have to deal with these large version-jumps more > often than the developers do. Jumping over several Isabelle releases at the same time is indeed very hard. Users can avoid that by following the official release schedule -- the distances between Isabelle2007 -- Isabelle2008 -- Isabelle2009 -- Isabelle2009-1 are not too big. Isabelle2005 -- Isabelle2007 is in fact a counter example, with 25 months between the releases and the result being rather unstable. At that time it was not completely clear if we would ever recover from a continously "intermediate" state, and join the fate of notorious projects such as SML/NJ or the STIX fonts. Anyway, one should distinguish between really large libraries and the underlying system infrastructure. A library could well be developed in a Wikipedia style, and people in Nijmegen are working on that, for example. Makarius

**Follow-Ups**:

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

- 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