Planning in Description Logics: Deduction versus Satisfiability Testing

Description Logics (DLs) are formalisms for taxonomic reasoning about structured knowledge. Adding the transitive closure of roles to DLs also enables them to represent and reason about actions and plans. The present paper explores several essentially different encodings of planning in Description Logics. We argue that DLs represent an ideal framework for analysing and comparing these approaches. Thus, we have identified two essentially different deductive encodings (a "causal" and a "symmetric" one), as well as a satisfiability-based approach. While the causal encoding is more appropriate for reasoning about precondition-triggered causal events, the symmetric encoding is more amenable to reasoning about possible outcomes of courses of actions without actually executing them (while allowing both progression and regression). In the deductive approaches, the existence of a plan corresponds to an inconsistency proof rather than to a model of some formula. Viewing planning as satisfiabili..