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

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



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