Power and Limits of Structural Display Rules
From MaRDI portal
Publication:5277918
DOI10.1145/2874775zbMath1407.03067OpenAlexW2281452765MaRDI QIDQ5277918
Agata Ciabattoni, Revantha Ramanayake
Publication date: 12 July 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2874775
Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Temporal logic (03B44) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items
Linear Logic Properly Displayed, Logicality, double-line rules, and modalities, Syntactic Completeness of Proper Display Calculi, THE LOGIC OF RESOURCES AND CAPABILITIES, Disentangling structural connectives or life without display property, Intermediate logics admitting a structural hypersequent calculus, Semi De Morgan logic properly displayed, Algebraic proof theory: hypersequents and hypercompletions, Bilattice logic properly displayed
Cites Work
- 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
- Proof analysis in modal logic
- Proof methods for modal and intuitionistic logics
- Displaying and deciding substructural logics. I: Logics with contraposition
- On logics with coimplication
- Cut-free sequent calculi for some tense logics
- Constructive canonicity in non-classical logics
- Displaying modal logic
- Display logic
- Bunched logics displayed
- Hypersequent and display calculi -- a unified perspective
- Cancellative residuated lattices
- A note on the substructural hierarchy
- Structural Extensions of Display Calculi: A General Recipe
- Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5
- On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics
- Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications
- Constructive negation, implication, and co-implication
- Expanding the Realm of Systematic Proof Theory
- A constructive analysis of RM
- Logic Programming with Focusing Proofs in Linear Logic
- Gaggles, Gentzen and Galois: how to display your favourite substructural logic
- Substructural logics on display
- Theoremhood-preserving Maps Characterizing Cut Elimination for Modal Provability Logics
- Embedding the hypersequent calculus in the display calculus
- From Frame Properties to Hypersequent Rules in Modal Logics
- A system of interaction and structure
