Re: Semantic information for math representations of physics

Le 3 févr. 05, à 13:20, JB Collins a écrit :

> [...] Those things being said, I am going to take your
> response as guidance that says something like "when
> concepts are defined in MathML, use them; when they
> are not, for user extensibility, rely on OpenMath."

What we know:
- OpenMath and MathML are informally compatible (that is, everyone 
believes so)
- the policy in the two bodies (W3C Math Working/Interest Groups and 
the OpenMath society) converge (which was not the case at the time 
MathML content was created, I think).

MathML-content has been started with a view that an element-name is the 
best representation for a mathematical symbol... thus it needs to 
declare all these element-names, for example, in the DTD, hence specify 
them all part of the language specification. Extensibility is not 
normalized

OpenMath has started with extensibility in mind from the start on. 
There is no element in the OpenMath language  that denotes a precise 
mathematical "notion", "symbol", "concept". All of them are described 
in content-dictionaries the management of which is somewhat easier.
Content-dictionaries can be contributed and modified easier than a 
language specification.

There has been some discussions, probably not enough, about bringing 
MathML and OpenMath in sync but this has not been finalized.

There are intents to promote a tighter compatibility declaration such 
as cross-pointing between OpenMath symbols and MathML symbols and 
indicating best practice for the usage of OpenMath along with MathML.

Comments and suggestions about this would be most welcome!

Both OpenMath and MathML, however, do not treat the problematic of 
grounding the extension of a symbol, for example, using a definition. 
That definition could be formal or informal, it would, typically, need 
further developments such as theorems, proofs, or axioms.
This last step, an attempt at complete representation of mathematical 
documents is the goal of the OMDoc language, 
http://www.mathweb.org/omdoc/.
OMDoc's user-base or gang of tools is not as rich...

Physics has not been touched much in OMDoc, as far as I know. I would 
view such statements as the formal statement about the nature of an 
observable as being a possible extension of OMDoc.
(which could even be something like the statement of the type of a 
symbol).

OMDoc theories are not, yet, convertible back into an OpenMath content 
dictionary.
This is a known issue which we intend to tackle in the ActiveMath 
authoring gang of tools (headed by jEditOQMath, 
http://www.activemath.org/projects/jEditOQMath).

OMDoc documents are the base of our ActiveMath learning environment. 
The formal part of OMDocs are not much used yet though there are some 
intents in the direction of proof-planning usage for education...

The content in the Mizar Mathematical Library is one of the most famous 
formal mathematics libraries and, clearly, conversion from there to 
OMDoc is something that interests many involved in OMdoc and a start of 
it has been attempted by Michael Kohlhase (on this list usually) among 
others.
I heard of no results thus far.

I did not know of the goal of Mizar encoding to provide a platform for 
the exchange of mathematical documents between theorem provers... the 
conversion of the logical foundation is, as far as I know, often a very 
tough problem when considering such exchange and the logical foundation 
of Mizar documents is very high level, I heard.

paul

> As an additional question to throw in, I am also
> interested in knowing if MathML / OpenMath borrow or
> cooperate with the MIZAR project. While I started this
> thread on the MathML reflector, you pointed to
> OpenMath and its use for interchanging documents for
> theorem provers. The MIZAR project provides a similar
> capability. While they seem primarily focused on
> supporting mathematicians, there seems to be a lot to
> borrow from.

Received on Thursday, 3 February 2005 12:51:55 UTC