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

Question about theory




Is there a good answer to the question of which "version" of the reals
that the PVS type 'real' uses? I'm writing a paper whose intended
audience will include computer algebra specialists who know almost
nothing about theorem proving, and it would be useful to be able
to say something like:

PVS categorises the reals equivalently to Dedkind cuts, or to Cauchy 
sequences...

The documentation makes no mention of such questions that I can find,
and reading the prelude section on the reals it would appear that
the reals might be underspecified in this regard. Knowing even this
for certain would be useful.


-- 
*E-mail*aaa@dcs.st-and.ac.uk*******  Dr Andrew A Adams
**snail*30 Woodburn Terrace********  School of Comp Sci
***mail*St Andrews KY16 8BA, UK****  University of St Andrews
****Tel*+44-1334-470013/463268*****  St Andrews KY16 9SS