Re: Two bugs in the OWL 2 Direct Semantics and the SS&FSS documents

Hi Boris,

+1 on Bug 2.
Bug 1 and fix is more complicated and I'd like to see some more discussion.

-Alan

On Mon, Mar 29, 2010 at 11:20 AM, Boris Motik
<boris.motik@comlab.ox.ac.uk> wrote:
> Hello,
>
> Two bugs in the OWL 2 spec have recently come to light (see details below). To the best of my knowledge, all existing implementations either don't implement the relevant features, or conform to the *intended* spec and not to the spec as currently written (I have confirmed this with the implementers of Racer, Pellet,  FaCT++ and HermiT). It is highly unlikely that anyone would implement the buggy spec as it would make implementation difficult or impossible. I therefore hope that we can fix these problems prior to re-publication when XSD goes to Rec.
>
>
> 1. A bug in the OWL 2 Direct Semantics
>
> Section 2.3 of the Direct Semantics document defines the ISNAMED function, which is used in the definition of the semantics of easy keys. Unfortunately, this function has been defined to be true for an element of the domain *if and only if* it interprets a named individual, whereas it should be true *if* an element interprets a named individual (leaving open whether ISNAMED is true for other elements). This makes easy keys not so easy: as a side-effect of this definition, ISNAMED acts as a nominal, which has consequences for the computational properties of the profiles. In particular, ontology entailment (which is the basic computational problem for OWL 2) becomes NP-hard with keys in OWL 2 EL.
>
> We can fix the error by the following two steps:
> - We need to make ISNAMED a part of an interpretation. Thus, an interpretation needs to become a tuple of the form I = ( ΔI , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ LT , ⋅ FA , ISNAMED).
> - We need to weaken the definition of ISNAMED from iff to if. That is, for each named individual a, ISNAMED(a^I) must be true (but not the other way around).
>
>
>
> 2. A bug in Section 11.2 of the Syntax document
>
> The global restrictions in Section 11.2 of Structural Specification and Functional-Style Syntax are designed to ensure that (amongst other things) in OWL 2 DL "property assertions connect anonymous individuals in a tree-like way"; this is needed in order to ensure decidability. Unfortunately, we forgot to disallow anonymous individuals from occurring in ObjectHasValue and ObjectOneOf class expressions, which means that anonymous individuals *can* be connected in a non-tree-like way, and hence fails to ensure decidability.
>
> This problem can be fixed simply by adding the relevant restriction in Section 11.2 of Structural Specification and Functional-Style Syntax.
>
>
> Please let me know how you feel about this.
>
> Regards,
>
> Boris
>

Received on Monday, 29 March 2010 18:03:26 UTC