[om] OpenMath and PVS

[Richard Fateman]

Rather than use OM as an interface to PVS, I was thinking that
you might make use of PVS's definitions in some way, e.g. to
define (say) "natural number"   . It seems like you are
treating it as something to be documented, which I suppose
is something.
No, I don't think I need anything sent to me; I don't actually
need to use PVS (or OM) at the moment.
Regards
RJF


Michael Kohlhase wrote:

> 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


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