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



This question is a perfect example why I dislike the use of the word âinconsistency" in connection with the work of KunÄar and Popescu. Probably most people associate that word with some sort of incorrect logical reasoning. However, their work is concerned with Isabelle's automatic detection and rejection of circular definitions. Obvious ones such as x == x+1 and i==j, j==i+1 have been rejected for many years, but they found some cases where a very devious user could sneak a circular definition through. 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. 

And itâs worth stressing again: even consistent definitions can be wrong.

Larry Paulson


> On 20 Aug 2016, at 17:29, Ken Kubota <mail at kenkubota.de> wrote:
> 
> Which restriction was introduced in Isabelle (2016) in order to avoid the inconsistency of earlier versions revealed by KunÄar/Popescu? 





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