Proofs for temporal logics: focus on the multi-agent case

International audienceIn this work we present and discuss some features of proofs in the case of temporal logics. More precisely, we discuss the relation between proofs for temporal logics built in two distinct frameworks: sequent calculi and tableau based calculi, taking as a typical example of temporal logic propositional LTL (Linear Temporal Logic). This work is a survey focussing on the comparison between sequent calculi and tableaux proofs. We also illustrate with some details the tableau based proofs for ATL ⇤ (the most expressive logic of the family of Alternating-Time Temporal Logics) proposed by Amélie David in 2015. Such a logic takes into account the presence of several agents that can cooperate (or not) in a given scenario to achieve some temporal objectives. Up to our knowledge, no proof-system in the sequent style is known for ATL ⇤