Sequent calculi usually provide a general deductive setting that uniformly embeds other proof-theoretical approaches, such
as tableaux methods, resolution techniques, goal-directed proofs, etc. Unfortunately, in temporal logic, existing sequent
calculi make use of a kind of inference rules that prevent the effective mechanization of temporal deduction in the general
setting. In particular, temporal sequent calculi either need some form of cut, or they make use of invariants, or they include
infinitary rules. This is the case even for the simplest kind of temporal logic, propositional linear temporal logic (
PLTL). In this paper, we provide a complete finitary sequent calculus for
PLTL, called
FC\mathcal{FC}
, that not only is cut-free but also invariant-free. In particular, we introduce new rules which provide a new style of temporal
deduction. We give a detailed proof of completeness.
This work has been partially supported by Spanish Project TIN2004-079250-C03.