Re: [isabelle] soundness of Isabelle/HOL



HOL Zero (http://proof-technologies.com/holzero.html) was mentioned already.
HOL Light has had some self-verification applied (
http://www.cl.cam.ac.uk/~jrh13/papers/holhol.html).
Jitawa is a theorem prover verified in HOL (
http://www.cl.cam.ac.uk/~mom22/jitawa/).
For more about the idea you mentioned, parsing "False" as "True", see
Pollack Inconsistency (http://www.cs.ru.nl/~freek/pubs/rap.pdf).

On Mon, Jan 30, 2012 at 10:26 AM, Lars Noschinski <noschinl at in.tum.de>wrote:

> On 30.01.2012 10:59, Matthias Schmalz wrote:
>
>> I already know that Isabelle follows the LCF approach and that HOL is
>> built from a modest number of axioms using conservative extension
>> methods. It is therefore very likely that proofs by Isabelle are
>> correct. I also know that this soundness guarantee is restricted to the
>> inference core; for example, nothing prevents users from configuring the
>> parser to parse "False" as "True" and therefore giving the impression
>> that "False" can be proved. (And of course, soundness rests on the
>> assumption that compiler, ML libraries, operating system, and hardware
>> behave correctly.)
>>
>
> I think HOL Zero tries to make sure that you cannot reconfigure parser and
> pretty-printer in a way that confuses the user. If you search for
> mark at proof-technologies.com on this list, you should find some discussion
> on this topic.
>
>  -- Lars
>
>




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