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

Re: [PVS-Help] "1 = 0" pvs problem



Hi Lingzhao,

Although the consequent is false, the sequent is true because one of the
antecedents is false.  Just remember to read the sequent as "the
conjunction of the antecedents implies the disjunction of consequents",
and the basic rules of implies (i.e., false implies anything).

Regards,
Sam

lingzhao <maolzh@xxxxxxxxx> wrote:

> Hi,
> 
> 
> I am using pvs, but sometimes I encountered some problems. 
> 
> When I was trying to prove a lemma in pvs, I found one proof sequence as
> below:
> 
> 
>         [-1]  (x!1 = 0)
>         [-2]  (s0!1(1) = 2)
>         [-3]  s0!1(0) = 1
>         [-4]  m!1 = 0
>         {-5}  (0 = 2)
>         [-6]  (s1!1 = s0!1 WITH [(0) := 3])
>           |-------
>         [1]   1 = 0
>         
>         Rule? (assert)
>         Simplifying, rewriting, and recording with decision procedures,
>         
>         This completes the proof of update_privilege.1.1.
> 
> 
> ´╗┐After I typed a "assert" rule in pvs, it proves!
> 
> The problem is that the consequent formula " ´╗┐[1]   1 = 0 " is
> absolutely not right, but why pvs assert that it can be proved by the
> antecedent formulas?
> 
> Thanks,
> Lingzhao