Jon,

On 13/09/12 04:16, Jon Lockhart wrote:
Are you saying then for the Boolean block I have to just replace it with
the one that you have provided in the email?


Not only would you have to replace the Boolean block but also remove the integer comparison around the references to Boolean global variables. For example, the predicate

  masterStop = 0

must be changed to either

  ¬ masterStop

or

  masterStop = False


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.

To use this is very simple for the most part. In a predicate context, just treat Boolean expressions as though they were predicates. In an expression context, Boolean expressions can be combined to give other Boolean expressions as you would expect, e.g. a ∧ b. However, to create a Boolean expression from a predicate p, you need to write

  [ | p]

It is probably worth understanding what is going on at least once. It is easiest to think in terms of sets. A schema is just a set of bindings. The empty schema [], which is the same as [ | true], is a set containing just the empty binding, i.e. {()}. So [] is much like the SML type 'unit', a type that has only one value. Thus Boolean is the set {{}, {()}} where {} represents false and {()} represents true, hence our definition of True and False. So an expression of type Boolean is a schema. When a schema S is used as a predicate, the predicate is θS ∈ S. For one of our Boolean expressions B as a predicate, the predicate is θB ∈ B which is equivalent to () ∈ B. So you can see how the corresponding predicate is derived.


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.

If you feel inclined to try the latest patch, it is here, with instructions:
http://www.lemma-one.com/ProofPower/patches/patches.html

I'm fairly familiar with the installation process, so it only takes me a few minutes to build a patched version. However, a new release may be around the corner - I don't know what Rob's plans are there.


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?

I see what you mean. Yes, for an axiomatic description, one wants to be sure that it is not introducing a contradiction into the theory, making the theory inconsistent. ProofPower has a mode of operation where it does not assume such axioms are consistent until they have been proved consistent. This works by showing that each axiom is a conservative extension to the theory, i.e. does not introduce an inconsistency.

For Z, at the start of your theory, you would do

  set_flag ("z_use_axioms", false);

Note, then, that z_get_spec does not simply give you the axiom as a theorem. After an axiomatic description paragraph, start a consistency proof with e.g.

  z_push_consistency_goal %SZT%minNumberFloors%>%;

See section 5.3, page 93, of usr011.dvi for examples.

Phil


_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to