*To*: Mark <mark at proof-technologies.com>*Subject*: Re: [isabelle] Need a "What's the foundation of Theory.thy" utility*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Tue, 09 Jul 2013 22:45:58 -0500*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1373405593778@names.co.uk>*References*: <1373405593778@names.co.uk>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Mark,

Like I said to Ramana, even a third-party verifier like yours needs to be able to give a basic report on what foundation is being used. If all I'm interested in is standard HOL, then I want to know as fast as possible whether someone's using standard HOL.Can you spell out in what sense HOL Zero does not meet your aims on this? I'm eager to hear about any ideas for improving it.

On 7/9/2013 4:33 PM, "Mark" wrote:

Hi Gottfried, I think you're advocating the "proof auditing" idea that I've been trying to push in recent years.

Do you envisage that this utility would have a human aspect to its usage, reviewing that the reported foundation is good ....No, it's only to list anything that's being used in the theory and language that's either axiomatic, or might be axiomatic.By "axiomatic" are you referring to any HOL axioms, constant definitions, type definitions, etc (i.e. what I call "assertions", which is what mathematicians call "axioms") made in the theory, or are you referring to just HOL axioms (i.e. the completely unrestricted form of HOL assertion)?

As far as types, there is this statement in isar-ref.pdf: If you introduce a new type axiomatically, i.e. via typedecl and axiomatization, the minimum requirement is that it has a non-empty model, to avoid immediate collapse of the HOL logic.

Don't you mean "yes" as the answer to my quesion? Surely whatever foundation is being printed out by the utility needs to be examined in detail, with all its subtlety, by a human to make sure it's good foundation rather than nonsense. This is not a 10 seconds exercise, even with the most user-friendly utility imaginable.

Also, it would do some easy checks to rule out the possibility of a person doing sneaky things, like doing checksum comparisons on third-party files a person is distributing with their theory, where the local third-party files would be obtained from the original source.I don't get what you're talking about here with checksums. Is this used by Isabelle or something?

If someone writes 100,000 lines of source and at the end claims to prove the Riemann Conjecture, the first thing you want to know is what's in their THY that's axiomatic, or can't be determined to be axiomatic. The utility is to give you that information fast.This really does sound like a tool for supporting proof auditing.

If someone's not using anything axiomatic beyond what Complex_Main gives them in Isabelle, then their doing stupid stuff like trying to fool people with deceptive notation still wouldn't allow them to prove something that's not true. It would just appear to be something different on the surface. The statement of a theorem after 50,000 lines of source is always going to take some effort to figure out what it proves. The utility is to let you know what the limitations there are to the foundation.That's right, the proof audit should only examine what's been used. Intermediate stuff is irrelevant if it doesn't get used. Specifically you need to be examining all axioms and definitions that get used in the proof of the supposed theorem.

Right now I'm speculating that when ML is used in Isar, it can't be determined that the ML does something axiomatic unless you inspect the ML, but I wouldn't know, which is the purpose of the utility, to get an official report on what the foundation is.Yes, this is where proof porting comes in. Ideally you want to be able to port the proof object to a target system (using proof recording), replay the proof and examine what axioms and definitions are getting used. HOL Zero is specifically designed for this target system role, of course. It is more trustworthy than any other system (although some people seem to disagree..). And it has the 'get_all_axioms', 'get_all_const_definitions', 'get_all_const_specifications' and 'get_all_tyconst_definitions' commands, primarily to help proof auditing. These reveal what gets used in the ported proof, because the base HOL Zero system has so little theory itself.

Regards, GB

**References**:

- Previous by Date: Re: [isabelle] Need a "What's the foundation of Theory.thy" utility
- Next by Date: [isabelle] PhD Position on SMT Reasoning at Uppsala University
- Previous by Thread: Re: [isabelle] Need a "What's the foundation of Theory.thy" utility
- Next by Thread: Re: [isabelle] Need a "What's the foundation of Theory.thy" utility
- Cl-isabelle-users July 2013 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