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

Re: [PVS-Help] Proof By Contradition - How to do this in PVS?



Mark,
   Consider the sequent is

  [-1]  P1
  [-2]  P2
  |-----------
   [+1]   C1

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

R

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.

It's not clear to me how to accomplish this in the PVS prover.  Any suggestions would be most welcome.

Thanks - Mark Janney

Ricky W. Butler
NASA Langley Research Center
Hampton, VA  23681-2199
R.W.Butler@larc.nasa.gov
http://shemesh.larc.nasa.gov/fm/
phone: 757-864-6198
fax: 757-864-4234