The characterization of the semantics of NAT's in terms of second order logic theories including circumscription formulas and proposition 1 in [Lifschitz1995] allow us to prove the equivalence between the following axiom sets.

Now, we use several rules for computing circumscription described in [Lifschitz1993]. The first equivalence below can be proved using formula (19) and proposition 2 in [Lifschitz1993]. The second equivalence uses formula (19) and proposition 3 in that paper.

Using the equivalence (27) in
section 3.2 of [Lifschitz1993], we can
prove that is
equivalent to the following formula, which
does not depend on *better*.

Finally, predicate completion [Lifschitz1993] give us the result of the theorem.

Theorem 1 shows that the nested abnormality
theory described by is
equivalent to the second order theory
whose axioms are , and
. This means that using theorem
proving methods for first order
logic we can
decide the selectability of any situation
with respect to the strategy described by
axioms to . For
example, we can prove that action
*Move(A,T)* is selectable at
(i.e.,
),
but action *Move(C,T)* is not (i.e.,
).

Tue Jul 21 09:54:27 PDT 1998