[Om] OpenMath on the Semantic Web?

[Christoph Lange]

On Tue, Feb 3, 2009 at 3:58 PM, Paul Libbrecht <paul at activemath.org> wrote:
> - I believe we have an instance-of type of relationship, namely the
> relationship between OMS and symbol-declaration

Sure we do, but it's far from obvious to people who are used to the
semantic web. And it's not exactly the same. In RDF, both instance and
class have URIs. In our case, the symbol declaration has a URI, but
the OMS doesn't. The "instantiation" is rather an implicit one: it's
not the single OMS that counts as a proper instance, but its
interrelation with other OMSes in the same OMOBJ.

> - do we have any construct or FMP to say that a symbol-declaration is a
> generalization of another symbol-declaration? (i.e. that, in order to
> restrict the world, one could just consider the more general case) ?

Nothing standardized, just constructed things like "forall x . x is
sym1 => x is sym2" -- whose semantics depends on the underlying logic
and what our symbols are (e.g. sets).

> I am not 100% sure that DEFMP satisfies this.

I think DefMP is something different -- and much more general than
"symbol1 isGeneralizationOf symbol2", as it allows for defining one
symbol by _any_ combination of other symbols. It compares best to an
OWL axiom for a class, where one class is defined in terms of other
classes.

> - properties? would be attributions?

It depends. Attributions are something like metadata-like annotations,
so maybe they are similar to OWL AnnotationProperties. But sometimes
attributions are more formal, e.g. when used for types.

Otherwise, properties in RDF/OWL allow for modeling relationships in
any way, and in mathematics, there are lots of ways of doing so, e.g.
sets, proper relations, functions, propositions, …

> And clearly, OWL or RDF is missing a notion of applications, variables,
> bound-variables.

It would be possible to construct a lot of that in a very clumsy way,
basically transforming the whole XML tree structure of an OMOBJ
literally into an RDF graph. (Compare Massimo Marchiori's MKM 2003
paper.) For my work, I chose not to do so, as I don't see much value
in such a representation. Automated theorem provers, CASes, and other
term rewriting systems are IMHO best for working with OMOBJs, whereas
RDF is useful for representing incomplete outlines of the higher
levels of mathematical knowledge (e.g. what
examples/notations/properties exist for some symbol, and in which CD
they are given; see
http://kwarc.info/projects/swim/pubs/semwiki08-notation-semantics.pdf
)

Cheers,

Christoph

-- 
Christoph Lange, http://de.wikipedia.org/wiki/Benutzer:Langec, ICQ# 51191833