. Because    is consistent,   / 
" 
=  , and hence by definition      , and as   →
. 

extension of Assume that such that false /     Let W be a model such that for all
= 
= 
.

of its disjuncts is in . By definition this disjunct is true in . Hence every clause in .  is true in
□
.

An alternative way of obtaining the intractability of cautious reasoning for all classes with a Horn objective part is to apply Theorem 8.2 in (Kautz & Selman, 1991)    that reduces brave reasoning to cautious reasoning by adding a default :         and the intractability result for brave reasoning in Horn classes (Stillman, 1990). This is not applicable to the 2-literal case because in it brave reasoning is tractable.

Theorem 4.13 Testing defaults with conclusions that are conjunctions of literals, is co-NP-hard. The Proof: Let be a set of clauses. We show that there is a default theory such that
≠ c false if and only if    is satisfiable. Let    be the set of propositional variables that occur in . Let be an injective function that maps each clause to a propositional variable = ( ) such that / . Define the set of defaults as follows.

fa ls e fa ls e
Assume that is satisfiable. Let be a model such that = . Let

$$\begin{array}{r l r l}{t}&{{}=}&{C n(t)}\end{array}$$
el such that $\quad=\quad.$ Let . 
$$\begin{array}{r l r l r l r l r l}{{}}&{{}}&{{}}&{{}}&{{}}&{{}}\\ {={}}&{{}}&{{}}&{{}}&{{}}&{{}}\\ {\end{array}$$
$\nu$ . 
Obviously   ' is consistent and it does not contain false. 2  Clearly   ' is an extension of
= ( ) 
there is an extension soft such that ' Because Because for all   =   ( )
with Assume that there is an extension of such that false / . Let Let Let model such that for all propositional variables false        false    GD(         ) for no    =    ( )
. Now GD(          ) for some 
=  ( )    and hence :
and

= . Because this holds for all      , finally
□
l