On Tuesday 24 March 2009 05:07:09 Artur Oliveira Gomes wrote:

>I'm having hard times to achieve some proofs of preciondition
>and initialization using ProofPower.
>The file attached contains 3 examples that I still can not prove.
>If anyone could help me out with those proofs, I will be thankful.

These are all existential conjectures.

ProofPower is sometimes quite dumb about these things
(sometimes quite smart), it only really knows about
the kinds of existential proofs which are necessary
for proving consistency of things like recursive
definitions (and that stuff only really works for HOL
its not so good in Z).  So usually you will have to
come up with a witness for the existential goal

In the case of an existential with a schema as the
signature the witness will usually be a binding
display.  So for each of your proofs you must
come up with the binding display of a witness
for your conjecture, i.e. a binding which satisfies
the body of the existential, and then offer it up
using exists-tac.  Then you have to prove that
your witness does satisfy the predicate.

(I didn't check whether you are trying to prove
the right thing!)

Roger Jones

Proofpower mailing list

Reply via email to