Despite the great relevance of temporal logics in many applications of computer science, their theoretical analysis is far from being concluded. In particular, we still lack a satisfactory proof theory for temporal logics and this is especially true in the case of branching-time logics.
In this talk, I will present a modular approach to the definition of labeled (natural) deduction systems for a large class of temporal logics. I will start with a system for the basic Priorean tense logics and show how to modularly enrich it in order to deal with richer and more complex logics, like LTL. I will also consider the extension to the branching case, focusing on the Ockhamist branching-time logics with a bundled semantics.
A detailed proof-theoretical analysis of the systems has been performed. In particular, in the case of discrete-time logics, for which rules modeling an induction principle are required, a procedure of normalization inspired to those of systems for Heyting Arithmetic has been defined.