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