Implementing Temporal Action Logics

Abstract

The aim of artificial intelligence (AI) research is the design and creation of systems capable of succeeding at tasks that require intelligence. Although the exact definition of intelligence is subject to much debate, it is more or less agreed upon that an intelligent system should be capable of reasoning about the effect of actions performed by itself and others within an environment, and creating and executing goals and actions.

A main project for the AIICS department at the Linköping University embodies the development of an autonomous, or intelligent, UAV (an unmanned aerial vehicle, in this case a helicopter). It uses a formalism for reasoning about action and change called Temporal Action Logic (TAL) to specify its environment, its goals, its actions and the results of these actions. For such a risk-sensitive system it is important that this reasoning can be performed efficiently so that the UAV can respond to events quickly. The work presented in this thesis takes on this last challenge. We explore to what extend increasingly expressive versions of temporal action logics can be implemented into existing theorem provers in a principled manner, while focusing on efficiency.

The first theorem-proving formalism that is used is logic programming. We show that a constrained version of TAL can be transformed into a sound logic program. We furthermore show that this constrained version cannot be relaxed any further while preserving a valid translation to a logic program.

The second formalism that we discuss is SAT Modulo Theories (SMT), which is a decision problem for logical first-order formulas with respect to combinations of background theories of which TAL combines several. We explore the possibility and computational feasibility of encoding TAL theories as SMT problems. We provide benchmarks results for different scenarios and compare it with an existing implementation that uses answer set programming.

An application called TALTranslator has been developed, which allows the user to specify a TAL theory and offers the possibility for the automatic translation of this theory into an off-the-shelf theorem prover.