Re: [ProofPower] Z Schemas - Help with Initialization and Precondition calculus
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 yourself. 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!) regards, Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Z Schemas - Help with Initialization and Precondition calculus
Roger, When I execute: a (REPEAT z_strip_tac THEN POP_ASM_T ante_tac THEN asm_rewrite_tac[]); ProofPower returns the following message: :# :# Exception- Fail * the assumption list is empty [POP_ASM_T.9302] * raised Exception+ Fail * the assumption list is empty [POP_ASM_T.9302] * raised Is everything fine? Artur 2009/3/24 Roger Bishop Jones r...@rbjones.com Artur, On Tuesday 24 March 2009 10:35:51 Artur Oliveira Gomes wrote: The problem is: only for those cases, what I choose as witness does not satisfy the predicate. Well, any sequence of length 1 (or zero?) does for the first case. Proof attached. If you still can't crack the other two send me your best attempt. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com -- Artur Oliveira Gomes ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Z Schemas - Help with Initialization and Precondition calculus
Hi there, 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. Best, -- Artur Oliveira Gomes examples.doc Description: MS-Word document ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
