From: Vaughan Pratt <pratt@cs.stanford.edu>

Date: Mon, 05 Mar 2007 23:09:12 -0800

Message-ID: <45ED1398.7030902@cs.stanford.edu>

To: public-owl-dev@w3.org

CC: semantic-web@w3.org

Date: Mon, 05 Mar 2007 23:09:12 -0800

Message-ID: <45ED1398.7030902@cs.stanford.edu>

To: public-owl-dev@w3.org

CC: semantic-web@w3.org

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 PrattReceived on Tuesday, 6 March 2007 07:09:41 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 20:58:14 UTC
*