Syntactic Completeness of Proper Display Calculi

DOI10.1145/3529255zbMath1505.03121arXiv2102.11641OpenAlexW3130894656MaRDI QIDQ5056369

Alessandra Palmigiano, Giuseppe Greco, Jinsheng Chen, Apostolos Tzimoulis

Publication date: 8 December 2022

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2102.11641

zbMATH Keywords

lattice expansionsunified correspondenceproper display calculiproperly displayable logicsanalytic inductive inequalities

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items

Linear Logic Properly Displayed, Non-normal modal logics and conditional logics: semantic analysis and proof theory, Labelled calculi for lattice-based modal logics

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algebraic proof theory for substructural logics: cut-elimination and completions
• Algorithmic correspondence and canonicity for distributive modal logic
• Algorithmic correspondence for intuitionistic modal mu-calculus
• A Sahlqvist theorem for distributive modal logic
• Proof analysis in modal logic
• Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• Lattice logic properly displayed
• Multi-type display calculus for semi De Morgan logic
• Displaying modal logic
• Sequent calculus proof theory of intuitionistic apartness and order relations
• Display logic
• Focussing and proof construction
• Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics. I
• Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics. II
• Semi De Morgan logic properly displayed
• Bounded sequent calculi for non-classical logics via hypersequents
• Algorithmic correspondence and canonicity for non-distributive logics
• Logics for rough concept analysis
• Non normal logics: semantic analysis and proof theory
• Bilattice logic properly displayed
• Proper multi-type display calculi for rough algebras
• A Multi-type Calculus for Inquisitive Logic
• Multi-type display calculus for dynamic epistemic logic
• Multi-type display calculus for propositional dynamic logic
• Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications
• Logic Programming with Focusing Proofs in Linear Logic
• Cut Elimination in the Presence of Axioms
• THE LOGIC OF RESOURCES AND CAPABILITIES
• Unified correspondence as a proof-theoretic tool
• Slanted Canonicity of Analytic Inductive Inequalities
• Unified Correspondence
• From Frame Properties to Hypersequent Rules in Modal Logics
• Power and Limits of Structural Display Rules
• Minimal predicates, fixed-points, and definability