Focused Proof-search in the Logic of Bunched Implications

The logic of Bunched Implications (BI) freely combines additive and multiplicative connectives, including implications; however, despite its well-studied proof theory, proof-search in BI has always been a difficult problem. The focusing principle is a restriction of the proof-search space that can c...

Descripción completa

Detalles Bibliográficos
Autores principales: Gheorghiu, Alexander, Marin, Sonia
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2021
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7984104/
http://dx.doi.org/10.1007/978-3-030-71995-1_13
_version_ 1783668006307495936
author Gheorghiu, Alexander
Marin, Sonia
author_facet Gheorghiu, Alexander
Marin, Sonia
author_sort Gheorghiu, Alexander
collection PubMed
description The logic of Bunched Implications (BI) freely combines additive and multiplicative connectives, including implications; however, despite its well-studied proof theory, proof-search in BI has always been a difficult problem. The focusing principle is a restriction of the proof-search space that can capture various goal-directed proof-search procedures. In this paper we show that focused proof-search is complete for BI by first reformulating the traditional bunched sequent calculus using the simpler data-structure of nested sequents, following with a polarised and focused variant that we show is sound and complete via a cut-elimination argument. This establishes an operational semantics for focused proof-search in the logic of Bunched Implications.
format Online
Article
Text
id pubmed-7984104
institution National Center for Biotechnology Information
language English
publishDate 2021
record_format MEDLINE/PubMed
spelling pubmed-79841042021-03-23 Focused Proof-search in the Logic of Bunched Implications Gheorghiu, Alexander Marin, Sonia Foundations of Software Science and Computation Structures Article The logic of Bunched Implications (BI) freely combines additive and multiplicative connectives, including implications; however, despite its well-studied proof theory, proof-search in BI has always been a difficult problem. The focusing principle is a restriction of the proof-search space that can capture various goal-directed proof-search procedures. In this paper we show that focused proof-search is complete for BI by first reformulating the traditional bunched sequent calculus using the simpler data-structure of nested sequents, following with a polarised and focused variant that we show is sound and complete via a cut-elimination argument. This establishes an operational semantics for focused proof-search in the logic of Bunched Implications. 2021-03-23 /pmc/articles/PMC7984104/ http://dx.doi.org/10.1007/978-3-030-71995-1_13 Text en © The Author(s) 2021 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Gheorghiu, Alexander
Marin, Sonia
Focused Proof-search in the Logic of Bunched Implications
title Focused Proof-search in the Logic of Bunched Implications
title_full Focused Proof-search in the Logic of Bunched Implications
title_fullStr Focused Proof-search in the Logic of Bunched Implications
title_full_unstemmed Focused Proof-search in the Logic of Bunched Implications
title_short Focused Proof-search in the Logic of Bunched Implications
title_sort focused proof-search in the logic of bunched implications
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7984104/
http://dx.doi.org/10.1007/978-3-030-71995-1_13
work_keys_str_mv AT gheorghiualexander focusedproofsearchinthelogicofbunchedimplications
AT marinsonia focusedproofsearchinthelogicofbunchedimplications

Ejemplares similares