Focused proof-search in the logic of bunched implications
From MaRDI portal
Publication:2233409
DOI10.1007/978-3-030-71995-1_13OpenAlexW3139860392MaRDI QIDQ2233409
Alexander Gheorghiu, Sonia Marin
Publication date: 18 October 2021
Full work available at URL: https://arxiv.org/abs/2010.08352
Related Items
Semantical analysis of the logic of bunched implications, Explorations in Subexponential Non-associative Non-commutative Linear Logic, Non-associative, non-commutative multi-modal linear logic
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Algebraic proof theory for substructural logics: cut-elimination and completions
- Linear logic
- Focusing and polarization in linear, intuitionistic, and classical logics
- Decision problems for propositional linear logic
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- A formal framework for specifying sequent calculus proof systems
- Relating labelled and label-free bunched calculi in BI logic
- The semantics and proof theory of the logic of bunched implications
- Uniform proofs as a foundation for logic programming
- Focused and Synthetic Nested Sequents
- A Unified Display Proof Theory for Bunched Logic
- The semantics of BI and resource tableaux
- Classical BI: Its Semantics and Proof Theory
- A Logical Characterization of Forward and Backward Chaining in the Inverse Method
- Logic Programming with Focusing Proofs in Linear Logic
- The Logic of Bunched Implications
- Semantic Labelled Tableaux for Propositional BI
- Bunched Hypersequent Calculi for Distributive Substructural Logics
- Extended Kripke lemma and decidability for hypersequent substructural logics
- Modular Focused Proof Systems for Intuitionistic Modal Logics
- Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
- Logic for Programming, Artificial Intelligence, and Reasoning
- Logical Approaches to Computational Barriers
