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

Re: Thank you!!!




> 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