Corollary 5.20 Testing 
= for strict total orders P and literals in any of the classes of default theories below is NP-hard.

| normal unary                               | Horn clauses      |
|--------------------------------------------|-------------------|
| normal unary                               | 2-literal clauses |
| od ered unary                              | literals          |
| prerequisite-free ordered unary   literals |                   |

5.2.3 TRACTABLE CLASSES Next we give a restricted tractable class of prioritized default theories for which the unique P-preferred L extensions can be computed by using P as the order in which the application of defaults is attempted. Exhaustive search is avoided because there is no need to retract a decision to apply a default. The theorem is given in a general form for any tractable subset of classical propositional logic, like Horn clauses, 2-literal clauses, or 1-literal clauses. The theorem and the algorithm are part of the folklore of nonmonotonic reasoning.

Theorem 5.21  Let F  be a class of formulae such that satisfiability testing for F takes polynomial time in the size of . Let C be a class of default theories such that for some finite set      F and F is finite. Then for ∆ C,
F,
and strict total orders P on the defaults in ∆ , the problem of testing ∆ = f is solvable in polynomial time on the size of Proof: By Lemma 5.4 there is at most one P-preferred L extension for each member of C,
and because the defaults in members of C are normal, there is at least one extension for each member of C by Theorem 3.1 in (Reiter, 1980). Therefore there is exactly one P-preferred L extension for each member of C . A decision procedure for the class of default theories stated in the theorem is given in Figure 8.  The procedure computes a set that consists of and the conclusions of the generating defaults of the extension Cn (  ) of
, and returns true if and only if    =   .

Let : 1 1 1 1 1 1 1 1 be the ordering P of defaults in is inconsistent the procedure returns true.  In this case Cn (     ) =      is the only extension of which agrees with the statement of the lemma. Otherwise extensions of are consistent.  Define
::::::::: and Π i = - i i
; for all
. The correctness 0
; = : 1   1 proof is by induction on and we obtain the P -preferredness t of Cn ( ) as the case =
Induction hypothesis: for all if is consistent, is a maximal consistent 0 subset of Π i such that j, and Cn( j) is a P   ( j ×  j)-preferred L extension of The induction proof is straightforward.  That the procedure runs in polynomial time on the size of is also obvious.  Thus any polynomial time subset C of classical propositional logic produces a tractable class of default theories.

Without priorities reasoning with prerequisite-free normal default rules and Horn clauses is NP-complete (Stillman, 1990). For normal defaults, tractability can be obtained also for defaults with prerequisites if suitable restrictions are imposed on the prerequisites, conclusions, and the objective parts of the default theories. Next we present such a class that is neither subsumed by nor subsumes the tractable prerequisite-free classes. The idea behind