[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.