[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] PVS-doubt about PVS-tutorial@WIFT'95
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.
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
Room No. 317,
National Aerospace Laboratories,
Direct Fixed Phone: +91 - 080 - 2508 6507
Mobile: +91 99 89 40 50 78