In the ongoing discussion about monotonic vs. non-monotonic negation (better known as negation as failure), it is often overlooked that not only non-monotonicity is an issue but actually there are several definitions of both monotonic and non-monotonic forms of negation in the literature) with subtle but important differences. On this page we aim to shed light on the "landscape" of different forms of negation and clarification of terminology. This overview is by no means to be understood to be exhaustive, but shall cover and clarify the most prominent forms of negation in the context of logics and rule languages, especially those mentioned in discussions within the RIF working group.
For the sake of simplicity we will restrict ourselves to the propositional case although all mentioned logics have first-order extensions.
First of all, we treat the most important forms of negation in non-monotonic logics. Monotonicity meas that whenever some sentence φ is provable from a theory T, φ will still be provable from any superset of T.
In order to illustrate the differences betwen different forms of negation, we choose an axiomatic representation of classical logic here. As well known, classical logics can be characterized by the following axiomatization
- φ → (ψ → φ)
- (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))
- (φ ∧ ψ) → φ
- (φ ∧ ψ) → ψ
- (φ → ψ) → ((φ → χ) → (φ → (ψ ∧ χ)))
- φ → (φ ∨ ψ)
- ψ → (φ ∨ ψ)
- (φ → χ) → ((ψ → χ) → ((φ ∨ ψ) → χ))
- (φ → ψ) → ((φ → ¬ψ) → ¬φ)
- ¬φ → (φ → ψ)
- φ ∨ ¬φ
plus modus ponens as its only inference rules. The last axiom, the so called law of the excluded middle (LEM), deserves special interest. Since it allows non-constructive inferences, e.g. the double negation axiom
- 11'. ¬¬φ → φ
is provable in classical logics.
Intuitionistic logic is a part of classical logic, that is, all formulas provable in intuitionistic logic are also provable in classical logic. However, intuitionistic logics disallows indirect proofs, that is all intuitionistic proofs must be constructive. For more details, see e.g. [Wolfram Mathworld http://mathworld.wolfram.com/IntuitionisticLogic.html]:
Intuitionistic logic (due to Heyting ) is simply the logic axiomatized by 1-10 from above, i.e. LEM is dropped and the double negation axiom no longer holds.
Alternatively, intuitionistic negation can be characterized by viewing ¬φ as an abbreviation for the formula φ→ ⊥, where ⊥ can be interpreted as contradiction. Then intuitionistic logic then can be axiomatized by the axioms of positive logic (1-8 from above) plus the additional axiom
- 9'. ⊥ → φ
Thus, proving ¬φ intuitionistically may be viewed as "proving the assumption φ leads to a contradiction", rather than proving that φ is wrong.
Note that the remarks on intuitionistic negation here mainly serve to clarify historical development of logics, where intuitionistic negation plays a significant role. Since the RIF condition language will very likely not include a proper implication connective (unlike in "intuitionistic logic programs", see e.g. ), we don't have to consider the heavy apparatus of Kripke semantics for intuitionistic (or intermediate) logic in order to understand the issue of having two kinds of negation. Partial logic  is simpler and probably sufficient for our purposes.
Constructive (aka Strong) Negation
As mentioned above, intuitionistic logic is in a sense "constructive" since only formulae entailed are those which can be constructively proved. Constructive negation (due to Nelson in 1949) adds to intuitionistic logic the insight that primitive propositions may not only be constructively verified but also be constructively falsified. Two essential features characterize the concept of constructive negation:
- by constructive negation one can characterize atomic negative information.
- there exists an effective procedure to reduce falsification of complex statements to verification or falsification of its parts by a normal form transformation.
We will use the symbol '-' to denote strong negation, in order to distinguish it from '¬' in the following. Actually, Nelson presented strong negation as an alternative to intuitionistic negation, but we treat them here in a common framework presenting constructive logic as an extension of intuitionistic logic, due to Vorob'ev. Indeed, intuitionistic negation in constructive logic is definable by:
- ¬φ := φ → -φ
where constructive logic is axiomatized by the axioms of intuitionistic logic plus the following:
- N1. -(φ → ψ) ↔ (φ ∧ -ψ) N2. -(φ ∧ ψ) ↔ (-φ ∨ -ψ) N3. -(φ ∨ ψ) ↔ (-φ ∧ -ψ) N4. φ ↔ - - φ N5. -¬φ ↔ φ N6. (for atomic φ) -φ → ¬φ
Constructive logic with these additional axioms is a conservative extension of intuitionistic logic in the sense that any formula of constructive logic without strong negation in constructive logic is a theorem iff it is a theorem in intuitionistic logic. Axioms N1-N5 allow the usual normal form transformation known from classical logic, by elimination of double negation and de Morgan's laws, in order to move negations in front of atomic formulae only. By N6, we see why constructive negation is also called "strong" negation. This obviously still holds in case we would reintroduce LEM to the combined logic, i.e. constructive negation is indeed stronger than classical negation.
Strong negation is important for us, since it has also been introduced in dialects of logic programming. In particular, what Gelfond and Lifschitz called "classical" negation in  is in fact strong negation.
Two Kinds of Negation in Partial Logic
Intuitionistic logic is mainly a logic about the implication connective → that captures constructive deduction. Since the RIF condition language will probably not include an implication connective, using intuitionistic logic or constructive logic with strong negation for RIF would be like breaking a fly on the wheel. A much simpler logic allowing to distinguish between two kinds of negation is partial logic, which assigns both a truth and a falsity extension to a predicate such that they need not be the set-theoretic complement of each other.
This allows for "truth value gaps" (partiality) and for "truth value clashes" ("paraconsistency"). Thus partial logic defines a small family of three- and four-valued logics (depending on the requirements that are imposed on interpetations and the choice of definition clauses for connectives). It also allows to distinguish between different kinds of predicates, which may be partial or total. Classical logic can be viewed as the special (overidealized) case of partial logic where all predicates are total (an assumption that seems to be justified for mathematics, but not for knowledge representation).
In partial logic, there is a strong negation (also called "Kleene negation") and a weak negation proposed by Lukasiewicz. While strong negation represents explicit falsity, weak negation represents non-truth. Partial logic is better-suited to knowledge representation than classical logic. E.g. the notion of a minimal model does in fact not make much sense in classical logic. Classical interpretations, as total truth value assignments, cannot be compared with each other in terms of their information content. However, minimal means informationally minimal and therefore requires a notion of interpretations with information content as provided by partial interpretations.
Negation-as-failure can be explained as weak negation under the preferential semantics of partial minimal/stable models.
Negation-as-failure, often also called "negation as failure to proof", or default negation, does not behave monotonically: in the following rule (we use the same symbols '←' and '¬' as above here to denote implication and negation as failure)
a ← ¬ b
a is derivable from this rule whenever b fails to be provable. Thus, assuming that b is not provable from theory T, a would be derivable when the rule is added to T, but whenever we add b to T, a will no longer be derivable from this rule, i.e. ¬ behaves nonmonotonically. Consequently, monotonic logics can not serve as a basis to define the semantics of negation as failure, and thus several alternative semantics have been defined in the literature to define nonmonotonic negation.
In the following, whenever we speak of a rule (or ruleset, resp.), we mean generally (sets of) formulae of the form:
- φ ← ψ
where φ and ψ are possible complex formulae built from connectives ∧, ∨, ¬ as usual. We say that a rule (ruleset) is normal, if φ is atomic and ψ is a conjunction of possibly negated atomic formulae, and disjunctive if φ is a disjunction of atomic formulae and ψ is a conjunction of possibly negated atomic formulae.
φ is also called head, and ψ the body of the rule.
Negation-as-Failure in the Case of a Stratified Rule Set
A normal ruleset is called stratifiable, whenever negation is acyclic, i.e., no negative body atom refers recursively to itself. E.g., a rule set containing the following rule
a ← ¬ a
is not stratifiable.
There is wide agreement on the semantics of stratifiable rules: they have a unique minimal model, which is their only intended model, according to the perfect model semantics . In a nutshell, this semantics allows to compute the unique minimal model of a normal ruleset stepwise, by dividing it into strata which depend on each other by negation, i.e. only the heads of rules of lower strata are allowed to occur negatively in rule bodies of higher strata.
Also, when adding complex formulae in rule bodies there is agreement on how to deal with this generalization .
Negation-as-Failure in the Case of a Non-Stratifiable Rule Set
For rule sets that are not stratifiable the semantics of negation-as-failure becomes much more difficult: there is no simple intuition about the intended models of a non-stratifiable rule set. It is clear that not all minimal models are intended models, but it also seems that not all intended models are minimal due to the inclusive semantics of disjunction. The two most prominent proposals for the semantics of non-stratifiable rules are the stable model semantics and the well-founded semantics (see below).
Two useful test cases for semantics of non-stratifiable rules are the odd loop a ← ¬ a and the even loop a ← ¬ b, b ← ¬ a.
Notice that according to classical logic the odd loop allows to infer a, while according to intuitionistic logic it only allows to infer ¬¬a, which is not equivalent to a, intuitionistically .
The even loop seems to represent the disjunctive information a ∨ b. This is not only suggested by classical logic, but also by the minimal model semantics and by the stable model semantics.
Stable Model and Answer Set Semantics
The stable model semantics for negation-as-failure has been defined in . Stable models are not necessarily unique, a set of normal rules may have several stable models (as in the case of the even loop), or it may have no stable model (as in the case of the odd loop).
The stable model semantics has been extended to additionally allow for strong negation (called "classical" therein) and disjunctive rules in  where the term stable model has been given up in favor of answer set.
Extensions of normal rules to allow for more connectives have been defined in [11,12], a polynomial reduction to disjunctive rules has been proposed in .
-TO BE COMPLETED-
The well-founded semantcs for normal rulesets has been defined in . Each normal ruleset has a unique well-founded model, which does, however, not capture the implicit disjunctive information as represented by even loops. Thus, in the case of the even loop, the well-founded model is the empty set.
There is currently no agreement on how to extend the well-founded semantcs to disjunctive or more general rules. This problem together with the fact that the well-founded semantics ignores implicit disjunctive information seems to indicate that it defines rather a proof theory but not a model-theoretic semantics.
-TO BE COMPLETED-
Some of the explanations on this page are based on discussions with and notes from Sergeij Odintsov and David Pearce.
- D. Pearce: From here to there: stable negation in logic programming. In D. M. Gabbay and H. Wansing, editors, What is Negation?, pages 161--181. Kluwer Academic Publishers, 1999.
- A. Heyting: Die formalen regeln der intuitionistischen logik. Sitzungsberichte der Preussischen Akademie von Wissenschaften. Physikalisch-mathematische Klasse, 42--56, 1930.
- D. Nelson: Constructible falsity. J. Symbolic Logic, 14(1):16--26, 1949.
- N. Vorob'ev: Constructive propositional calculus with strong negation. Transactions of Steklov's Institute, 72:195-227, 1964. In Russian.
A. J. Bonner, L.T. Mc Carty: Adding Negation-as-Failure to Intuitionistic Logic Programming. Proc. of the North American Conference on Logic Programming (NACLP). MIT Press, 681--703, 1990. http://citeseer.ist.psu.edu/bonner92adding.html
H. Herre, J. Jaspars, G. Wagner: Partial Logics with Two Kinds of Negation as a Foundation for Knowledge-Based Reasoning. In D.M. Gabbay and H. Wansing (Eds.), What is Negation?, Kluwer Academic Publishers, 1999. http://www.informatik.tu-cottbus.de/~gwagner/papers/PartialLogics.pdf
M. Gelfond, V. Lifschitz: Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing 9(3/4):365--386, 1991. http://citeseer.ist.psu.edu/gelfond91classical.html
- T.C. Przymusinski: Perfect Model Semantics, Proc. 5th Int. Conf. and Symp. on Logic Pro- gramming, MIT Press, Cambridge, Ma, 1988, pp. 1081-1096.
- J.W. Lloyd and R.W. Topor. Making Prolog more Expressive. Journal of Logic Programming, 3:225-240, 1984.
M. Gelfond and V. Lifschitz. The Stable Model Semantics for Logic Programming, In: Proc. of the Fifth Joint International Conference and Symposium. The MIT Press, 1988, 1070--1080. http://citeseer.ist.psu.edu/gelfond88stable.html
H. Herre and G. Wagner: Stable Models are Generated by a Stable Chain. Journal of Logic Programming 30:2 (1997). http://citeseer.ist.psu.edu/herre97stable.html
V. Lifschitz, L. Tang, and H. Turner. Nested Expressions in Logic Programs. Annals of Mathematics and Artificial Intelligence, 25(3-4):369–389, 1999. http://citeseer.ist.psu.edu/lifschitz99nested.html
D. Pearce, V. Sarsakov, T. Schaub, H. Tompits, S. Woltran. Polynomial Translations of Nested Logic Programs into Disjunctive Logic Programs. Tech Report, 2002. http://citeseer.ist.psu.edu/550878.html
A. Van Gelder, K.A. Ross, and J.S. Schlipf. The Well-Founded Semantics for General Logic Programs. Journal of the ACM 38(3):620--650, 1991. http://citeseer.ist.psu.edu/gelder91wellfounded.html