Re: [isabelle] soundness of Isabelle/HOL



Sorry - Jitawa is the verified runtime. The self-verifying prover on top of
it is called Milawa (http://www.cs.utexas.edu/~jared/milawa/Web/).

On Mon, Jan 30, 2012 at 10:45 AM, Ramana Kumar <rk436 at cam.ac.uk> wrote:

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