Mechanized Reasoning About Actions Specified in .4
Sakthi Subramanian · 1993
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 com-plete partial descriptions of the world are usually deemed necessary. This leads to non-monotonic reasoning which has proven to be difficult to for-malize. 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 for-realizing the mapping from partial descriptions of the world to the models of the world usually for-realized by applying default rules to partial de-scriptions. We formalize this mapping by includ-ing partial descriptions of the world as explicit ob-jects 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. *The work described here was supported in part by NSF Grant MIP-9017499.