Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic

DOI10.1007/s11225-023-10052-7OpenAlexW4380624652MaRDI QIDQ6067745

Norihiro Kamide

Publication date: 17 November 2023

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11225-023-10052-7

zbMATH Keywords

completeness theoremcut-elimination theoremlinear-time temporal logicrefutation-aware Gentzen-style sequent calculusrefutation-aware Kripke-style semantics

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Bounded linear-time temporal logic: a proof-theoretic investigation
• Proof theory of Nelson's paraconsistent logic: a uniform perspective
• Dual intuitionistic logic and a variety of negations: the logic of scientific research
• Cut-free sequent systems for temporal logic
• Concerning the semantic consequence relation in first-order temporal logic
• Applications of Kripke models to Heyting-Brouwer logic
• The logic of information structures
• Refutation systems in modal logic
• Dual-intuitionistic logic
• Temporal resolution using a breadth-first search algorithm
• Decidable fragments of first-order temporal logics
• Refutations, proofs, and models in the modal logic K4
• Paraconsistent computation tree logic
• An approach to infinitary temporal proof theory
• Intuitive semantics for first-degree entailments and `coupled trees'
• A formalization of the propositional calculus of H-B logic
• Semantics-based nonmonotonic inference
• A Łukasiewicz-style refutation system for the modal logic S4
• Falsification-aware semantics and sequent calculi for classical logic
• Logics and falsifications. A new perspective on constructivist semantics
• Uniform proofs as a foundation for logic programming
• Falsification, natural deduction and bi-intuitionistic logic
• A Paraconsistent Linear-time Temporal Logic
• Relating first-order monadic omega-logic, propositional linear-time temporal logic, propositional generalized definitional reflection logic and propositional infinitary logic
• Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic
• Counterexample-guided abstraction refinement for symbolic model checking
• Nonclausal deduction in first-order temporal logic
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• Natural deduction systems for Nelson's paraconsistent logic and its neighbors
• Constructible falsity and inexact predicates
• Sequential Calculus for a First Order Infinitary Temporal Logic
• The Logic of Contradiction
• Propositional temporal logics: decidability and completeness
• Investigation of finitary calculus for a discrete linear time logic by means of infinitary calculus
• Handbook of Model Checking
• Refutations in Wansing’s Logic
• A deductive-reductive form of logic: General theory and intuitionistic case
• Monodic temporal resolution
• A Machine-Oriented Logic Based on the Resolution Principle
• Clausal temporal resolution
• Embedding theorems for LTL and its variants
• A MODAL TRANSLATION FOR DUAL-INTUITIONISTIC LOGIC
• Constructible falsity
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic