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

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



The answer to this question has lead me to have these following questions:
What logic system is PVS based upon? If you have a logic system with well
defined derivation rules, can you customize PVS to understand those derivation
rules of that system? The system inlcudes rules such as
"modus tollens" and "modus ponens".
Thank you,
Ahmed


On Mon, 23 Apr 2007, Ricky W. Butler wrote:

> 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