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

Hi Boris,

both seem sensible to me, +1. Cheers, Uli

On 29 Mar 2010, at 11:17, Boris Motik 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:04:39 UTC