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

Re: [PVS-Help] quotient constructions in PVS

Lawrence Paulson writes:
   From: Lawrence Paulson <lp15@cam.ac.uk>
   Date: Thu, 19 Aug 2004 14:51:28 +0100
   Subject: [PVS-Help] quotient constructions in PVS
   Does PVS provide any support for quotienting type 
   or set with respect to an equivalence relation?

The prelude (view with M-x view-prelude-file) defines equivalence
classes, kernels, and quotions and proves a view standard
results. Bart Jacobs (bart@cs.kun.nl) developed this material.
However, I am not aware of any paper about it.

   Can anyone refer me to a paper describing a quotient construction 
   performed using PVS? 

A quotient construction in higher-order logic is probably too
simple to deserve its own paper. Are there papers describing
_just_ quotients in Isabelle/Hol?

I use quotions in my CMCS 04 paper "Predicate and Relation
Lifting for Parametric Algebraic Specifications". The motivating
example is formalized in PVS, see Prop. 3.5. I can put the PVS
sources online if you are interested.