Focused Proof-search in the Logic of Bunched Implications

TL;DR

This paper introduces a focused proof-search method for the logic of Bunched Implications (BI), reformulating its proof calculus with nested sequents and establishing its soundness and completeness through cut-elimination, thus enabling goal-directed proof search.

Contribution

It develops a focused proof-search framework for BI by reformulating its sequent calculus with nested sequents and proving its soundness and completeness.

Findings

Focused proof-search is complete for BI.

Nested sequents simplify the proof calculus.

Soundness and completeness are proven via cut-elimination.

Abstract

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.