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

zbMATH Open1254.03033MaRDI QIDQ2904053FDOQ2904053

Authors: Rajeev Goré, Linda Postniece, Alwen Tiu 

Publication date: 5 August 2012

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

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)

Cited In (21)

• Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents
• Title not available (Why is that?)
• 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)
• On Synonymy in Proof-Theoretic Semantics: The Case of \(\mathtt{2Int}\)
• Analytic cut and Mints' symmetric interpolation method for bi-intuitionistic tense logic
• Hennessy-Milner properties via topological compactness
• Algorithmic correspondence for intuitionistic modal mu-calculus
• Modal interpolation via nested sequents
• Tableau Development for a Bi-intuitionistic Tense Logic
• Reprint of: ``A more general general proof theory
• 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)