[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 <firstname.lastname@example.org>
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 (email@example.com) 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.