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

[PVS-Help] (no subject)

Dear Authors of PVS Tutorial @WIFT'95 and PVS-Help volunteers,

I am writing this mail to the authors of "A tutorial introduction to PVS"

I just began to learn PVS. While reading (and practising the phone-book
example) the above tutorial (which I downloaded from the URL
http://www.liacs.nl/~devink/fm2003/wift-tutorial.ps), I happened to see a
slightly different output from PVS (my version of PVS is 5.0).

I have a doubt. Its regarding the proof about "KnownAdd" conjecture. As
discussed in lines 9 and 10 on page 12 (excluding the boxes) of the
tutorial, with type for AddPhone function being [B,N,P -> B]  we cannot
prove the conjecture. However, even after changing the type to [B,N,GP ->
B], as suggested on lines -12 to -9, I am left with the same interaction
from PVS i.e same as when the type was [B,N,P -> B].

But when I changed "pn: P" to "pn: GP" in the FORALL quantifier, the proof
proceeds in a flash.

My questions:
1. Why the type checker did not raise an error when I passed "pn: P" to
AddPhone whose type signature is [B,N,GP -> B] ?

2. Assuming that GP is a restricted sub-type of P, with type of AddPhone
being [B,N,GP -> B] the proof should have proceeded without changing the
type in FORALL quantifier.

I agree that my mail might look too silly and wordy, but I request you to
give some constructive reply. As of now, I have not got LATEX on my
machine, so I may not give you the LATEX output proof.

Thanks in advance,
Dr. Gourinath Banda
PhD, MSEngg, BTech
Scientist Fellow,
Formal Verification,
Room No. 317,
National Aerospace Laboratories,

Direct Phone: +91 - 080 - 2508 6507