Re: [isabelle] Isabelle Foundation & Certification



Dear Larry, 

You wrote: 
>> I'd like to point out again that users need to take responsibility for their own definitions. I regularly see proofs that are valueless because they are based on incorrect definitions.  
>> To my mind, a soundness bug is when a valid expression or proof state is transformed into something wrong. The problem identified here are that Isabelle is failing to prohibit certain definitions that don't 
>> make sense. There is no claim that Isabelle is doing anything wrong with these definitions. It's hard to believe that a user could make such definitions accidentally.

Your position here puzzles me now as much as it did the last time we talked about this. Let's forget about Isabelle/HOL for a second, and think of a logic L with axioms and deduction rules, but no definitions. 
Further, assume that L is known, or strongly believed to be consistent, in that it does not prove False. Now consider L_D, the logic L augmented with definitional mechanisms. This augmented logic should of course not prove False either! Writing meaningful definitions is the user's responsibility, but having the definitions consistent is the logic L_D's responsibility. Guaranteed consistency distinguishes definitions from arbitrary new axioms -- I learned this years ago from your papers and books.      

You wrote: 
>> It would be interesting to find out how these problems were identified: whether they were looked for out of curiosity, or whether on the other hand they manifested themselves 
>> in the course of an actual proof.

Ondra discovered the typedef inconsistency, so he is the best person to answer this. 

All the best, 
   Andrei 
 



---------------------------------------------------------------------------


Please note that Middlesex University's preferred way of receiving all correspondence is via email in line with our Environmental Policy. All incoming post to Middlesex University is opened and scanned by our digital document handler, CDS, and then emailed to the recipient.

If you do not want your correspondence to Middlesex University processed in this way please email the recipient directly. Parcels, couriered items and recorded delivery items will not be opened or scanned by CDS.  There are items which are "exceptions" which will be opened by CDS but will not be scanned a full list of these can be obtained by contacting the University.





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