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

Re: [PVS-Help] starting to work in PVS



On 5/5/08 3:50 AM, "popescu2@xxxxxxxx" <popescu2@xxxxxxxx> wrote:

> 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.

Although it's not an actual Isar-style proof capability, you might want to
look at Cesar Munoz's ProofLite package for PVS:

   http://research.nianet.org/~munoz/ProofLite/

It provides declarative proofs, albeit at a lower level of abstraction than
what Isar supports.


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

I don't know, but would consider these unlikely.


> (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 have been working on a search tool called Hypatheon.  Originally it was to
be a web-based tool, then the project lost funding and was dormant for a
while.  I have recently revived it in a less ambitious form.  The tool will
run as a separate application connected to PVS, providing a database search
feature to support interactive proving.  It's not ready yet, but should be
available in about two months.


> 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?

Yes, the prelude has several types of subrange induction schemes, and
datatypes have their own induction schemes that are found in separate
theories generated when the datatypes are introduced.


> Thanks in advance for any advice on these,
>    Andrei Popescu
> 


Regards,

Ben Di Vito
1 South Wright Street, MS 130
NASA Langley Research Center
Hampton, VA 23681   USA

voice: +1-757-864-4883     fax: +1-757-864-4234
b.divito@xxxxxxxx
http://shemesh.larc.nasa.gov/people/bld