Re: Question on DL negation

On Mar 8, 2007, at 5:47 AM, Vaughan Pratt wrote:

> Bijan Parsia wrote:
>>> 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.
>> [snip]
>> I don't know where you are getting that from. I'm not talking  
>> about any *nonmonotonic* negation or implication. And I'm not  
>> proposing it, I'm pointing out that that's how PDL works.
>
> According to http://en.wikipedia.org/wiki/Dynamic_logic_% 
> 28modal_logic%29 the negation connective of PDL applies only to  
> propositions, not programs.

Since, in the context, I made an *analogy* between negation of  
*roles* (along with other role contructors such as union,  
intersection, etc. i.e., the normal truth functional connectives  
applied to binary predicates) and the negation of "transitions" (aka  
programs) in the PDL *family* of logics (i.e., it's an extension to  
basic PDL). As in:
		<http://citeseer.ist.psu.edu/degiacomo95pdlbased.html>

Or in PDL^-, as I pointed to before. (I find the above paper a bit  
confusing. Sigh. I don't have time to delve, at the moment, into the  
precise difference between PDL^- and DIFR.)

The correspondence between ALC_{reg} and Converse PDL (i.e., without  
role negation) is nicely presented in:
	 	<http://citeseer.ist.psu.edu/calvanese98reasoning.html>

Since you are a major PDL guy (cited in the above papers!), I'm a tad  
confused and uncomfortable with this discussion. We *have* to be  
having terminological problems, or I am completed confused. Neither  
is a happy state for me.

Note that I wasn't trying to do anything funky. When someone asks  
about disjointness (or negation) of roles or concepts (i.e.,  
properties or classes), I am *not* thinking of any sort of exotica  
such that one has to, e.g., worry about paradoxes. I am thinking of  
normal truth functional  negation applied to two- and one-place  
predicates, or, more generally, to first order formulae. How you  
restrict negation can, of course, have profound affects on the  
complexity of the language. But sometimes the language lacks an  
explicit negation constructor (e.g., OWL Lite) but it is definable.  
In that case, adding an explicit one won't change the complexity  
(*clearly* you know this; I'm just trying to establish the context  
without making any assumptions).

> PDL's negation is a nonmonotonic (in fact antimonotonic) operation,  
> in the sense that if p <= q then not-q <= not-p.  Similarly  
> implication p -> q is nonmonotonic but not (purely) antimonotonic:  
> it is antimonotonic in p and monotonic in q.
>
> You may be thinking of nonmonotonic logics, where "nonmonotonic"  
> refers to the deductive closure operation yielding the set of all  
> consequences, not to the logical connectives.

Yep.

> Normally in logic, if a set G of formulas is a subset of a set G',  
> the deductive closure of G is a subset of that of G'.  This does  
> not hold in general in nonmonotonic logics, where deductive closure  
> need be neither monotonic nor antimonotonic.

Yes.

Cheers,
Bijan.

Received on Thursday, 8 March 2007 08:11:41 UTC