Re: [ProofPower] ProofPower Update
Rob, Sorry for the slow response. I have thought quite a bit about this, but these days such cogitations don't always go anywhere useful. On Thursday 30 Aug 2012 21:58, Rob Arthan wrote: On 11 Aug 2012, at 15:07, Roger Bishop Jones wrote: and a number of cases where identifiers which I had been using are now used in MathsEgs theories which are in my ancestry these include Tree TREE Pair Were you using these names for things of your own? Yes. If so, then perhaps this would be solved if the underlying names of constants were prefixed with the theory name. What I am considering in this area is an option controlled by a flag (say structured_HOL_namespace), which I would turn on towards the end of the HOL build, whereby the HOL parser would do this for you. When you define constant xyz in theory abc, the underlying name would be xyz.abc and abc would be introduced as an alias for that. And likewise for types. This behaviour would be optional and language-specific (e.g., you wouldn't want it for Z, and you might not want it in HOL). Would that have saved you any trouble? I don't think my problems with the new version of maths_egs are of any concern, and don't for me motivate changes. I do think changes in this area are desirable but I would say that my own prime motivation would be to move to a situation in which proof tools can make use of results obtained in other proof tools, i.e. the motivations for OpenTheory and my X-Logic. I think being able to eliminate junk from theories is something which would help in that enterprise, and as it happens it would probably would also help to mange the above kind of problem. I think that probably would involve using compound constant names, at least behind the scenes, not necessarily in front of the children. But I'm not keen on the use of the ProofPower aliasing mechanism to manage the use of simple names. A key feature I think is simply to be able to hide names, or project a theory according to a signature, but also it would be nice to be able to rename on import. I am inclined now to think that it might have been a mistake to automatically inherit all the ancestry when adding a parent. This connects with the discussion about conservative extension, since it represents an alternative way of obtaining the kind of abstraction which new_specification provides, and possibly somewhat superior in that the details are all there, but not actually exported. Putting it in that context, the idea that the structured namespace is something you opt into at some point seems to me doubtfull, though you might want it to default to behaviour which is backward compatible, i.e. if the local names are all globally unique then they will all get correctly resolved as at present. However, once you put it in this context, then you are really looking at a bigger problem in which concensus across theorem provers is essential. Personally, I think that shouldn't just be HOL provers, and as you know I advocate importing results even if proofs cannot be imported. As an example of what ideally might be possible, classical arithmetic is standard, no two provers should disagree about what is true (though they will differ about what they can prove), so exchange across any tool which is sound for first order arithmetic should be possible in that domain. All that of course is much more than you wanted to get into, and for my money you can safely do nothing here if your concern is just the occasional rework that people might have to do when you change maths_egs. (probably the most disruptive) and some identifiers consisting of or starting with subscripted D. Really - I can't find any identifiers that start with a subscripted character in the MathsEgs theories. The theory is topology which now contains some names which are the same as names you put into a bit of differential geometry you did for me way back. I have not yet considered a new way of building contribs. I feel that making MathsEgs build OK on the development system would not be productive in the absence of a little more clarity about how a contrib system would be expected to work. I had a discussion with Anthony Fox about how they do things in HOL4 and that has given me some more ideas on this. I think it is actually completely orthogonal to how the ProofPower code is organised. Yes. I got confused when you issues the trial reorganisation and tried to build maths_egs out of the RCS, which didn't work, but it did build in the normal way of course. In HOL4, the contents of a theory are exported to and imported from text files. So if you have code associated with a theory that you want to export to users of the theory, you put that in a separate file and let users load that file. As ML doesn't have separate compilation, such code has to be provided as source. To make things easier for the user, HOL4 has its own make function,
[ProofPower] Best platform for ProofPower?
I'm having bad luck lately getting suitable environments for running ProofPower. My laptop is on Ubuntu 10.4, and that is fine for ProofPower, but is now so out of date that I can't upgrade it, I would have to install a more recent version of Ubuntu from scratch. So I revived an old server to try out a more up-to-date context for running ProofPower. (my efforts in the amazon cloud ran into the buffers some time ago). So far I'm not having much success on Ubuntu 12.04 (the PolyML build doesn't seem to work for me). I'm interested to know what people are actually running ProofPower on these days? Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trying to Prove my Zed Specifications
Jon,
On 13/09/12 00:24, Jon Lockhart wrote:
Unfortunately the two extra sets I want to
declare and add to the spec are causing parser errors in ProofPower. The
sets I am trying to declare are TIMER == 0..5 and BOOLEAN == {0, 1}
which is allowed in the normal standard and has been syntactically
cleared by FUZZ and CZT through Anthony's Z Word Tools. Unfortunately
ProofPower doesn't allow me to do such a thing and I am wondering what
would be the proper protocol for adding such sets to a specification in
ProofPower.
These work in the version I have, 2.9.1w2.rda.120805, the latest patch
which fixes the recent Xpp issue. (Generally it would be useful to see
the error message you get.) ProofPower used to require ≜ (hat-equals)
for an abbreviation definition but a recent patch allows the standard ==
to be used. If you are using the 'current release' 2.9.1w2, == is not
supported. Can you check the version of ProofPower in the banner that
is shown when it starts?
My second question derives from this where right after the
sets I list some axioms which are used to hold globals which I use in
operations throughout the rest of my specification. They rely on the
boolean set I just created or are just parameters for the sets in
general. How would one go about proofing these or is it even necessary?
I'm not sure I understand the question. The axiomatic description
involving masterStop and masterReset is referring to the global variable
BOOLEAN that was defined to be 0 .. 5 earlier. The constraint holds
throughout the theory and is obtained as a theorem by
z_get_spec %SZT%masterStop%%
Phil
P.S. A better way to define booleans in Z is as follows:
BOOLEAN == ℙ []
True == [ | true]
False == [ | false]
This is standard Z. I don't know whether FuZZ accepts empty schemas.
The main advantage is that the usual logical connectives can be used
with such boolean expressions and the implicit conversion of schemas as
predicates allows such a boolean expressions to be used where a
predicate is required, and giving the expected predicate value. The
specification is more readable as a result. For example, your expression
if (elevatorRightHeading? = 1 ∧ elevatorGoingToFloor? = 1) then ...
could just be
if elevatorRightHeading? ∧ elevatorGoingToFloor? then ...
To negate a value one can write
¬ elevatorRightHeading?
rather than encouraging numerical tricks like
(1 - elevatorRightHeading?)
Note also that [] is a maximal set, so ℙ [] is too. Consequently type
checking ensures that such boolean values can take no other values.
Using BOOLEAN == {0, 1}, the constraint is a semantic one: type checking
will not reject e.g.
elevatorRightHeading? = 2
which, presumably, would be a mistake.
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trying to Prove my Zed Specifications
On 13/09/12 02:47, Phil Clayton wrote:
BOOLEAN that was defined to be 0 .. 5
I meant to say {0, 1}, of course!
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trying to Prove my Zed Specifications
Phil,
Are you saying then for the Boolean block I have to just replace it with
the one that you have provided in the email? Seems odd to be to just
through True and False in there like that where I am describing sets but if
it works, then I am all for it, I just need to see or understand how to use
it properly.
As for the version of ProofPower, I have version 2.9.1w2, which is what you
were saying does not support ==. Looks like I might have to update here
when the latest stable version is released on the site.
What I was saying on the masterStop / masterReset axiom, along with the
minNumberFloors, maxNumberFloors, etc axioms, since I am using those as
global variables essentially, is how do I prove them and preconditions on
them like I have down for my States so far? Is is necessary too, or if I
just get the spec of them they are already shown to be theorems?
Thanks,
Jon Lockhart
On Wed, Sep 12, 2012 at 9:53 PM, Phil Clayton phil.clay...@lineone.netwrote:
On 13/09/12 02:47, Phil Clayton wrote:
BOOLEAN that was defined to be 0 .. 5
I meant to say {0, 1}, of course!
__**_
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**comhttp://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
