next up previous
Next: Advice Taking Scenario Up: Blocks World Example Previous: Theorem 1


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 setsgif.


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 tex2html_wrap_inline760 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 gif is equivalent to the second order theory whose axioms are tex2html_wrap_inline750 , gif and gif. This means that using theorem proving methods for first order logicgif we can decide the selectability of any situation with respect to the strategy described by axioms gif to gif. For example, we can prove that action Move(A,T) is selectable at tex2html_wrap_inline736 (i.e., tex2html_wrap_inline768 ), but action Move(C,T) is not (i.e., tex2html_wrap_inline770 ).

Josefina Sierra
Tue Jul 21 09:54:27 PDT 1998