Re: Question on DL negation

On 5 Mar 2007, at 15:34, Michael Schneider wrote:

>
> [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.

Hi Michael, it does not necessarily break it, but it might make it  
very much harder because it is "un-local", and locality is a property  
that all known reasoning & optimisation techniques make use of. If  
you want to know more, have a look at "Mary likes all cats" (ie,  
whomever Mary does not like is not a cat, i.e., this is an  
allValuesFrom on a role complement) at

C. Lutz and U. Sattler. Mary likes all Cats. In F. Baader and U.  
Sattler, editors, Proceedings of the 2000 International Workshop in  
Description Logics (DL2000), number 33 in CEUR-WS, pages 213-226,  
Aachen, Germany, August 2000. RWTH Aachen. Proceedings online  
available from http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/ 
CEUR-WS/Vol-33/.
Bibtex entry Abstract Paper

Cheers, Uli

>
> 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.
>
>