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

[PVS-Help] Prove an axiom?


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.


Mark Brown