Re: [isabelle] soundness of Isabelle/HOL

HOL Zero ( was mentioned already.
HOL Light has had some self-verification applied (
Jitawa is a theorem prover verified in HOL (
For more about the idea you mentioned, parsing "False" as "True", see
Pollack Inconsistency (

On Mon, Jan 30, 2012 at 10:26 AM, Lars Noschinski <noschinl at>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 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.