Cut-elimination and proof search for bi-intuitionistic tense logic

MaRDI QIDQ2904053zbMATH OpenFDO

Authors Rajeev Goré, Linda Postniece, Alwen Tiu

Publication date 5 August 2012

zbMATH Keywords

cut eliminationbi-intuitionistic logicintuitionistic modal logicdeep inferenceintuitionistic tense logic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Recommendations

• Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents
• Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents
• Deep Inference in Bi-intuitionistic Logic
• Taming displayed tense logics using nested sequents with deep inference
• A Cut-Free Sequent Calculus for Bi-intuitionistic Logic

Cited in

(21)

• Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents
• scientific article; zbMATH DE number 1341474 (Why is no real title available?)
• Prawitz, Proofs, and Meaning
• A more general general proof theory
• A bi-intuitionistic modal logic: foundations and automation
• Terminating calculi and countermodels for constructive modal logics
• Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents
• Bi-classical connexive logic and its modal extension: cut-elimination, completeness and duality
• Consistency, completeness, and classicality
• Taming displayed tense logics using nested sequents with deep inference
• On the Blok-Esakia theorem
• Deep Inference in Bi-intuitionistic Logic
• MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
• Analytic cut and Mints' symmetric interpolation method for bi-intuitionistic tense logic
• On Synonymy in Proof-Theoretic Semantics: The Case of \(\mathtt{2Int}\)
• Algorithmic correspondence for intuitionistic modal mu-calculus
• Modal interpolation via nested sequents
• Hennessy-Milner properties via topological compactness
• Reprint of: ``A more general general proof theory
• Tableau Development for a Bi-intuitionistic Tense Logic
• A proof-theoretic approach to negative translations in intuitionistic tense logics

This page was built for publication: Cut-elimination and proof search for bi-intuitionistic tense logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2904053)