#### Paper

Toward efficient default reasoning by David Etherington and James Crawford.

#### Summary

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

#### Comparison

#### Observations (starting points for discussion)

#### Further readings

-- FabrizioMorbini - 20 Dec 2006