Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Unified Gentzen-style Framework for Until-free LTL

Norihiro Kamide, Sara Negri

TL;DR

This work addresses unifying Gentzen-style sequent calculus and natural deduction for the until-free propositional LTL fragment. To this end, it develops a temporal single-succedent calculus $SLT_{omega}$ alongside the standard $LT_{omega}$, using infinitary rules and a primitive negation. Key contributions include cut-elimination for $SLT_{omega}$, a precise equivalence with $LT_{omega}$, and a natural deduction system $NLT_{omega}$ with a normalization result. The framework enables straightforward transfer of meta-theoretic results across formalisms and has potential impact for logic-based verification and formalization tasks.

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.

A Unified Gentzen-style Framework for Until-free LTL

TL;DR

This work addresses unifying Gentzen-style sequent calculus and natural deduction for the until-free propositional LTL fragment. To this end, it develops a temporal single-succedent calculus alongside the standard , using infinitary rules and a primitive negation. Key contributions include cut-elimination for , a precise equivalence with , and a natural deduction system with a normalization result. The framework enables straightforward transfer of meta-theoretic results across formalisms and has potential impact for logic-based verification and formalization tasks.

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.
Paper Structure (5 sections, 10 theorems, 22 equations)

This paper contains 5 sections, 10 theorems, 22 equations.

Table of Contents

  1. Introduction
  2. Sequent calculus and cut elimination
  3. Natural deduction
  4. Equivalence and normalization
  5. Concluding remarks and acknowledgments

Key Result

Proposition 2.5

Let $L$ be LT$_{\omega}$ or SLT$_{\omega}$. The sequents of the form $\hbox{\rm X}^i\hbox{\it $\alpha$}, \hbox{\it $\Gamma$} \Rightarrow \hbox{\rm X}^i\hbox{\it $\alpha$}$ for any formula $\hbox{\it $\alpha$}$ and any natural number $i$ are derivable in $L$.

Theorems & Definitions (21)

  • Definition 2.1
  • Definition 2.2: LT$_{\omega}$
  • Remark 2.3
  • Definition 2.4: SLT$_{\omega}$
  • Proposition 2.5
  • Proposition 2.6
  • Proposition 2.7
  • Lemma 2.8
  • Lemma 2.9
  • Theorem 2.10: Cut elimination for SLT$_{\omega}$
  • ...and 11 more