[ CogSci Summaries home | UP | email ]
http://www.jimdavies.org/summaries/

D. McDermott and J. Doyle (1980). Nonmonotonic logic 1, Artificial Intelligence", Vol. 13, p41-72, 1980

@Article{kn:doy80,
  author =       "D. McDermott and J. Doyle",
  title =        "Nonmonotonic logic 1",
  journal =      "Artificial Intelligence",
  year =         "1980",
  volume =       "13",
  pages =        "41--72",
  key =          "McDermott and Doyle 80",
}

Author of the summary: David Furcy, 1999, dfurcy@cc.gatech.edu

Cite this paper for:

SYSTEMS: TMS is described in terms of the non-monotonic logic.
A formalization of non-monotonic logic using the modality M.
Soundess and completeness of the non-monotonic logic.
Decidability of non-monotonic sentential (propositional) logic
A generalized tableau method as a proof procedure for the non-monotonic sentential calculus.
The weakness of the non-monotonic logic described lies in its semantics (namely the semantics of the modality M).

Summary

The authors extend standard logic into a non-monotonic logic which allows new axioms to be added (through observations for example) that invalidate previously made inferences. Such non-monotonic reasoning capabilities seem crucial for systems with incomplete information about their environment. This paper only deals with routine revision of beliefs (i.e. how to deal with exceptions to general facts) as opposed to world-model reorganization (e.g., the Copernican revolution).

The meaning of the modality M, namely "consistency with current beliefs", is formalized by extension of the notions of deductive closure and fixed point used in standard (monotonic) logics. After a description of a model theory for the new logic, a proof procedure is presented based on the tableau procedure used in standard logic. The main theoretical results of this paper are the completeness of non-monotonic logic, the decidability of non-monotonic sentential calculus (but the non-monotonic predicate calculus is not even semi-decidable). This non-monotonic logic is showed to be adequate for describing the behavior of the TMS system which maintains consistency by preventing not p and Mp to be true simultaneously, as well as p and not p to be true simultaneously (using dependency-directed backtracking). Unfortunately, the new logic fails to capture a completely coherent notion of consistency,

Detailed outline

Review of some concepts in monotonic logic

A theory is a set of axioms (denoted by A or B in the following). The Sentential (or propositional) Calculus (SC) contains axioms for a language that only contains propositional variables. The Predicate Calculus (PC) is a theory for an extended language (and an extended set of axioms) containing variables and quantifiers.
Now, if S is a set of formulas, then S |- p iff p is derivable from S using the available inference rules and Th(S) = {p such that S|- p}. So, Th(S) is the set of all formulas (theorems) that are (monotonically) derivable from S and the inference rules and axioms in the logic. Therefore, Th(S) is the closure operator for |-.

Monotonicity property:

A is included in Th(A), and
If A is included in B, then Th(A) is included in Th(B)

Idempotence property: Th( Th(A) ) = Th(A). Thus, Th(A) is the (smallest) fixed point of the Th closure operator for monotonic inference rules.

A model of S is an interpretation V which satisfies all formulas in S.

An extension of these concepts to non-monotonic logic

A new modality operator is introduced, namely Mp to mean that "p is consistent with all current beliefs." The dual of M, not M (not p) is denoted Lp. This new modality enables non-monotonic inferences based on guesses/assumptions. Let us define As(A,S) = { Mq such that (not q) is not in S} - Th(A), that is the set of assumptions consistent with S and that are not monotonically derivable from the axioms. Furthermore, let us define the analogue of Th for NM logics, namely NM(A,S) = Th(A u As(A,S)). Thus, NM(A,S) is Th(A) u the set of all consistent assumptions plus all formulas (monotonically) derivable from them and Th(A). Finally, TH(A) is the intersection of all fixed points of NM(A,-) or the entire language if there are no such fixed points. A |~ p iff p belongs to TH(A).

A NM theory has a model only if the operator NM(A,-) has a classically consistent fixed point. A non-monotonic model of A is a pair (V,S) where S is a fixed point of A and V is a (monotonic) model of S. A NM theory can have zero, one, several or infinitely many fixed points. In the first case, the theory is inconsistent. Theoretical results: NM-PC is sound and complete, that is A|~p iff |=p (provability is equivalent to validity). However, the main weakness of the logic lies in its semantics since it ispossible for Mp to be true in some model even when not p is derivable. This is because the meaning of Mp does not only depend on that of p, but also on the available axioms.

Many new concepts are defined, such as arguability (the nearly dual of provability: p is arguable from A if p is in at least one fixed point of A) and assumability (p is assumable in a consistent theory A if the theory A u {p} is also consistent). The semantical weakness of the NM logic means that the correlation between assumability of p and arguability of Mp is weak.

Summary author's notes:

none

Back to the Cognitive Science Summaries homepage
Cognitive Science Summaries Webmaster:

JimDavies ( jim@jimdavies.org )

Last modified: Mon Apr 5 09:02:17 EDT 1999