*To*: Matthias.Schmalz at inf.ethz.ch*Subject*: Re: [isabelle] soundness of Isabelle/HOL*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Mon, 30 Jan 2012 10:48:04 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAMej=27xPBHN5aNBVsj4iLR49iWNW4J5NdP+pEeNHdQ1NTr=xA@mail.gmail.com>*References*: <4F266A0F.8000906@inf.ethz.ch> <4F267057.5090906@in.tum.de> <CAMej=27xPBHN5aNBVsj4iLR49iWNW4J5NdP+pEeNHdQ1NTr=xA@mail.gmail.com>*Sender*: ramana.kumar at gmail.com

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

**References**:**[isabelle] soundness of Isabelle/HOL***From:*Matthias Schmalz

**Re: [isabelle] soundness of Isabelle/HOL***From:*Lars Noschinski

**Re: [isabelle] soundness of Isabelle/HOL***From:*Ramana Kumar

- Previous by Date: Re: [isabelle] soundness of Isabelle/HOL
- Next by Date: Re: [isabelle] soundness of Isabelle/HOL
- Previous by Thread: Re: [isabelle] soundness of Isabelle/HOL
- Next by Thread: Re: [isabelle] soundness of Isabelle/HOL
- Cl-isabelle-users January 2012 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