Causal action theories and satisfiability planning
Charles H. Turner, Vladimir Lifschitz · 1998
This dissertation addresses the problem of representing and reasoning about commonsense knowledge of action domains. Until recently, most such work has suppressed the notion of causality, despite its central role in everyday talking and reasoning about actions. There is good reason for this. In general, causality is a difficult notion, both philosophically and mathematically. Nonetheless, it turns out that action representations can be made not only more expressive but also mathematically simpler by representing causality more explicitly. The key is to formalize only a relatively kind of causal knowledge: knowledge of the conditions under which facts are In the first part of the dissertation we do this using inference rules and rule-based nonmonotonic formalisms. As we show, an inference rule $\phi\over\psi$ can be understood to represent the knowledge that if is caused then $\psi$ is (Notice that we do not say $\phi$ causes $\psi$.) This leads to and expressive action representations in Reiter's default logic, a rule-based nonmonotonic formalism. This approach also yields action descriptions in logic programming, thus raising the possibility, at least in principle, of automated reasoning about actions and planning. In the second part of the dissertation, we introduce a new modal non-monotonic logic--the logic of universal causation (UCL)--specifically designed for describing the conditions under which facts are We show that UCL provides a more traditional semantic account of the mathematically approach to causal knowledge that underlies our causal theories of action. For instance, instead of the inference rule $\phi\over\psi$ we write the modal formula $\subset\phi \supset \subset\psi$, where $\subset$ is a modal operator read as caused. In the third part of the dissertation, we show that a subset of UCL is well-suited for automated reasoning about actions. In particular, we show that the class of simple UCL theories provides an expressive basis for the computationally challenging task of automated planning. Simple UCL theories have a concise translation into classical logic, and, as we show, the classical models of the translation correspond to valid plans. This enables satisfiability with causal action theories, with state of the art performance on large classical planning problems.