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

Re: [PVS-Help] what to do when consequents are logically opposite



Hi, CHEN Chunqing

 I think using lemma command (lemma "forall_or[{x: T| x > ALPHA(x!1) AND x < OMEGA(x!1)}]") defined in the prelude file should be help.
you can try.	

        qgxu@mail.shu.edu.cn
          2006-09-29

======= 2006-09-29 14:52:19 您在来信中写道:=======

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

= = = = = = = = = = = = = = = = = = = =