LANG: issue 5.1 - Uniform treatment of literal/data values

I promised to say something about the possible use of key constraints
in this context, so here it is.

Carsten Lutz, Ulrike Sattler, Carlos Areces and myself have been
looking into the idea of reasoning w.r.t. a set of "key" axioms. These
are axioms of the form "C hasKey k1,...,kn", where C is a class and k1
to kn are a list of functional datatype properties (in general these
could be functional paths, but this usually leads to undecidability).

In its simplest form the class C would be Thing, and there would only
be a single functional datatype property in each axiom, e.g., "Thing
hasKey k". Adding this axiom would be equivalent to making the
datatype property k inverse functional. Referring to Dan's state code
example, adding the axiom "Thing hasKey stateCode" would support the
desired entailment.

The problem of reasoning w.r.t. such axioms is similar to (but worse
than) the problem of reasoning with nominals (i.e., classes defined
extensionally using the oneOf constructor) - in fact it is easy to see
that the expressive power of keys subsumes that of nominals because if
keyProp is an key for Thing and ranges over the integers, then
restriction classes of the form "onProperty keyProp toValue i", where
i is an integer, can be used as nominals. It is, however, still
possible to separate reasoning w.r.t. datatypes from reasoning
w.r.t. the object domain (using a more sophisticated datatype
reasoner) s.t. a hybrid reasoner is sound and complete iff both the
object and datatype reasoners are sound and complete.

Obviously this work is still at a relatively early stage, so I don't
want to suggest that it represents any kind of "compromise solution"
to the problem (even if such a compromise were acceptable).

Regards, Ian

[1] http://lists.w3.org/Archives/Public/www-webont-wg/2002Apr/0261.html

Received on Wednesday, 18 September 2002 10:29:04 UTC