A Unified Gentzen-style Framework for Until-free LTL

TL;DR

This paper introduces a unified Gentzen-style framework for until-free propositional linear-time temporal logic, providing a consistent proof system with cut-elimination and normalization, advancing formal reasoning methods in temporal logic.

Contribution

It presents a novel unified proof-theoretic framework for until-free LTL, combining sequent calculus and natural deduction with infinitary rules.

Findings

Established equivalence between sequent calculus and natural deduction systems

Proved cut-elimination and normalization theorems for the framework

Unified approach simplifies reasoning in until-free LTL

Abstract

A unified Gentzen-style framework for until-free propositional linear-time temporal logic is introduced. The proposed framework, based on infinitary rules and rules for primitive negation, can handle uniformly both a single-succedent sequent calculus and a natural deduction system. Furthermore, an equivalence between these systems, alongside with proofs of cut-elimination and normalization theorems, is established.