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

*To*: "Janney, Mark-P26816" <Mark.Janney@xxxxxxxxx>, <pvs-help@xxxxxxxxxxx>*Subject*: Re: [PVS-Help] Proof By Contradition - How to do this in PVS?*From*: "Ricky W. Butler" <R.W.Butler@xxxxxxxxxxxxx>*Date*: Mon, 23 Apr 2007 13:07:39 -0400*In-Reply-To*: <9D31108D62FAE54AA21AEF899D69931E01F2250B@AZ25EXM04.gddsi.com>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <9D31108D62FAE54AA21AEF899D69931E01F2250B@AZ25EXM04.gddsi.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

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

- Prev by Date:
**[PVS-Help] Proof By Contradition - How to do this in PVS?** - Next by Date:
**Re: [PVS-Help] Proof By Contradition - How to do this in PVS?** - Prev by thread:
**[PVS-Help] Proof By Contradition - How to do this in PVS?** - Next by thread:
**Re: [PVS-Help] Proof By Contradition - How to do this in PVS?** - Index(es):