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

*To*: CHEN Chunqing <chenchun@xxxxxxxxxxxxxxx>*Subject*: Re: [PVS-Help] what to do when consequents are logically opposite*From*: Sam Owre <owre@xxxxxxxxxxx>*Date*: Fri, 29 Sep 2006 00:09:17 -0700*Cc*: pvs-help@xxxxxxxxxxx*Comments*: In-reply-to CHEN Chunqing <chenchun@comp.nus.edu.sg>message dated "Fri, 29 Sep 2006 14:49:06 +0800."*In-reply-to*: <Pine.GSO.4.64.0609291357450.14538@sf3.comp.nus.edu.sg>*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*: <Pine.GSO.4.64.0609291357450.14538@sf3.comp.nus.edu.sg>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi Chunqing, You have to be more careful when quantifiers are involved; 1 and 2 are not logically opposite. The opposite of 1 is NOT (FORALL (t: {x: T| x > ALPHA(x!1) AND x < OMEGA(x!1)}): NOT tp1!1(t, x!1)) which is logically equivalent to EXISTS (t: {x: T| x > ALPHA(x!1) AND x < OMEGA(x!1)}): tp1!1(t, x!1) This would then be provable by skolemizing the FORALL, then using the new skolem constant to instantiate the EXISTS. As for the second problem, please send your spec to pvs-bugs@csl.sri.com, so I can diagnose the problem. I believe it is already fixed in current versions of PVS, but I'd like to be certain. Thanks, Sam CHEN Chunqing <chenchun@comp.nus.edu.sg> wrote: > Date: Fri, 29 Sep 2006 14:49:06 +0800 (GMT-8) > From: CHEN Chunqing <chenchun@comp.nus.edu.sg> > To: pvs-help@csl.sri.com > Subject: [PVS-Help] what to do when consequents are logically opposite > Sender: pvs-help-bounces+owre=csl.sri.com@csl.sri.com > > Hi, all, > > First of all, thanks Professor Sam Owre for his quick and effective reply > of my last question and so I can continue my adventure in PVS :) > > Right now I met a problem during a proof (PVS version is 3.1), the detail > is below: > > [1] OO?(PROJ_1(x!1)) > |--------- > {1} FORALL (t: {x: T| x > ALPHA(x!1) AND x < OMEGA(x!1)}): > NOT tp1!1(t, x!1) > [2] FORALL (t: {x: T| x > ALPHA(x!1) AND x < OMEGA(x!1)}): > tp1!1(t, x!1) > > where tp1!1 is a function returning boolean value. To me the consequences > 1 and 2 are logically opposite (I have specified a lemma below for it and > checked the validated by PVS already): > > Uni_n_Emp_temp: LEMMA > (forall (y: II): forall (x: {xx: T| x > ALPHA(y) and x < OMEGA(y)}): > NOT tp1(x, y)) OR > (forall (y: II): forall (x: {xx: T| x > ALPHA(y) and x < OMEGA(y)}): tp1(x, y)) > => true; > > Since in sequent calculus, consequences are disjunctive, right? and hence > the above proof should be correct in my opinion. Though PVS does not > behave the way :) Can anyone kindly enlighten me what to do in this > situation? > > So I tried the command (merge-fnums (1, 2)), and thought that may solve > the problem by merging two consequences together. However, this time PVS > claims the following error message: > > ------------- start of the message ------------ > Rule? (merge-fnums (1, 2)) > No change on: (skip) > Uni_n_Emp.2.1.2 : > > [1] OO?(PROJ_1(x!1)) > |--------- > {1} FORALL (t: {x: T| x > ALPHA(x!1) AND x < OMEGA(x!1)}): > NOT tp1!1(t, x!1) > [2] FORALL (t: {x: T| x > ALPHA(x!1) AND x < OMEGA(x!1)}): > tp1!1(t, x!1) > > Rule? > Ill-formed rule/strategy: 2 > No change on: (skip) > Error: Attempt to take the car of 2 which is not listp. > [condition type: simple-error] > > Restart actions (select using :continue): > 0: Return to Top Level (an "abort" restart). > 1: Abort entirely from this process. > [1] pvs(41): > ------------ end of the message --------------- > > Did anyone encounter the similar problem before, and could you please > share your experience? > > Thank you in advance. > > Cheers > Chunqing

**References**:**[PVS-Help] what to do when consequents are logically opposite***From:*CHEN Chunqing

- Prev by Date:
**Re: [PVS-Help] what to do when consequents are logically opposite** - Next by Date:
**[PVS-Help] Substitution matter** - Prev by thread:
**Re: [PVS-Help] what to do when consequents are logically opposite** - Next by thread:
**[PVS-Help] problem when proving false in forall clause** - Index(es):