A single proof-theoretic framework that treats a Gentzen-style single-succedent sequent calculus and a Gentzen-style natural deduction system for the until-free fragment of propositional linear-time temporal logic uniformly. Using infinitary rules and rules for primitive negation - as modified extensions of Gentzen's LJ and NJ - it establishes an equivalence between the two systems and proves cut-elimination and normalization, with cut elimination for the sequent calculus implying normalization for natural deduction.
This NCL'24 proceedings paper introduces a unified Gentzen-style proof-theoretic framework for the until-free fragment of propositional linear-time temporal logic (LTL). Built on infinitary inference…