[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: s_hsson@kaist.ac.kr*Subject*: Re: Thank you!!!*From*: "Dave Stringer-Calvert" <davesc@minster.cs.york.ac.uk>*Date*: Wed, 19 Nov 1997 09:29:10 +0000*Cc*: pvs-help@csl.sri.com*In-Reply-To*: s_hsson@kaist.ac.kr "Thank you!!!" (Nov 19, 3:11pm)*References*: <199711190611.PAA14119@jiri.kaist.ac.kr>

> But, when we try to prove this theory, prover chooses only one of AXIOMS > or THEOREM. > > Could you show me how to prove all of AXIOMS or THEOREM. Ah, I think I know what you're attempting now. When you type M-x prove, the formula currently under the cursor is passed to the theorem prover for you to prove. In your system of axioms, followed by a theorem, I would infer that what you mean is something like: ( t1 AND t2 AND t3 AND t4 ) => t10 That is to say, you are proving the theorem t10, with respect to the given axioms. If this is what you are trying to do, then you should place the cursor over the formula t10, and then do M-x pr. Having, interactively or by copying, given a proof to each formula in a pvs theory, you can use M-x prove-theory to re-run all of the proofs associated with that theory. > In addition, we do not know if it is proper to use THEOREM. Things which you wish to state as facts, use AXIOM. Anything which you wish to try and prove can use any of the keywords THEOREM, LAW, CONJECTURE, LEMMA, CLAIM, COROLLARY, FACT, FORMULA, PROPOSITION, SUBLEMMA (They are all equivalent as far as PVS is concerned). I would suggest you try browsing some of the introductory PVS tutorials for further help: http://www.csl.sri.com/pvs/examples/ Dave -- Dave Stringer-Calvert, MEng MACM, Department of Computer Science, University of York, Heslington, York, YO1 5DD. [+44|0] 1904 432764

**References**:**Thank you!!!***From:*s_hsson@kaist.ac.kr

- Prev by Date:
**Thank you!!!** - Next by Date:
**ADT axioms** - Prev by thread:
**Thank you!!!** - Next by thread:
**Thank you!!!** - Index(es):