Algebraic proof theory for substructural logics: cut-elimination and completions
From MaRDI portal
Publication:409322
DOI10.1016/J.APAL.2011.09.003zbMATH Open1245.03026OpenAlexW2169981414MaRDI QIDQ409322FDOQ409322
Authors: Agata Ciabattoni, Nikolaos Galatos, Kazushige Terui 
Publication date: 13 April 2012
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.apal.2011.09.003
Recommendations
substructural logiccut eliminationresiduated latticeMacNeille completionGentzen systemalgebraic proof theorystrucural rulesubstructural hierarchy
Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Cut-elimination and normal-form theorems (03F05) Other algebras related to logic (03G25)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Boolean Algebras with Operators. Part I
- Boolean Algebras with Operators
- Residuated frames with applications to decidability
- MacNeille completions of FL-algebras
- Zur Kennzeichnung der Dedekind-MacNeilleschen Hülle einer geordneten Menge
- Residuated lattices. An algebraic glimpse at substructural logics
- Adding involution to residuated structures
- The finite model property for various fragments of intuitionistic linear logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Canonicity results of substructural and lattice-based logics
- Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
- Correspondences between gentzen and hilbert systems
- Partially Ordered Sets
- Logic Programming with Focusing Proofs in Linear Logic
- Towards a semantic characterization of cut-elimination
- Cut elimination and strong separation for substructural logics: an algebraic approach
- Title not available (Why is that?)
- Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
- Algorithmic correspondence and canonicity for distributive modal logic
- Extending intuitionistic linear logic with knotted structural rules
- Hypersequents, logical consequence and intermediate logics for concurrency
- Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
- A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
- Algebraic aspects of cut elimination
- MacNeille completions of lattice expansions
- Minimal varieties of residuated lattices
- Kripke Semantics for Basic Sequent Systems
- Ein System des Verknüpfenden Schliessens
- Title not available (Why is that?)
- Expanding the Realm of Systematic Proof Theory
- Title not available (Why is that?)
- Specially ordered groups
- Which structural rules admit cut elimination? An algebraic criterion
- MacNeille completions and canonical extensions
- On the completion by cuts of distributive lattices
Cited In (50)
- Canonical formulas for \(k\)-potent commutative, integral, residuated lattices
- Intermediate logics admitting a structural hypersequent calculus
- Title not available (Why is that?)
- Integrally closed residuated lattices
- Focused proof-search in the logic of bunched implications
- Skolemization and Herbrand theorems for lattice-valued logics
- MOST SIMPLE EXTENSIONS OF ARE UNDECIDABLE
- Which structural rules admit cut elimination? An algebraic criterion
- Extensions of Lambek Calculi
- Densification of FL chains via residuated frames
- Syntactic Completeness of Proper Display Calculi
- Density revisited
- Join-completions of partially ordered algebras
- Poset products as relational models
- Higher-Order Categorical Substructural Logic: Expanding the Horizon of Tripos Theory
- Disjunction property and complexity of substructural logics
- MacNeille completions of FL-algebras
- Algebraic proof theory: hypersequents and hypercompletions
- FIBRED ALGEBRAIC SEMANTICS FOR A VARIETY OF NON-CLASSICAL FIRST-ORDER LOGICS AND TOPOLOGICAL LOGICAL TRANSLATION
- MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics
- Proof theory for lattice-ordered groups
- Conuclear images of substructural logics
- Judgement aggregation in non-classical logics
- Jankov Formulas and Axiomatization Techniques for Intermediate Logics
- The distributivity on bi-approximation semantics
- The logic of pseudo-uninorms and their residua
- Taming paraconsistent (and other) logics: an algorithmic approach
- Universal proof theory: semi-analytic rules and Craig interpolation
- Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
- Uniform proofs of standard completeness for extensions of first-order MTL
- Specifying proof systems in linear logic with subexponentials
- Semantical approach to cut elimination and subformula property in modal logic
- Modal translation of substructural logics
- Power and limits of structural display rules
- Finite embeddability property for residuated lattices via regular languages
- Hypersequent rules with restricted contexts for propositional modal logics
- Hyper-MacNeille completions of Heyting algebras
- Residuated structures and orthomodular lattices
- An algebraic approach to the disjunction property of substructural logics
- Tools for the investigation of substructural and paraconsistent logics
- The bounded proof property via step algebras and step frames
- Algebraic proof theory for LE-logics
- Expanding the Realm of Systematic Proof Theory
- THE LOGIC OF RESOURCES AND CAPABILITIES
- A note on the substructural hierarchy
- Distributive residuated frames and generalized bunched implication algebras
- Finite-valued semantics for canonical labelled calculi
- FULL LAMBEK CALCULUS WITH CONTRACTION IS UNDECIDABLE
- Topological duality and algebraic completions
- Cut elimination and strong separation for substructural logics: an algebraic approach
Uses Software
This page was built for publication: Algebraic proof theory for substructural logics: cut-elimination and completions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q409322)
