Encoding Definitional Fragments of Temporal Action Logic into Logic Programming

Abstract. Temporal Action Logics (TAL) is an expressive class of nonmono-tonic temporal logics for reasoning about action and change. In previous work, it has been shown that a very general fragment of the logic can be reduced to first-order logic with equality. Consequently, standard theorem proving techniques can be used to reason in TAL. TAL is intended to be used for robotics. In this case, standard theorem proving techniques are too general and do not provide efficient decision procedures. The goal of this article is to identify a limited subset of TAL that can be directly mapped to a normal logic program. Although quite restric-tive, this sets the lower bound on what can be done with direct mappings to logic programs. Discussions concerning extensions to the restricted fragment are also provided.