View article

We present cut-free labelled sequent calculi for a central formalism in logics of agency: STIT logics with temporal operators. These include sequent systems for , and . All calculi presented possess essential structural properties such as contraction- and cut-admissibility. The labelled calculi and are shown sound and complete relative to irreflexive temporal frames. Additionally, we extend current results by showing that also can be characterized through relational frames, omitting the use of BT+AC frames.