A Unified Gentzen-style Framework for Until-free LTL
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.
Authors
- Norihiro Kamide (ORCID: https://orcid.org/0000-0001-7736-8055)
- Sara Negri (ORCID: https://orcid.org/0000-0003-3958-6312)
Institutions
- Nagoya City University (JP)
- University of Genoa (IT)
Publication Details
- Journal
- Electronic Proceedings in Theoretical Computer Science
- Published
- 2024-12-28
- DOI
- https://doi.org/10.4204/eptcs.415.16
- Citations
- 1
- Primary Topic
- Formal Methods in Verification
- Type
- article
- Field-Weighted Citation Impact
- 0.36
Funders
- Istituto Nazionale di Alta Matematica "Francesco Severi"
- European Commission
- Ministero dell’Istruzione, dell’Università e della Ricerca
- Norges Forskningsråd
- Cordis
- Gruppo Nazionale per le Strutture Algebriche, Geometriche e le loro Applicazioni
- Japan Society for the Promotion of Science