There seems to be a good amount of work on the formal semantics of tense, e.g. statements of the form "Dave ate the cookie," and also of modality, e.g. statements of the form "Dave might be at home."
But I've seen next to nothing of the formal semantics of the coordination of these two phenomenon, e.g. "Dave might have eaten the cookie."
Are there resources on this? In particular, the formal semantics of tensed statements with epistemological modality.
Maybe this is what the doctor ordered:
E. Allen EMERSON, CHAPTER 16 - Temporal and Modal Logic,
Editor(s): JAN VAN LEEUWEN,
In Handbook of Theoretical Computer Science, Formal Models and Semantics, Elsevier, 1990, Pages 995-1072, ISBN 9780444880741,
https://doi.org/10.1016/B978-0-444-88074-1.50021-4.
(https://www.sciencedirect.com/science/article/pii/B9780444880741500214)
Abstract: Publisher Summary
This chapter discusses temporal and modal logic. The chapter describes a multiaxis classification of systems of temporal logic. The chapter describes the framework of linear temporal logic. In both its propositional and first-order forms, linear temporal logic has been widely employed in the specification and verification of programs. The chapter describes the competing framework of branching temporal logic, which has seen wide use. It also explains how temporal logic structures can be used to model concurrent programs using non-determinism and fairness. The chapter also discusses other modal and temporal logics in computer science. The chapter describes the formal syntax and semantics of Propositional Linear Temporal Logic (PLTL). The chapter also describes the formal syntax and semantics for two representative systems of propositional branching-time temporal logics.
But that one’s hard to get; here an open-access paper:
https://ojs.aaai.org/index.php/AIIDE/article/download/12836/12683
Their system appears to include time as a primitive type, and something called “Impulse” to handle I believe modality - where modality has something to do with one’s attitudes, perhaps, towards other possible states of affairs, or classes of states of affairs?
A story encoded in Impulse consists of 6 parts:
- A time basis T , which is a set of intervals
- An object type hierarchy, which consists of subset defini- tions of a root set O that contains all objects
- An action type hierarchy, which consists of subset defini- tions of a root set Actions, that contains all actions
- A set of action properties P , which is a set of functions, mapping from an action to either an object or an interval
- A set of action instances Σ that make up the story
- A set of Impulse sentences Ψ that encode additional information about the story
