Mechanized Reasoning About Actions Specified in A

Contents

In order to prove that a sequence of actions can transform an initial situation of the world to a goal situation when complete knowledge of the world is never available, default rules that serve to complete partial descriptions of the world are usually deemed necessary. This leads to non-monotonic reasoning which has proven to be difficult to formalize. In this paper, we present a mechanized formalization for default reasoning about actions specified in the language .A in the Boyer-Moore logic, a first-order logic. The main idea is to use the Boyer-Moore logic as a meta-language for forrealizing the mapping from partial descriptions of the world to the models of the world usually forrealized by applying default rules to partial descriptions. We formalize this mapping by including partial descriptions of the world as explicit objects in the universe of discourse and define a Lisp interpreter that takes a partial description as an argument and simulates the default behavior of the world by applying the "commonsense law of inertia" to the partial description. We formalize some typical examples and show mechanicalproofs requiring default reasoning about actions.