On Action Theory Change
  As historically acknowledged in the Reasoning about Actions and Change
community, intuitiveness of a logical domain description cannot be fully
automated. Moreover, like any other logical theory, action theories may also
evolve, and thus knowledge engineers need revision methods to help in
accommodating new incoming information about the behavior of actions in an
adequate manner. The present work is about changing action domain descriptions
in multimodal logic. Its contribution is threefold: first we revisit the
semantics of action theory contraction proposed in previous work, giving more
robust operators that express minimal change based on a notion of distance
between Kripke-models. Second we give algorithms for syntactical action theory
contraction and establish their correctness with respect to our semantics for
those action theories that satisfy a principle of modularity investigated in
previous work. Since modularity can be ensured for every action theory and, as
we show here, needs to be computed at most once during the evolution of a
domain description, it does not represent a limitation at all to the method
here studied. Finally we state AGM-like postulates for action theory
contraction and assess the behavior of our operators with respect to them.
Moreover, we also address the revision counterpart of action theory change,
showing that it benefits from our semantics for contraction.
