A logic of intention and attempt (Q934779)

This paper presents a logic of intention and attempt (LIA) to enable reasoning about the dynamics of intentions and actions, mediated by the notion of attempt in action execution. Here actions are construed as basic actions that are essentially bodily movements of an agent. Attempts are construed as mental processes, while intentions are mental states. The logic takes the form of a multi-modal logic with operators for (linear) time (\(\square\phi\), for `\(\phi\) is true now and henceforth always'), belief (\(\text{Bel}_i\phi\), for `agent \(i\) believes \(\phi\)'), goals (\(\text{Goal}_i\phi\), for `agent \(i\) has chosen the goal that \(\phi\)'), and importantly attempts (\(\langle\langle i: \alpha\rangle\rangle\phi\), for `agent \(i\) tries to move its body in way \(\alpha\) and \(\phi\) holds after \(i\)'s attempt'). The language is provided with a typical Kripke-type model theory, with each modality interpreted through its own accessibility relation. Much of the paper provides an axiomatization for the logic with attention to the interaction of these modalities, and in the semantics attention to the corresponding conditions on the respective relations. Soundness and completeness for LIA are claimed based on standard Sahlqvist results.