5.2.2 INTRACTABLE CLASSES WITH TOTAL PRIORITIES
The next theorems are based on reductions from intractable problems of brave reasoning in Reiter's default logic to prioritized default logic with total priorities. Theorem 5.17  Let F  be a class of formulae and C  a class of finite default theories such tha t
- if C, then C where     F and   is a propositional
.

variable that does not occur in    or    , and
- each member of C has at least one extension.

The problem of testing ∆ = b   for ∆    C and       F is polynomial time many-one reducible to the problem of testing ∆ ′ = p   where ∆ ′   C,    is a propositional variable, and P is a strict total order on defaults in ∆ ¹ .

C be a default theory, Proof: Let that does not occur in         or  . Let P be any strict partial order on such that  :     is the P-least element. We claim that          = b    if and only if
==
preferred to extensions if it is possible to apply it, and   belongs to those extensions if and oly if   belongs to them.

As a corollary, together with a theorem that shows the intractability of brave reasoning of the class in Reiter's default logic (Kautz & Selman, 1991), we obtain the following result.

Corollary 5.18  Testing Theorem 5.19  Let C  be a class of finite default theories such that the conclusion of each default is a literal and each member of C has at least one extension. The problem of testing
∆ = b  for ∆   C and literals  is polynomial time many-one reducible to the problem of testing A = 4 where T is a strict total order on defaults in A.

Proof: Let ∆ =           be a default theory in C . We reduce testing ∆ = b  to ∆ = f  as follows. Let t be the set of defaults with as the conclusion. Let T be a strict total order on such that 'x ( \ ') T. We claim that ∆ = b if and only if ∆ = f Assume that A \#b . Because by assumption there is at least one extension of A, by Lemma 5.4 there is exactly one T-preferred r extension   of ∆ . Clearly   /   . Therefore A // .

Asssse
. If
= .

then clearly ∆ = f . Assume that
' is an extension of ∆ such that   /    . Now appl(      '). As  '     ' for all  'T  and not appl( ' ') for all '   ', there is no 'T  such that appl( ' ' ). Hence ' is not T-preferred L . Therefore belongs to all T-preferred L extensions of ∆ and ∆ = 4 .

□
The following corollary is obtained with the intractability results of brave reasoning by Kautz and Selman (1991) and Stillman (1990) for the classes mentioned.