[om] OpenMath and PVS

[Michael Kohlhase]

Dear Richard,

I copmpletely agree with the sentiment to use something as formal as the 
PVS prelude as content dictionaries in OpenMath. This is clearly 
necessary in many applications of OpenMath. In fact this was one of the 
motivations for me to develop the OMDoc format, which allows to cover 
such documents.

Incidentally, in the draft of the OM2 standard, we have weakened the 
requirements for content dictionaries from a prescription of a format 
(the OM cd encoding) to a set of minimal requirements that a content 
dictionary must fulfill. As far as I can see this includes the PVS 
prelude. An XML encoding of the prelude (for instance the OMDoc version) 
clearly fulfils the requirements.

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