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

Re: [PVS-Help] Prove an axiom?


The theorem prover is always invoked with the first formula that appears
after the current position of the cursor. Move the cursor to the lemmas
and then invoke the theorem prover.


Mark Brown said:
> Hello,
> I'm having trouble with a case where PVS asks me to prove an axiom.  I'm
> working on an example that is posted at
> http://www.csl.sri.com/cgi-bin/pvs/pvs-bug?id=893.  I have copy-pasted
> the kernel theory into a new PVS file.  When I finish typechecking this
> example and run the prover with PVS | Prover Invocation | prove, I am
> presented with a "Rule?" prompt for the separation AXIOM.  The sequent
> PVS wants me to prove has no antecedent and the entire axiom as the only
> succedent.
> What am I missing here?  I was expecting that PVS would simply accept
> the axiom and proceed to help me prove the lemmas derived from this
> axiom.
> Thanks,
> Mark Brown

Cesar A. Munoz H., Senior Staff Scientist
National Institute of Aerospace
100 Exploration Way
Hampton, VA 23666, USA
Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988