A Logic for Reasoning about Actions and Explicit Observations

摘要

We propose a formalism for reasoning about actions based on multi-modal logic which allows for expressing observations as flrst-class objects. We introduce a new modal operator, namely [o a], which allows us to capture the notion of perceiving an observation given that an action has taken place. Formulae of the type [o a] mean 'after perceiving observation o, given a was performed, necessarily ip'. In this paper, we focus on the challenges concerning sensing with explicit observations, and acting with nondeterministic effects. We present the syntax and semantics, and a correct and decidable tableau calculus for the logic.