- From: Paul Libbrecht <paul@activemath.org>
- Date: Thu, 3 Feb 2005 13:51:16 +0100
- To: JB Collins <joebmath@yahoo.com>
- Cc: RobertM@dessci.com, www-math@w3.org

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