On Tue, Feb 3, 2009 at 3:58 PM, Paul Libbrecht <[email protected]> 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 _______________________________________________ Om mailing list [email protected] http://openmath.org/mailman/listinfo/om
