A first-order Temporal Logic for Actions

TL;DR

This paper introduces a multi-modal first-order temporal logic for actions, enabling the expression of complex temporal and state-related aspects of actions, with applications in action theory and a decidable fragment.

Contribution

It develops a novel multi-modal first-order temporal logic with unification and quantification, and provides tableaux rules for a decidable fragment.

Findings

Logic can express various temporal aspects of actions

Decidable fragment with tableau rules

Applicable to action theory and temporal reasoning

Abstract

We present a multi-modal action logic with first-order modalities, which contain terms which can be unified with the terms inside the subsequent formulas and which can be quantified. This makes it possible to handle simultaneously time and states. We discuss applications of this language to action theory where it is possible to express many temporal aspects of actions, as for example, beginning, end, time points, delayed preconditions and results, duration and many others. We present tableaux rules for a decidable fragment of this logic.