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 (
Jitawa is a theorem prover verified in HOL (
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