[om] OpenMath and PVS

[Michael Kohlhase]

Richard,

I have worked on an OMDoc (see http://www.mathweb.org/omdoc) interface 
for PVS, which outputs the formulae in OpenMath. If you are interested, 
I can send you an OMDoc version of the prelude.

Unfortunately, we never got around to exporting proofs from PVS, and the 
code has been dormant for a while now.

Michael


-------------------------------------------------------------------------
    Prof. Dr. Michael Kohlhase,         Office: Research 1, Room 62
    Professor for Computer Science      Campus Ring 12,
    School of Engineering & Sciences    D-28758 Bremen, Germany
    International University Bremen     tel/fax: +49 421 200 3140/3103
    http://www.cs.cmu.edu/~kohlhase     e-mail: 
<m.kohlhase at iu-bremen.de>
--------------------------------------------------------------------------


Richard Fateman wrote:
> Have any of the OM activities interacted with PVS,
> in particular
> see
> http://pvs.csl.sri.com/doc/prelude.html
> 
> or for background, see the
> PVS home page
> http://pvs.csl.sri.com/
> 
> if not, its level of formalization might be worth examining and
> perhaps even adopting.
> 
> RJF
> 
> -- 
> om at openmath.org  -  general discussion on OpenMath
> Post public announcements to om-announce at openmath.org
> Automatic list maintenance software at majordomo at openmath.org
> Mail om-owner at openmath.org for assistance with any problems
--
om at openmath.org  -  general discussion on OpenMath
Post public announcements to om-announce at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-owner at openmath.org for assistance with any problems