Toward efficient default reasoning by David Etherington and James Crawford.


Default reasoning aims to formalize the "notion of jumping to conclusions". A brief but complete introduction to non monotonic reasoning is available here.

Harder then classical logic. Even though it was supposed to imitate human reasoning (jumping to conclusions, and therefore fast). Two things make it hard:

  • need to check for consistency of a formula respect to a KB many times during a proof.
  • the order in which default rules are used is fundamental
The first is more important than the second. So, the authors, in this paper, tackle the first problem.

There are sufficient conditions to check for consistency (that are fast), but they are useless in practical environment because they can be used only under conditions that normally are not satisfied:

  • a formula f in CNF is consistent if all the literals in not f don't occur in the KB. Or if a literal in not f appears only in formulas where the other literals are pure literals. A pure literal is a literal whose complement never appears in the KB.

Proposed solution: two approximations,

  • consider a subset of the Kb (called context) as the KB against which to test consistency
  • use approximate fast consistency checks


Observations (starting points for discussion)

Further readings

-- FabrizioMorbini - 20 Dec 2006

Edit | Attach | Watch | Print version | History: r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r1 - 2006-12-20 - FabrizioMorbini
  • Edit
  • Attach
This site is powered by the TWiki collaboration platform Powered by PerlCopyright © 2008-2017 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding URCS? Send feedback