% comments on approaches to negation in RuleML % by Benjamin Grosof % created 4/25/03 Approaches to Negation in RuleML by Benjamin Grosof V1 draft 4/25/2003 I. Negation As Failure It appears pretty uncontroversial that we want to support negation-as-failure (NAF). NAF is the most commonly used form of negation in commercially important rule systems, i.e in Prolog, SQL, OPS5 production rules, ECA rules. Hornlog plus NAF is called "Normal" LP or "Ordinary" LP. More precisely, body atoms may have a NAF operator appear immediately before them, in which case they are interpreted as a NAF negative literal. The semantics of negation-as-failure gets a bit complicated, however, when it interacts with recursive/cyclic dependencies among predicates/literals, since in general there may be oscillatory ill-definedness of whether a cyclically-dependent literal is to be entailed as in or out of the model (i.e., conclusion set). The essential example of such oscillatory ill-definedness is the following LP rulebase RB1: p <- fneg p. where "fneg" stands for the NAF operator. In this rulebase, if p is out, then p is in, and p is justifiable as in iff p is out. Yet p cannot both be in and out. Several semantics have been proposed for negation-as-failure in normal LP's. The large majority of the knowledgeable LP R&D community, including myself, prefers/recommends the well-founded semantics (WFS) [due to Van Gelder et al, approx. 1991] for the choice of semantics, as opposed to various other proposals, e.g., stable model semantics. WFS has several virtues: it corresponds well to natural intuitions about what should be entailed, produces exactly one conclusion set / model, which can be tractably computed (worst-case time is quadratic in the size of the propositional instantiation of the rulebase). It uses a third truth value -- "u" for "undefined" -- for the nastily oscillatory cases of cyclic dependence. E.g., in RB1, p is defined as having truth value "u" rather than "t" ("true", i.e., "in") or "f" ("false" in the sense of NAF, i.e., "out"). II. Strong Negation, i.e., "Classical" Negation It is also convenient syntactic sugar to have a form of strong negation, often called "classical" negation -- but a quite limited form of classical negation. Let us call the strong-negation operator "cneg" or "not", and the NAF operator "fneg" or "fail". There is a common approach, which has been implemented many times, and formalized several times in the LP / rules literature. "Extended" Logic Programs [due to Gelfond and Lifschitz, approx. 1990] is probably the best-known theoretical formalization of it. In this approach, the "cneg" operator syntactically may appear immediately before a literal, in the body, or in the head. If NAF is also permitted, the "fneg" operator is permitted immediately before the "cneg" operator, and in the body only. The first, and most basic, aspect of the semantic treatment of strong negation is to view "cneg p", where p is any predicate, as equivalently standing for another "not_p", where "not_p" is a newly introduced predicate. More precisely, any appearance of a literal expression "cneg p(t)" is rewritten as "not_p(t)", where "p" is a predicate and "t" is a tuple of argument terms. A single new predicate "not_p" is introduced for each predicate "p" that appears in the original rulebase. Queries are rewritten in like fashion. Intuitively, what is going on is that one reasons (entails, infers) *separately* about both "sides" (positive and strong-negative) of each predicate "p". This form of classical negation is quite limited. Syntactically, it cannot appear generally in front of arbitrary expressions, but rather only in front of individual literals. Contrapositivity does not hold as it does in classical logic, e.g., from "cneg q <- cneg p" one cannot entail "p <- q". There is no logical property of "the excluded middle" as there is in classical logic: it is not the case that either "p(t)" or "cneg p(t)" must be in the model of the LP for every literal "p(t)". Relationship of Strong Negation to NAF The second semantic aspect of strong negation is its relationship to NAF. Intuitively, if one interprets NAF as weak negation, then one expects that strong negation of a given atom "p(t)" should logically imply the weak negation of that same atom "p(t)", but not (in general) vice versa. I.e., one expects that "cneg p(t)" should logically imply "fneg p(t)" but not (in general) vice versa. This relationship actually involves more than simply rewriting "cneg p(t)" as "not_p(t)"; it requires semantically constraining the relationship between what is entailed about "p(t)" and what is entailed about "not_p(t)". Conflict Handling in presence of Strong Negation The third semantic aspect of strong negation is its relationship to consistency, i.e., to conflict handling. There have been several proposals about this aspect. In classical logic, if one asserts two facts "p" and "cneg p", then there is a global inconsistency; there are no models, and every ground literal is derivable. Gelfond and Lifschitz in their definition of "Extended" LP [approx. 1990] take this same approach. This is rather brittle, which is a serious disadvantage for large-scale and/or multi-authored rulebases. However, when the LP language includes NAF, not just strong negation, then the LP language is already fundamentally non-monotonic and thus capable of representing default reasoning. Other approaches to the conflict handling aspect of the semantics of strong negation are based, accordingly, upon the spirit of default reasoning. They treat strong negation as part of supporting defaults in the generalized LP language. There are several such approaches to defaults in LP, in the literature. The one which appears most practical today is probably Courteous LP. My personal favorite approach to strong negation is, accordingly, to support it as part of the Courteous feature, i.e., as part of the extension of LP to Courteous LP. Courteous LP guarantees consistency of the overall conclusion set, and behaves paraconsistently in that conflict is localized only to the literals directly involved, rather than being "globalized" as in classical logic. E.g., consider the following rulebase RB2: q. r <- q. r <- v. s <- r. p. cneg p <- q. entails the conclusions "q", "r", and "s" which are intuitively justified. Unlike the brittle classical-spirit approach to conflict handling, it does not entail "v", nor "cneg q", nor "cneg r", nor "cneg s". And, rather conservatively, it entails neither side of the unresolved conflict about "p" -- neither "p" nor "cneg p" is concluded. III. Closed-World Axioms for Individual Predicates It is often useful to represent a closed-world axiom for an individual predicate. Generally, one can always view this as a kind of low-priority default. Intuitively, CWA(p), where p is a predicate, says roughly "if 'p(x)' is not concluded after all the explicit rules that can (positively) imply 'p' have had their chance, then conclude 'cneg p(x)', where 'x' is any tuple of ground terms of arity appropriate for 'p'". Intuitively, this is very close to the following rule R3: cneg p(?x) <- fneg p(?x) . here "?x" is a tuple of free variables of arity appropriate for "p". We use "?" to prefix logical variables. There have been a number of different proposed technical formulations for this in the LP/rules literature. In courteous LP, this can be represented rather simply, either (1) as the rule R3; or (2) as the following rule R4 cneg p(?x). where "?x" is a tuple of free variables of arity appropriate for "p" together with additional rules that define the priority of rule R4 relative to other rules in the given rulebase in which R4 appears, e.g., as lower priority than all other rules whose head contains a positive literal in "p". Here, is a rule label, which is simply a name for the rule. A Courteous LP specifies prioritization among rules using a syntactically reserved predicate "overrides" which takes a pair of rule labels as its arguments. E.g., consider the following rulebase RB5: p(a). p(b) <- q(b). q(b). q(c). q(d). cneg p(?x) . overrides(r51, r56). overrides(r52, r56). where "=/=" stands for inequality. Then the Courteous LP RB5 entails the following conclusions: p(a) p(b) q(b) q(c) q(d) cneg p(c) cneg p(d) overrides(r51, r56) overrides(r52, r56) Note that one can write general-form quantified rules about "overrides", enabling one to be concise when specifying the relative prioritization of CWA(p) in large rulebases. IV. Syntactic Sugar for Specifying CWA(p) It might be useful to define a sublanguage of RuleML that corresponds simply to adding strong negation and CWA(p) type rules to Normal LP, without other capabilities for priorities. Let us call this, say, N2LP ("N2" short for "two forms of negation"). An issue is how to define the semantics of this N2LP, however. Since strong negation is explicit in it, there is the potential for conflict. I propose using Courteous LP semantics, i.e., treating this expressive class as a (strict) special case of Courteous LP. We could have a special kind of statement, or perhaps use a special predicate, to specify CWA(p). The floor is open to specific syntactic proposals for this. Also, in full Courteous LP, a specific kind of statement for CWA(p) might be a useful syntactic feature to provide more conciseness in specification, and perhaps to help enable a bit extra performance optimization in inferencing engines. The scope of the CWA(p) would have to be carefully defined, e.g., relative to a particular module vs. relative to the whole rulebase. I thus recommend waiting a bit to finalizing defining such syntax until we have the syntax (and semantics) for a (RuleML) modules mechanism in place.