Roger, Yeah rookie mistake there huh? I remember us going over that when we first went over the axioms and their proofs, and I most certainly overlooked the little prime added to the variable name.
I got back to the specification today, and moved on to proving the elevator
state schema, Elevator_State, and I moved the static component elevator to
an axiom, similar to the static components of button. Unfortunately I get a
weird sub goal pop up that says "{} = elevator" after I work on the
existence proof. Is this b/c I used the empty set as the witness to the
elevator axiom proof?
Attached is the exact output from the entire elevator state section and the
specification.
Thanks,
Jon
On Tue, Oct 9, 2012 at 3:52 PM, Roger Bishop Jones <r...@rbjones.com> wrote:
> Jon,
>
> On Tuesday 09 Oct 2012 20:22, Jon Lockhart wrote:
>
> > I am having a little trouble getting the axioms created,
> > moving the static portions of the Button_State to an
> > axiom from the schema. I can't seem to get the proof to
> > operate properly. Any suggestions?
>
> The problem is that the existential goal you are trying to
> prove has decorations on the names of the variables, but the
> witness you have supplied does not.
>
> This is a point of difference between proving the non-
> emptyness of a schema and the consistency of an axiomatic
> specification.
>
> Because the names in the signature of the axiomatic spec
> have already been introduced as global variables (aka
> constants), they cannot be used as the names in the
> existential which must be proven to establish the
> consistency of the axiomatic specification.
> So they get primed.
>
> When z exists tac complains that it can't match the witness
> against the signature of the existential, first check that
> the names you have used in the binding are exactly those in
> the existential you are trying to prove, then check that the
> expressions have the right type.
>
> regards,
> Roger Jones
>
>
elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data
errorEncountered.doc.gz
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
