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

Re: [PVS-Help] unprovable sequent proved




Wim: It checks out.  Prior to the expansion of b2n, you have
the sequent:

mq0_34.1 :  

[-1]  p!1 = q!1
[-2]  x!1`hello(q!1)(r!1) + x!1`welcome(r!1)(q!1) +
       b2n(x!1`newusers(r!1)(q!1))
       = b2n(x!1`nbh(q!1)(r!1))
{-3}  x!1`pc(q!1) = 34
{-4}  empty?(x!1`nbh(q!1))
  |-------
[1]   x!1`hello(q!1)(r!1) + x!1`welcome(r!1)(q!1) +
       b2n(x!1`newusers(r!1)(q!1))
       = b2n(FALSE)

These formulas are recorded in the decision procedures so that the
antecedent formulas are true, and the consequents are false. 
Now, in the assert that closes this branch, you assert that
 x!1`nbh(q!1)(r!1) is false, then this propagates to -2 in the above
 sequent, which contradicts formula 1.

Does this make sense?  It would be nice to generate the explanation, but
the Shostak procedures are not easily instrumented to keep this
information.  Yices does generate an unsat core, but the use of
Shostak (which nicely supports multiple contexts) is more heavily
integrated into PVS than Yices.

Best,
Shankar

W.H. Hesselink <w.h.hesselink@rug.nl> wrote:

> Dear Sam, or other help-desk-worker,
> 
> Attached is a small dump with one lemma that is valid and proved.
> The problem is that the last sequent in the lefthand branch is
> unprovable, but PVS nevertheless accepts it by (assert).
> I assume PVS has kept some knowledge in some database, but how can the
> user know this and reckon with it?
> 
> Best regards,
> Wim
> -- 
> Wim H. Hesselink
> 
> Dept. of Computing Science       /   Bernoulliborg, office 374
>    University of Groningen      /    Nijenborgh 9, 9747 AG
>                P.O.Box 407     /     phone +31 50 3633933 (or *3939)
>          9700 AK Groningen    /      fax   +31 50 3633800
>            The Netherlands   /       http://www.cs.rug.nl/~wim