Re: Question on DL negation

[CC'd to public-owl-dev]

Hi Bijan!

Bijan Parsia wrote on 5 Mar 2007:

> On 5 Mar 2007, at 10:45, Matt Williams wrote:
> 
>>
>> Dear All,
>>
>> As I understand, most DL's do not allow for the negation of roles.
>>
>> However, given a formula of the form R(x,y) (where R is some role),  
>> since this is equivalent to (R(x,y) & \top(y))
> 
> That's not a class expression. The standard negation constructor,  
> e.g., in OWL, applies only to class expresession (i.e., to formulae  
> with at most one free variable).
> 
>> which could be negated as ¬( R(x,y) & \top(y)),
> 
> Only if you had negation of arbitrary formulae, which you generally  
> don't. And if you did, you could just say ~R(x, y) :)
> 
>> is it possible to effectively relax this constraint in some cases  
>> without affecting the logic?
> 
> So, there are at least two forms of role negation you might consider:  
> negation of *ground* roles and negation of *arbitrary* roles. The  
> former allows you to so say that, e.g., bob does *not* love mary,  
> where as the latter allows you to say that love and hate are disjoint.
> 
> In OWL, given nominals, you can encode the former, e.g., bob:  
> complementOf(hasValue.love({mary}). In this way, it's clear that  
> nominals are more expressive than aboxes alone. In OWL 1.1, you can  
> express the former directly and you can express the latter at least  
> in the form of disjointness of properties.

Very interesting! Perhaps, a little more is needed to model a real role 
negation based on owl11:disjointProperty:

First, as you suggested above:

   (1) DisjointProperties( hates loves )

Then, I would want to make 'hates' and 'loves' subproperties of some 
combined 'hatesORloves' property:

   (2) ObjectProperty( hatesORloves )
       SubPropertyOf( hates hatesORloves )
       SubPropertyOf( loves hatesORloves )

This is possible even in OWL1.0. What's missing now is a means to 
"close" this definition, somewhat like:

   (3) SubPropertyOf( hatesORloves unionPropertyOf(hates loves) )

or as an alternative to (1) through (3):

   DisjointPropertyUnion( hatesORloves hates loves )

So, what's missing (at least from the perspective of role negation) in 
the current OWL11 draft are logical constructors for properties: 
'unionPropertyOf', 'intersectionPropertyOf' and 'complementPropertyOf' - 
and perhaps syntactic sugar like 'DisjointPropertyUnion'.

But I'm most probably not the first one who stumbles over this, so there 
might be at least two reasons, why there are no such constructors:

   1) Very few interest or usecases on them, and/or

   2) perhaps they would even break decidability of OWL/DL.

So, do you (or some other people working on OWL1.1) know why there 
aren't such constructors in the draft?


Cheers,
Michael

>> I'm interested in rules that have a single role as the head, and  
>> negation of such heads would be useful...
> 
> Hope this helps.
> 
> Cheers,
> Bijan.

Received on Monday, 5 March 2007 15:35:04 UTC