Focused proof-search in the logic of bunched implications

DOI10.1007/978-3-030-71995-1_13OpenAlexW3139860392MaRDI QIDQ2233409FDOQ2233409

Alexander Gheorghiu, Sonia Marin

Publication date: 18 October 2021

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

Recommendations

• The semantics and proof theory of the logic of bunched implications
• Formalised Inductive Reasoning in the Logic of Bunched Implications
• scientific article; zbMATH DE number 1390270
• scientific article; zbMATH DE number 1753197
• Logic for Programming, Artificial Intelligence, and Reasoning
• Focused proof search for linear logic in the calculus of structures
• scientific article; zbMATH DE number 1231702
• Proof search in nested sequent calculi
• scientific article; zbMATH DE number 1348467
• scientific article; zbMATH DE number 1696800

zbMATH Keywords

logicfocusingproof-searchbunched implications

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Cites Work

• Decision problems for propositional linear logic
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• The semantics and proof theory of the logic of bunched implications
• The semantics of BI and resource tableaux
• The Logic of Bunched Implications
• Semantic Labelled Tableaux for Propositional BI
• Title not available (Why is that?)
• Linear logic
• Algebraic proof theory for substructural logics: cut-elimination and completions
• Focusing and polarization in linear, intuitionistic, and classical logics
• Focused and Synthetic Nested Sequents
• Logic Programming with Focusing Proofs in Linear Logic
• Uniform proofs as a foundation for logic programming
• Title not available (Why is that?)
• Title not available (Why is that?)
• Logical Approaches to Computational Barriers
• A Logical Characterization of Forward and Backward Chaining in the Inverse Method
• A formal framework for specifying sequent calculus proof systems
• Title not available (Why is that?)
• Classical BI: Its Semantics and Proof Theory
• A Unified Display Proof Theory for Bunched Logic
• Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
• Logic for Programming, Artificial Intelligence, and Reasoning
• Modular Focused Proof Systems for Intuitionistic Modal Logics
• Title not available (Why is that?)
• Relating labelled and label-free bunched calculi in BI logic
• Bunched Hypersequent Calculi for Distributive Substructural Logics
• Title not available (Why is that?)
• Extended Kripke lemma and decidability for hypersequent substructural logics

Cited In (5)

• Formalised Inductive Reasoning in the Logic of Bunched Implications
• Semantical analysis of the logic of bunched implications
• Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
• Explorations in Subexponential Non-associative Non-commutative Linear Logic
• Non-associative, non-commutative multi-modal linear logic

This page was built for publication: Focused proof-search in the logic of bunched implications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233409)