Re: Question on DL negation

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.

> 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 12:52:15 UTC