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

Hello,

Bug 1 becomes apparent only if you consider entailment of key axioms -- that is, if you have an OWL 2 DL ontology O and you want to check whether O entails a particular key axiom. Had we correctly defined the semantics of keys, this should be easy; however, Markus Krötzsch has noticed that this is not the case. Actually, the EL, QL, and RL implementations cannot implement the specification as it is (as implementing the published semantics would destroy the good computational properties of these logics). Theoretically speaking, DL implementations could implement the spec as is without an increase in computational complexity, but this would require quite complex techniques.

For all other types of axioms, their entailment can be checked without any problems even with the existing semantics.

Although bug 1 might seem complex, it is actually the simplest one to deal with, in the sense that nobody will have implemented the spec in the sense it was written in. I made a silly error when formalizing the intuitive semantics behind easy keys, and nobody noticed this error. I'm 100% certain that all developers actually had my intuitive interpretation in mind, so fixing this bug would actually bring the specification in line with the implementations. Therefore, despite the apparent technicality of the problem, I believe this change to be quite innocuous from a practical point of view.

Regards,

Boris

On 29 Mar 2010, at 19:02, Alan Ruttenberg wrote:

> 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:18:38 UTC