Re: Question on DL negation

Bijan Parsia wrote:
> 
> On 5 Mar 2007, at 17:21, Vaughan Pratt wrote:
> 
>> Bijan Parsia wrote:
>>> You can see by playing around with combinations of the role 
>>> constructors the effects on complexity.
>>> Remember that all this is just (a fragment of) FOL (well, except if 
>>> you add transitive closure per se), so all the constructors are just 
>>> normal propositional (for the most part) connectives on binary 
>>> predicates.
>>> Expressive role constructors are associated with propositional 
>>> dynamic logic (and converse propositional dynamic logic).
>>> It's also instructive to see how arbitrary concept negation is 
>>> difficult. You can see in the tractable fragments document that most 
>>> of them allow concept (i.e., restricted) disjointness:
>>>     <http://www.cs.man.ac.uk/~ezolin/logic/complexity.html>
>>
>> The difficulty with negation arises when passing from predicates to 
>> classes.
> 
> I don't see that at all. I'm not sure what you mean by "predicates" and 
> "classes" here. In DLs, classes generally refer to one place predicates 
> (consider the obvious model theoretic intepretation).

That's quite reasonable provided you're talking about some other 
framework than OWL, e.g. the sets and classes of Goedel-Bernays set 
theory.  To quote from section 3, Classes, in the OWL reference manual 
at http://www.w3.org/TR/owl-ref/,

> every OWL class is associated with a set of individuals, called the class extension

Not every predicate has a class extension in that sense, for example the 
predicate true(x).   There is no "set of everything."  In contrast its 
negation the predicate false(x) does have an extension, namely the empty 
set.

> 
>> The negation of a predicate simply complements its truth value.
> 
> Er... \forall(x)(C(x) \leftarrow \neg D(x)).
> 
> The predicate doesn't have a truth value.

Ok, I start to see why you're having difficulty understanding me.  If 
you insist that a predicate such as D(x) does not have a truth value at 
each x then it's easy to see we're going to be talking at cross 
purposes.  My reading of your example is that whenever C holds of x, D 
does not, verified formally by taking the truth value of D at x, 
negating it, and verifying that the resulting truth value is *true*. 
Your reading may well be different, but in that case I'd be very 
interested in seeing it.

The fact that the truth value of D(x) depends on x doesn't mean that it 
doesn't have a truth value, it just means that it has a dependent truth 
value.

>>   Lifting logical connectives to the status of operations on sets and 
>> classes is a delicate business.
> 
> I don't know why you put it this way. That is, I don't see any 
> additional insight and some confusion. General negation is powerful and 
> thus difficult. Having it allows for some nice interdefinability.

If this is already adequately reflected in OWL's semantics of negation 
then you're quite right that I'm wasting bandwidth inappropriately by 
stepping in here.  However if it's not then it seems to me that it is a 
potential future stumbling block for both implementers and users.

> 
>> In the standard (Fischer-Ladner) semantics of propositional dynamic 
>> logic, propositional negation of P is interpreted as the complement of 
>> the set of worlds in which P holds *relative to* a specified *set* W 
>> of all possible worlds constituting the underlying set of the Kripke 
>> structure.  If your semantics has that form then you are on safe 
>> ground with negation.  If however it just has the intuitive meaning of 
>> "everything else" then you leave yourself wide open to the problems of 
>> impredicativity such as Russell's Paradox.
> 
> Uh, I'm very skeptical about this last bit, though I'm no PDL person.
> 
>     <http://www.springerlink.com/content/cf40guhq1m5t6lpu/>
>     <http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B6WJ0-4B55K9J-G-5&_cdi=6864&_user=494590&_orig=browse&_coverDate=04%2F30%2F1979&_sk=999819997&view=c&wchp=dGLbVlb-zSkzS&md5=e6986bd20377ddee8f055be2886a8368&ie=/sdarticle.pdf> 
> 
>     <http://www.csc.liv.ac.uk/~dirk/paper/mthesis-dirkwalther.pdf>
> 
> PDL with arbitrary negation of programs (i.e., arbitrary negation of 
> role expressions) is undecidable, but that's hardly the same thing as 
> allowing for paradoxes.  I'd be interested in your construction of the
> Russell's paradox in PDL^-.

Since my point was that you don't run afoul of Russell's paradox in PDL 
with Kripke semantics, and you were the one who brought in PDL^-, it 
would seem to me that whether or not it can be done in PDL^- is for you 
to answer.

That said, I'd be very interested to know whether anyone besides you on 
this list proposes to apply to programs the same logical connectives as 
are applied to propositions, especially the nonmonotonic ones such as 
negation and implication.  For anyone who has been thinking along these 
lines, the paper http://boole.stanford.edu/abstracts.html/#ActLog 
proposes one approach to this that is very different from taking 
literally the definition of a program as a set of behaviors and applying 
the usual set-theoretic operations as done in the Walther thesis you 
cited above.  With the exception of union, the set operations applied to 
programs tend to be pretty incoherent, being heavily dependent on the 
choice of notion of "behavior".  Union is an exception because for all 
notions of behavior it simply aggregates the behaviors, making the 
program A union B the nondeterministic choice of A or B.

Atomic negation, on the other hand, seems
> ok. But restriction to atomic negation and restriction to disjointness 
> are not quite the same thing.
> 
> Ok, this is a distraction now :)

If negation in OWL is well in hand then I agree, and again I'm sorry if 
I seemed to be butting in inappropriately.  If not then I'm grateful for 
this opportunity to stir things up a little.

Vaughan Pratt

Received on Tuesday, 6 March 2007 07:09:34 UTC