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

*To*: Ahmed Abdeen* <ahamed@xxxxxxxxxxxxxx>*Subject*: Re: [work] Re: [PVS-Help] Proof By Contradition - How to do thisin PVS?*From*: "Cesar A. Munoz" <munoz@xxxxxxxxxx>*Date*: Mon, 23 Apr 2007 14:58:28 -0400*Cc*: "Cesar A. Munoz" <munoz@xxxxxxxxxx>, "Janney,Mark-P26816" <Mark.Janney@xxxxxxxxx>, pvs-help@xxxxxxxxxxx, "Ricky W. Butler" <R.W.Butler@xxxxxxxxxxxxx>*In-Reply-To*: <Pine.GSO.4.58.0704231435150.4928@school.cs.indiana.edu>*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>*Organization*: NIA*References*: <9D31108D62FAE54AA21AEF899D69931E01F2250B@AZ25EXM04.gddsi.com><6.1.1.1.2.20070423125841.0393a790@pop.larc.nasa.gov><Pine.GSO.4.58.0704231435150.4928@school.cs.indiana.edu>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

A simple clarification: P1 AND P2 => C1 is equivalent to P1 AND P2 AND NOT C1 => FALSE. Indeed, PVS is based on classical higher-order logic (see Chapter 7 of "The Formal Semantics of PVS" for the precise set of rules). Therefore, formulas can be freely moved from the antecedent to the consequent, and viceversa, by negating them. Empty in the antecedent means TRUE, while empty in the consequent means FALSE. The PVS logic system cannot be customized to an arbitrary set of rules. However, particular deductive rules can be implemented as strategies. A proof by contradiction in PVS is not different from a direct proof. Assume that you have [-1] P1 [-2] P2 |----------- [+1] C1 If you type the proof command (case "NOT C1"), you get two sequents [-1] NOT C1 [-2] P1 [-3] P2 |------------ [+1] C1 and [-2] P1 [-3] P2 |------------ [+1] NOT C1 [+2] C1 The first sequent will be automatically transformed by PVS into the original one and the second sequent will be automatically proven by PVS as it's an instance of the excluded middle. Cesar On Mon, 2007-04-23 at 14:36, Ahmed Abdeen* wrote: > 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 -- Cesar A. Munoz H., Senior Staff Scientist mailto:munoz@nianet.org National Institute of Aerospace mailto:C.A.Munoz@larc.nasa.gov 100 Exploration Way, Room 214 http://research.nianet.org/~munoz Hampton, VA 23666, USA Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988 GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6 1A18 6000 89F5 C114 E6C4

**References**:**[PVS-Help] Proof By Contradition - How to do this in PVS?***From:*Janney, Mark-P26816

**Re: [PVS-Help] Proof By Contradition - How to do this in PVS?***From:*Ricky W. Butler

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

- Prev by Date:
**Re: [PVS-Help] Proof By Contradition - How to do this in PVS?** - Next by Date:
**[PVS-Help] PVS bugs 968, 948, and 978** - Prev by thread:
**Re: [PVS-Help] Proof By Contradition - How to do this in PVS?** - Next by thread:
**[PVS-Help] question about the list adt** - Index(es):