[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Proof By Contradition - How to do this in PVS?
Consider the sequent is
This is equivalent to
P1 AND P2 => C1
which is equivalent to
P1 AND P2 AND NOT C1 => TRUE
If you can create a contradiction among the premises,
the sequent is proved.
So in effect proof by contradiction is handled automatically.
You have to get used to the idea that you can move a premise
from + to - side or vice versa if you negate it. In fact PVS
does this with an expression that begins with NOT.
You could split the proof into two pieces by introducing a
case expression, e.g.
(case "NOT C1")
This will produce two subgoals, which might help you
think this through.
At 06:40 PM 4/20/2007, Janney, Mark-P26816 wrote:
I'm trying to
reconstruct a manual proof that used proof by contradition, i.e assume
the negation of your thesis and then derive a contradition.
Ricky W. Butler
It's not clear to me how to accomplish this in the PVS
prover. Any suggestions would be most welcome.
Thanks - Mark Janney
NASA Langley Research Center
Hampton, VA 23681-2199