*To*: OndÅej KunÄar <kuncar at in.tum.de>, Lawrence Paulson <lp15 at cam.ac.uk>, Ken Kubota <mail at kenkubota.de>*Subject*: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu*From*: Makarius <makarius at sketis.net>*Date*: Sun, 21 Aug 2016 22:55:14 +0200*Cc*: Andrei Popescu <A.Popescu at mdx.ac.uk>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <9f07313f-afdc-aeb1-a51f-52bf84a7421e@in.tum.de>*References*: <CDD6C40D-96BE-46B5-99F1-C9C35A8CE6D6@kenkubota.de> <C5CAD6F5-6760-4704-A5CF-89C0FB06F053@cam.ac.uk> <9f07313f-afdc-aeb1-a51f-52bf84a7421e@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

On 21.08.2016 21:41, OndÅej KunÄar wrote:

I guess the whole discrepancy boils down to the question ifdefinitions are part of logical reasoning. For me, this is the casesince you can view definitions as the following inference rule:T ----------- [side conditions] T' |- c = tAnd if "c = t" allows you to prove False, then I call it aninconsistency.

I don't find distinguishing between theorems stemming from axioms (and"pure" logical reasoning) and between theorems stemming fromdefinitions particularly enlightening.

While itâs right that they have fixed this problem, nobody had actually exploited it, and the fix had no effect on the millions of lines of Isabelle proofs in existence.

You are right. As far as I know, this was the case for any problems(either implementation bugs or more substantial problems) that werefound in other provers. But does this mean we should resign oninspecting and improving our kernels/logics? I hope not.

Makarius

**References**:**[isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu***From:*Ken Kubota

**Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu***From:*Lawrence Paulson

**Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu***From:*OndÅej KunÄar

- Previous by Date: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Next by Date: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Previous by Thread: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Next by Thread: [isabelle] Abbreviation makes Isabelle/HOL very slow
- Cl-isabelle-users August 2016 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