http://www.jimdavies.org/summaries/

@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", }

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

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,

Now, if S is a set of formulas, then S

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

A

A NM theory has a model only if the operator NM(A,-) has a classically consistent fixed point. A

Many new concepts are defined, such as

- 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