Are the acyclicity "nonstructural restrictions" too strict?

Hello!

It looks to me as if the "acyclicity" restriction on object properties in
the "nonstructural restrictions" chapter 7 of the OWL-1.1 draft 

  <http://www.webont.org/owl/1.1/owl_specification.html#7>

does not permit the definition of equivalent properties.

The acyclicity restriction is given by:

  A strict partial order < on the object property expressions
  [a "property expression" PE is either an object property or its inverse] 
  must exist such that each SubObjectPropertyOf(SUB PE) axiom in 
  [the axiom closure] Ax fulfils the following conditions:

    1) SUB is of the form SubObjectPropertyChain(PE PE), or
    2) SUB is of the form InverseObjectProperty(PE), or
    3) SUB is of the form SubObjectPropertyChain(PE1 ... PEn) 
       and PEi < PE for each 1 ? i ? n, or
    4) SUB is of the form SubObjectPropertyChain(PE PE1 ... PEn) 
       and PEi < PE for each 1 ? i ? n, or
    5) SUB is of the form SubObjectPropertyChain(PE1 ... PEn PE) 
       and PEi < PE for each 1 ? i ? n. 

First, to be clear on the nomenclature: Does "/strict/ partial order <" mean
that "<" has to be /irreflexive/? I will assume this in the rest of this
mail.

Now, let's regard an ontology which contains the following two axioms:

    (A1) SubObjectPropertyOf(p1 p2)
    (A2) SubObjectPropertyOf(p2 p1)

Note that these two axioms may either be explicitly stated in the ontology,
or may be entailed by other axioms, e.g. by an
'EquivalentObjectProperties(p1 p2)' axiom. For our discussion here this does
not make a difference, because the nonstructural restrictions deal with any
axioms occuring in the "axiom closure Ax" of an ontology.

The acyclicity condition demands that (A1), with SUB := 'p1' and PE := 'p2',
has to fulfil one of the five conditions mentioned above. If taken
literally, /none/ of these conditions really match, but by substituting
'SUB' by the expression 

    SUB' := "SubObjectPropertyChain(p1)"

I obtain the following axiom (A1'):

    (A1') SubObjectPropertyOf(
              SubObjectPropertyChain(p1)
              p2)

(A1') happens to be semantically equivalent to (A1), and (A1') now really
matches condition 3) above.

[
FIXME: Straight from the text, it does not seem to me that I am really
allowed to perform such a "semantics-save" substitution. All five conditions
start by

    "SUB is of the form ..."

and not by

    "SUB can be translated into the form ..."

Is this something which has to be fixed/clarified in the text, or did I do
non-allowed things?
]

AFAICS, /only/ the 3rd of the above condition seems to match without
changing the semantics of the ontology. For instance, in order to match
condition 2), p1 would have to be the inverse of p2, and this would
introduce a new assumption, which has not been stated elsewhere in the
ontology. For conditions 1), 4) and 5) I do not even see how a
transformation into an equivalent axiom can be applied.

Ok, so the 3rd condition can be (uniquely) matched by (A1), and from this
condition we obtain that that "p1 < p2" must hold. The analog argumentation
for (A2) leads to

    (A2') SubObjectPropertyOf(
              SubObjectPropertyChain(p2)
              p1)

which again uniquely matches condition 3, so we obtain that "p2 < p1" must
hold. Taken together, we have both "p1 < p2" and "p2 < p1". But because "<"
has to be "strict", i.e. irreflexive, this is not allowed, even if we know
that p1 and p2 are equivalent properties.

How do I have to interprete this result? Does this mean that now that we
have sub property chains in the language, it becomes possible that even
simple equivalence cycles between properties can lead to undecidability? Or
should the "strictness" condition on partial orders "<" be relaxed somehow?


Cheers,
Michael

--
Dipl.-Inform. Michael Schneider
FZI Forschungszentrum Informatik Karlsruhe
Abtl. Information Process Engineering (IPE)
Tel  : +49-721-9654-726
Fax  : +49-721-9654-727
Email: Michael.Schneider@fzi.de
Web  : http://www.fzi.de/ipe/eng/mitarbeiter.php?id=555

FZI Forschungszentrum Informatik an der Universität Karlsruhe
Haid-und-Neu-Str. 10-14, D-76131 Karlsruhe
Tel.: +49-721-9654-0, Fax: +49-721-9654-959
Stiftung des bürgerlichen Rechts
Az: 14-0563.1 Regierungspräsidium Karlsruhe
Vorstand: Rüdiger Dillmann, Michael Flor, Jivka Ovtcharova, Rudi Studer
Vorsitzender des Kuratoriums: Ministerialdirigent Günther Leßnerkraus

Received on Tuesday, 16 October 2007 07:39:43 UTC