Re: Are the acyclicity "nonstructural restrictions" too strict?

After considering your earlier query we had already realised that  
this part of the document was slightly broken. As a fix seemed to be  
both highly necessary (in order, e.g., to be fully backwards  
compatible with OWL) and of a of an editorial nature, Boris has  
already added an issue to the issue list and fixed the problem. I  
hope that no one objects to this. The section is still not as good/ 
clear as it should be, and will no doubt receive further attention as  
part of the OWL WG process, but at least it is now technically  
coherent (I think).

Thanks again for your help in debugging this document -- please do  
keep up the good work :-)

Ian

p.s. see http://en.wikipedia.org/wiki/Partial_ordering#Strict_and_non- 
strict_partial_orders for a definition of strict partial order

On 16 Oct 2007, at 08:39, Michael Schneider wrote:

>
> 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 18:04:03 UTC