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

[PVS-Help] starting to work in PVS



Hello, 

I have just taken up PVS after first traveling through  Isabelle and Coq.  I prefer PVS for what I am trying to do (modeling generic labelled transition systems and bisimilarity, and thus dealing with "very" strongly typed items) since it provides true predicate subtyping and allows me to define functions involving type-dependencies that cannot be expressed directly in Isabelle, and not even in Coq.  However, I am missing some features from the mentioned provers, and I wonder if they can be provided or compensated by some PVS features or techniques: 

(1) Most importantly: Support for structured, declarative proofs in the style of Isabelle-Isar. 

(2) Extendible first-order quasi-decision procedures.  

(3) Search for theorems with a given pattern available in a given context.  

(I am sure feature (3) is available somehow, but I was not able to find it yet.)  

I also have a small technical question: can one induct on a subtype of nat or a datatype somehow directly, without having to rephrase the theorem?

Thanks in advance for any advice on these, 
   Andrei Popescu