key: cord-0060360-068ov2bl
authors: Gheorghiu, Alexander; Marin, Sonia
title: Focused Proof-search in the Logic of Bunched Implications
date: 2021-03-23
journal: Foundations of Software Science and Computation Structures
DOI: 10.1007/978-3-030-71995-1_13
sha: 3cca5fde2d57b03175b53d8418ec334bf3745bb9
doc_id: 60360
cord_uid: 068ov2bl

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.

The Logic of Bunched Implications (BI) [31] is well-known for its applications in systems modelling [32] , especially a particular theory (of a variant of BI) called Separation Logic [37, 23] which has found industrial use in program verification. In this work, we study an aspect of proof search in BI, relying on its well-developed and well-studied proof theory [33] . We show that a goal-directed proof-search procedure known as focused proof-search is complete; that is, if there is a proof then there is a focused one. Focused proofs are both interesting in the abstract, giving insight into the proof theory of the logic, and have (for other logics) been a useful modelling technology in applied settings. For example, focused proof-search forms an operational semantics of the DPLL SAT-solvers [14] , logic programming [29, 1, 13, 7] , automated theorem provers [28] , and has been successful in providing a meta-theoretic framework in intuitionistic, substructural, and modal logics [27, 30, 25] .

Syntactically BI combines additive and multiplicative connectives, but unlike related logics such as Linear Logic (LL) [22] , BI takes all the connectives as primitive. Indeed, it arose from a proof-theoretic investigation on the relationship between conjunction and implication. As a result, sequents in BI have a more complicated structure: each implication comes with an associated contextformer. Therefore, in BI contexts are not lists, nor multisets, but instead are bunches: binary trees whose leaves are formulas and internal nodes contextformers. Additive composition (Γ ; ∆) admits the structural rules of weakening and contraction, whereas multiplicative composition (Γ, ∆) denies them. The principal technical challenges when studying proof-search in BI arise from the interaction between the additive and multiplicative fragments. We overcome these challenges by restricting the application of structural rules in the sequent calculus LBI as well as working with a representation of bunches as nested multisets.

Throughout we use the term sequent calculus in a strict sense; that is, meaning a label-free internal sequent calculus, formed in the case of BI by a context (a bunch) and a consequent (a formula). The term proof-search is consistently understood to be read as backward reduction within such a system. Although there is an extensive body of research on systems and procedures for semanticsbased calculi in BI [19, 20, 16, 17, 18] , there has been comparatively little formal study on proof-search in the strict sense. One exception is the completeness result for (unit-simple) uniform proofs [2] which is partially subsumed by the results herein.

The focusing principle was introduced for Linear Logic [1] and is characterised by alternating focused and unfocused phases of goal-directed proof-search. The unfocused phase comprises rules which are safe to apply (i.e. rules where provability is invariant); conversely, the focused phase contains the reduction of a formula and its sub-formulas where potentially invalid sequents may arise, and backtracking may be required. During focused proof-search the unfocused phases are performed eagerly, followed by controlled goal-directed focused phases, until safe reductions are available again. We say that the focusing principle holds when every provable sequent has a focused proof. This alternation can be enforced by a mechanism based on a partition of the set of formulas into two classes, positive and negative, which correspond to safe behaviour on the left and right respectively; that is, for negative formulas provability is invariant with respect to the application of a right rule, and for positive formulas, of a left rule, but in the other cases the application may result in invalid sequents.

The original proof of the focusing principle in Linear Logic was via long and tedious permutations of rules [1] . In this paper, we use for BI a different methodology, originally presented in [24] , which has since been implemented in a variety of logics [25, 5, 6] and proof systems [13] . The method is as follows: given a sequent calculus, first one polarises the syntax according to the positive/negative behaviours; second, one gives a focused variation of the sequent calculus where the control flow of proof-search is managed by polarisation; third, one shows that this system admits cut (the only non-analytic rule); and, finally, one shows that in the presence of cut the original sequent calculus may be simulated in the focused one. When the polarised system is complete, the focusing principle holds.

In LBI certain rules (the structural rules) have no natural placement in either the focused or the unfocused phases of proof-search. Thus, a design choice must be made: to eliminate/constrain these rules, or to permit them without restriction. The first gives a stricter control proof-search regime, but the latter typically achieves a more well-behaved proof theoretic meta-theory. In this paper, we choose the former as our motivation is to study computational behaviour of proof-search in BI, the latter being recovered by familiar admissibility results. The only case where confinement is not possible is the exchange rule. In standard sequent calculi the exchange rule is made implicit by working with a more convenient data-structure such as multisets as opposed to lists; however, the specific structure of bunches in BI means that a more complex alternative is required. The solution presented is to use nested multisets of two types (additive and multiplicative) corresponding to the two different context-formers/conjunctions.

In Section 2 we present the logic of Bunched Implications; in particular, Section 2.1 and Section 2.2 contain the background on BI (the syntax and sequent calculus respectfully); meanwhile, Section 2.3 gives representation of bunches as nested multisets. Section 3 contains the focused system: first, in Section 3.1 we introduce the polarised syntax; second, in Section 3.2 we introduce the focused sequents calculus and some metatheory, most importantly the cut-admissibility result; finally, in Section 3.3 we give the completeness theorem, from which the validity of the focusing principle follows as a corollary. We conclude in Section 4 with some further discussion and future directions.

2 Re-presentations of BI

The logic BI has a well-studied metatheory admitting familiar categorical, algebraic, and truth-functional semantics which have the expected dualities [34, 17, 33, 11, 32] . In practice, it is the free combination (or, more precisely, the fibration [15, 33] ) of intuitionistic logic (IL) and the multiplicative fragment of intuitionistic linear logic (MILL), which imposes the presence of two distinct context-formers in its sequent presentation. That is to say, the two conjunctions ∧ and * are represented at the meta-level by context-formers ; and , in place of the usual commas for IL and MILL respectively. Definition 1 (Formula). Let P be a denumerable set of propositional letters. The formulas of BI, denoted by small Greek letters (ϕ, ψ, χ, . . .), are defined by the following grammar, where A ∈ P,

If • ∈ {∧, ∨, →, } then it is an additive connective and if • ∈ { * , − * , * } then it is a multiplicative connective. The set of all formulas is denoted F.

A bunch is constructed from the following grammar, where ϕ ∈ F, ∆ :

The symbols ∅ + and ∅ × are the additive and multiplicative units respectively, and the symbols ; and , are the additive and multiplicative context-formers respectively. A bunch is basic if it is a formula, ∅ + , or ∅ × and complex otherwise. The set of all bunches is denoted B, the set of complex bunches with additive root context-former by B + , and the set of complex bunches with multiplicative root context-former by B × .

For two bunches ∆, ∆ ∈ B if ∆ is a sub-tree of ∆, it is called a sub-bunch. We may use the standard notation ∆(∆ ) (despite its slight inpracticality) to denote that ∆ is a sub-bunch of ∆, in which case ∆(∆ ) is the result of replacing the occurrence of ∆ by ∆ . If δ is a sub-bunch of ∆, then the context-former • is said to be its principal context-former in ∆(∆ • δ) (and ∆(δ • ∆ )).

Example 3. Let ϕ, ψ and χ be formulas, and let ∆ = (ϕ, (χ; ∅ + )); (ψ; (ψ; ∅ × )). The bunch may be written for example as ∆(ϕ, (χ; ∅ + )) which means that we can have ∆(ϕ; ϕ) = (ϕ; ϕ); (ψ; (ψ; ∅ × )).

A bunched sequent is a pair of a bunch ∆, called the context, and a formula ϕ, denoted ∆ ⇒ ϕ.

Bunches are intended to be considered up-to coherent equivalence (≡). It is the least relation satisfying:

-Commutative monoid equations for ; with unit ∅ + , -Commutative monoid equations for , with unit ∅ × ,

It will be useful to have a measure on sub-bunches which can identify their distance from the root node.

Definition 5 (Rank). If ∆ is a sub-bunch of ∆, then ρ(∆ ) is the number of alternations of additive and multiplicative context-formers between the principal context-former of ∆ , and the root context-former of ∆.

Let ∆ be a complex bunch, we use ∆ ∈ ∆ to denote that ∆ is a (proper) top-most sub-bunch; that is, ∆ is a sub-bunch satisfying ∆ = ∆ but ρ(∆ ) = 0.

Example 6. Let ∆ be as in Example 3, then ρ(∅ + ) = 2 whereas ρ(∅ × ) = 0; hence, ψ, ∅ × and (ϕ, (χ, ∅ × )) ∈ ∆. Consider the parse-tree of ∆:

Reading upward from ∅ + one encounters first ; which changes into , and then back to ; so the rank is 2; whereas counting up from ∅ × one only encounters ; so the rank is 0. 

The proof theory of BI is well-developed including familiar Hilbert, natural deduction, sequent calculi, tableaux systems, and display calculi [33, 17, 3] . In the foregoing we restrict attention to the sequent calculus as it more amenable to studying proof-search as computation, having local correctness while enjoying the completeness of analytic proofs.

Definition 7 (System LBI). The bunched sequent calculus LBI is composed of the rules in Figure 1 .

The classification of ∧ as additive may seem dubious upon reading the ∧ R rule, but the designation arises from the use of the structural rules; that is, the ∧ R and → R rules may be replaced by additive variants without loss of generality. The presentation in Figure 1 is as in [33] and simply highlights the nature of the additive and multiplicative context-formers. Nonetheless, the choice of rule does affect proof-search behaviours, and the consequences are discussed in more detailed in Section 3.1.

If ϕ has a LBI-proof, then it has a cut-free LBIproof, i.e., a proof with no occurence of the cut rule.

Throughout, unless specified otherwise, we take proof to mean cut-free proof. Moreover, if L is a sequent calculus we use L ∆ ⇒ ϕ to denote that there is an L-proof of ∆ ⇒ ϕ. Further, if R is a rule, then we may denote L + R to denote the sequent calculus combining the rules of L with R.

The following result, that a generalised version of the axiom is derivable in LBI, will allow for such sequents to be used in proof-construction later on. Lemma 9. For any formula ϕ, LBI ϕ ⇒ ϕ.

Proof. Follows from induction on size of ϕ.

The remainder of this section is the meta-theory required to control the structural rules, which pose the main issue to the study of proof-search in BI.

Lemma 10. The following rules are derivable in LBI, and replacing W with them does not affect the completeness of the system.

We can construct in LBI derivations with the same premisses and conclusion as these rules by use of the structural rules. Let LBI be LBI without W but with these new rules (retaining also * R , − * L , * R , R , and Ax), then W is admissible in LBI using standard permutation argument.

One may regard the above modification to LBI as forming a new calculus, but since all the new rules are derivable it is really a restriction of the calculus, in the sense that all proofs in the new system have equivalent proofs in LBI differing only by explicitly including instances of weakening.

Originally, sequents in the calculi for classical and intuitionistic logics (LK and LJ, respectively) were introduced as lists, and a formal exchange rule was required to permute elements when needed for a logical rule to be applied [21] . However, in practice, the exchange rule is often suppressed, and contexts are simply presented as multisets of formulas. This reduces the number of steps/choices being made during proof-search without increasing the complexity of the underlying data structure. Bunches have considerably more structure than lists, but a quotient with respect to coherent equivalence can be made resulting in two-sorted nested multisets; this was first suggested in [12] , though never formally realised.

Definition 11 (Two-sorted Nest). Nests (Γ ) are formulas or multisets, ascribed either additive (Σ), or multiplicative (Π) kind, containing nests of the opposite kind:

The constructors are multiset constructors which may be empty in which case the nests are denoted ∅ + and ∅ × respectively. No multiset is a singleton; and the set of all nests is denoted B/≡.

Given nests Λ and Γ , we write Λ ∈ Γ to denote either that Λ = Γ , if Γ is a formula, or that Λ is an element of the multiset Γ otherwise. Furthermore, we write Λ ⊆ Γ to denote ∀γ ∈ B/≡ if γ ∈ Λ then γ ∈ Γ . We will depart from the standard, yet impractical subbunch notation, and adopt a context notation for nests instead. We write Γ {·} + (resp. Γ {·} × ) for a nest with a hole within one of its additive (resp. multiplicative) multisets.The notation Γ {Λ} + (resp. Γ {Λ} × ), denotes that Λ is a sub-nest of Γ of additive (resp. multiplicative) kind; we may use Γ {Λ} when the kind is not specified. In either case Γ {Λ } denotes the substitution of Λ for Λ . A promotion in the syntax tree may be required after a substitution either to handle a singleton or an improper alternation of constructor types.

Example 12. The following inclusions are valid,

Note the absence of the {·} + constructor after substitution, this is due to a promotion in the syntax tree to avoid having two nested additive constructors. Similarly, since ∅ × denotes the empty multiset of multiplicative kind, substituting χ with it gives {ϕ, ψ , ψ , ∅ × } + ; that is, first the improper {ϕ, ∅ × } × becomes {ϕ} × ; then, the resulting singleton {ϕ} × is promoted to ϕ.

Typically we will only be interested in fragments of sub-nests so we have the following abuse of notation, where • ∈ {+, ×}:

The notion of rank has a natural analogue in this setting.

Definition 13 (Depth, Rank). Let • ∈ {+ , ×} be a nest, we define the depth on B as follows:

The equivalence of the two presentations, bunches and nests, follows from a moral (in the sense that bunches are intended to be considered modulo congruence) inverse between a nestifying function η and a bunching function β. The transformation β is simply going from a tree with arbitrary branching to a binary one, and η is the reverse.

Definition 14 (Canonical Translation). The canonical translation η : B → B/≡ is defined recursively as follows,

The canonical translation β : B/≡ → B is defined recursively as follows,

Applying η to the bunch in Example 3 gives the nest in Example 12:

The translations are inverses up-to congruence; that is,

Proof. The first two statements follow by induction on the depth (either for bunches or nests), where one must take care to consider the case of a context consisting entirely of units. The third statement employs the first in the forward direction, and proceeds by induction on depth in the reverse direction.

Definition 17 (System ηLBI). The nested sequent calculus ηLBI is composed of the rules in Figure 2 , where the metavariables denote possibly empty nests.

Observe the use of metavariable Γ instead of Π (resp. Σ) as sub-contexts in Figure 2 . This allows classes of inferences such as

to be captured by a single figure. In practice it implements the abuse of notation given above:

This system is a new and very convenient presentation of LBI, not per se a development of the proof theory for the logic.

Lemma 18 (Soundness and Completeness of ηLBI). Systems LBI and ηLBI are equivalent:

Proof. Each claim follows by induction on the context, appealing to Lemma 16 to organise the data structure for the induction hypothesis, without loss of generality.

The following is a proof in ηLBI.

We expect no obvious difficulty in studying focused proof-search with bunches instead of nested multisets; the design choice is simply to reduce the complexity of the argument by pushing all uses of exchange (E) to Lemma 18, rather than tackle it at the same time as focusing itself. In particular, working without the nested system would mean working with a weaker notion of focusing since the exchange rule must then be permissible during both focused and unfocused phases of reduction.

At no point in this section will we refer to bunches, thus the variable ∆, so far reserved for elements of B, is re-appropriated as an alternative to Γ .

Polarity in the focusing principle is determined by the invariance of provability under application of a rule, that is, by the proof rules themselves. One way the distinction between positive and negative connectives is apparent is when their rule behave either synchronously or asynchronously. For example, the * R and − * L highlight the synchronous behaviour of the multiplicative connectives since the structure of the context affects the applicability of the rule. Displaying such a synchronous behaviour on the left makes − * a negative connective, while having it on the right makes * a positive connective. Another way to characterise the polarity of a connective is the study of the inveribility properties of the corresponding rules. For example, consider the inverses of the ∨ L rule,

They are derivable in LBI with cut (below -the left branch being closed using Lemma 9) and therefore admissible in LBI without cut (by Lemma 8) .

This means that provability is invariant in general upon application of ∨ L since it can always be reverted if needed, as follows

Note however that dual connectives do not necessarily have dual behaviours in terms of provability invariance, on the left and on the right. For example, consider all the possible rules for ∧, of which some qualify as positive and others as positive.

All of these rules are sound, and replacing the conjunction rules in LBI with any pair of a left and right rule will result in a sound and complete system. Indeed, the rules are inter-derivable when the structural rules are present, but otherwise they can be paired to form two sets of rules which have essentially different proof-search behaviours. That is, the rules in the top-row make ∧ negative while the bottom row make ∧ positive. Each conjunction also comes with an associated unit, that is, − for negative conjunctio and + for positive conjunction. We choose to add all of them to our system in order to have access to those different proof search behaviours at will.

Finally, the polarity of the propositional letters can be assigned arbitrarily as long as only once for each. Definition 20 (Polarised Syntax). Let P + P − be a partition of P, and let A + ∈ P + and A − ∈ P − , then the polarised formulas are defined by the following grammar, P, Q ::= L | P ∨ Q | P * Q | P ∧ + Q | + | * | ⊥ L ::

The set of positive formulas P is denoted F + ; the set of negative formulas N is denoted F − ; and the set of all polarised formulas is denoted F ± . The subclassifications L and R are left-neutral and right-neutral formulas respectfully.

The shift operators have no logical meaning; they simply mediate the exchange of polarity, and thus the shifting into a new phase of proof-search. Consequently, to reduces cases in subsequent proofs, we will consider formulas of the form ↑↓N and ↓↑P , but not ↓↑↓N , ↓↑↓↑P , etc.

Definition 21 (Depolarisation). Let • ∈ {∨ , * , → , − * }, and let A + ∈ P + and A − ∈ P − , then the depolarisation function · : F ± → F is defined as follows:

Since proof-search is controlled by polarity, the construction of sequents in the focused system must be handled carefully to avoid ambiguity.

Positive and neutral nests, denoted by Γ and − → Γ resp., are defined according to the following grammars

A pair of a polarised nest and a polarised formula is a polarised sequent if it falls into one of the following cases

The decoration ϕ indicates that the formula is in focus; that is, it is a positive formula on the right, or a negative formula on the left. Of the three possible cases for well-formed polarised sequents, the first may be called unfocused, with the particular case of being neutral when of the form − → Γ ⇒ R; and the latter two may be called focused.

Definition 23 (Depolarised Nest). The depolarisation map extends to polarised nests · : B/≡ ± → B/≡ as follows:

We may now give the focused system. That is, the operational semantics for focused proof-search in LBI. All the rules, with the exception of P and N, are polarised versions of the rules from ηLBI.

Definition 24 (System fBI). The focused system fBI is composed of the rules on Figure 3 .

Note the absence of a cut-rule, this is because the above system is intended to encapsulate precisely focused proof-search. Below we show that a cut-rule is indeed admissible, but proofs in fBI + cut are not necessarily focused themselves. Here the distinction between the methodologies for establishing the focusing principle becomes present since one may show completeness without leaving fBI by a permutation argument instead of a cut-elimination one.

The P and N rules will allow us to move a formula from one side to another during the proof of the completeness of fBI + cut (Lemma 34).The depolarised version are not directly present in LBI, but are derivable in LBI (Lemma 9). However, the way they are focused renders them not provable in fBI because it forces one to begin with a potentially bad choice; for example, A ∨ B ⇒ A ∨ B has no proof beginning with ∨ R . In practice, they are a feature rather than a bug since they allow one to terminate proof-search early, without unnecessary further expansion of the axiom. In related works, such as [6, 5] , the analogous rules are eliminated by initially working with a weaker notion of focused proofsearch, and it is reasonable to suppose that the same may be true for BI. We leave this to future investigation.

Note also that, although it is perhaps proof-theoretically displeasing to incorporate weakening into the operational rules as in − * L and * R , it has good computational behaviour during focused proof-search since the reduction of ϕ − * ψ can only arise out of an explicit choice made earlier in the computation.

Soundness follows immediately from the depolarisation map; that is, the interpretation of polarised sequents as nested sequents, and hence proofs in fBI actually are focused proofs in ηLBI.

Theorem 25 (Soundness of fBI). Let Γ be a polarised nest and N a negative formula. If fBI Γ ⇒ N then ηLBI Γ ⇒ N Proof. Every rule in fBI except the shift rules, as well as the P and N axioms, become a rule in ηBI when the antecedent(s) and consequent are depolarised. Instance of the shift rule can be ignored since the depolarised versions of the consequent and antecedents are the same. Finally, the depolarised versions of P and N follow from Lemma 9 with the use of some weakening.

Example 26. Consider the following proof in fBI, we suppose here that propositional letters A and C are negative, but B is positive.

It is a focused version of the proof given in Example 19. Observe that the only non-deterministic choices are which formula to focus on, such as in steps (1) and (2) , where different choices have been made for the sake of demonstration. The point of focusing is that only at such points do choices that affect termination occur. The assignment of polarity to the propositional letters is what forced the shape of the proof; for example, if B had been negative the above would not have been well-formed. This phenomenon is standarly observed in focused systems (e.g. [7] ).

We now introduce the tool which will allow us to show that if there is a proof of a sequent (a priori unstructured), then there is necessarily a focused one.

Definition 27. All instances of the following rule where the sequents are wellformed are instances of cut, where − → ϕ denotes that ϕ is possibly prenexed with

Admissibility follows from the usual argument, but within the focused system; that is, through the upward permutation of cuts until they are eliminated in the axioms or are reduced in some other measure.

Let D be a fBI + cut proof, a cut is a quadruple L, R, C, ϕ where L and R are the premises to a cut rule, concluding C in D, and ϕ is the cut-formula. They are classified as follows:

Good -If ϕ is principal in both L and R.

Bad -If ϕ is not principal in one of L and R. Type 1: If ϕ is not principal in L. Type 2: If ϕ is not principal in R.

Definition 29 (Cut Ordering). The cut-rank of a cut L, R, C, ϕ in a proof is the triple cut-complexity, cut-duplicity, cut-level , where the cut-complexity is the size of ϕ, the cut-duplicity is the number of contraction instances above the cut, the cut-level is the sum of the heights of the sub-proofs concluding L and R. Let D and D be two fBI + cut proofs, let σ and σ denote their multiset of cuts respectively. Proofs are ordered by D ≺ D ⇐⇒ σ < σ , where < is the multiset ordering derived from the lexicographic ordering on cut-rank.

It follows from a result in [10] that the ordering on proofs is a well-order, since the ordering on cuts is a well-order.

Lemma 30 (Good Cuts Elimination). Let D be a fBI + cut proof of S; there is a fBI + cut proof D of S containing no good cuts such that D D.

Proof. Let D be as in hypothesis, if it contains no good cuts then D = D gives the desired proof. Otherwise, there is at least one good cut L, R, C, ϕ . Let ∂ be the sub-proof in D concluding C, then there is a transformation ∂ → ∂ where ∂ is a fBI + cut proof of S with ∂ ≺ ∂ such that the multiset of good cuts in ∂ is smaller (with respect to ≺) than the multiset of good cuts in ∂. Since ≺ is a well-order indefinitely replacing ∂ with ∂ in D for various cuts yields the desired D .

The key step is that a cut of a certain cut-complexity is replaced by cuts of lower cut-complexity, possibly increasing the cut-duplicity or cut-level of other cuts in the proof, but not modifying their complexity.

We denote by a double-line the fact that we do not actually use a weakening, but only the fact that it is admissible in fBI by construction (Lemma 10).

Let D be a fBI + cut proof of S that contains only one cut which is bad, then there is a fBI + cut proof D of S such that D ≺ D.

Proof. Without loss of generality suppose the cut is the last inference in the proof, then it may be replaced by other cuts whose cut-level or cut-duplicity is smaller, but with same cut-complexity.

First we consider bad cuts when L and R are both axioms. There are no Type 1 bad cuts on axioms as the formula is always principal, meanwhile the Type 2 bad cuts can trivially be permuted upwards or ignored; for example,

Here again we are using an appropriate version of Lemma 10. For the remaining cases the cuts are commutative in the sense that they may be permuted upward thereby reducing the cut-level. An example is given below.

The exceptional case is the interaction with contraction where the cut is replaced by cuts of possibly equal cut-level, but cut-duplicity decreases.

Theorem 32 (Cut-elimination in fBI). Let Γ be a positive nest and N a negative formula. Then, fBI Γ ⇒ N if and only if fBI+cut Γ ⇒ N .

Proof. (⇒) Trivial as any fBI-proof is a fBI + cut-proof. (⇐) Let D be a fBI + cut-proof of Γ ⇒ N , if it has no cuts then it is a fBI-proof so we are done. Otherwise, there is at least one cut, and we proceed by well-founded induction on the ordering of proofs and sub-proofs of D with respect to ≺. Base Case. Assume D is minimal with respect to ≺ with at least one cut; without loss of generality, by Lemma 30, assume the cut is bad. It follows from Lemma 31 that there is a proof strictly smaller in ≺-ordering, but this proof must be cut-free as D is minimal.

Inductive

Step. Let D be as in the hypothesis, then by Lemma 30 there is a proof ∂ of Γ ⇒ N containing no good cuts such that D D. Either D is cut-free and we are done, or it contains bad cuts. Consider the topmost cut, and denote the sub-proof by ∂, it follows from Lemma 31 that there is a proof ∂ of the same sequent such that ∂ ≺ ∂. Hence, by inductive hypothesis, there is a cut-free proof the sequent and replacing ∂ by this proof in D gives a proof of Γ ⇒ ϕ strictly smaller in ≺-ordering, thus by inductive hypothesis there is a cut-free proof as required.

The completeness theorem of the focused system, the operational semantics, is with respect to an interpretation (i.e. a polarisation). Indeed, any polarisation may be considered; for example, both (↓A − * B + )∧ + ↓A − and ↓(A + * ↓B − )∧ + A + are correct polarised versions of the formulas (A * B) ∧ A. Taking arbitrary ϕ the process is as follows: first, fix a polarised syntax (i.e. a partition of the propositional letters into positive and negative sets), then assign a polarity to ϕ with the following steps:

-If ϕ is a propositional atom, it must be polarised by default; -If ϕ = , then choose polarisation + or − ; -If ϕ = ψ 1 ∧ ψ 2 , first polarise ψ 1 and ψ 2 , then choose an additive conjunction and combine accordingly, using shifts to ensure the formula is well-formed;

-If ϕ = ψ 1 • ψ 2 where • ∈ { * , − * , →, ∨}, then polarise ψ 1 and ψ 2 and combine with • accordingly, using shifts where necessary.

Example 33. Suppose A is negative and B is positive, then (A * B) ∧ A may be polarised by choosing the additive conjunction to be positive resulting in (↓A * B) ∧ + ↓A (when ↓(A * ↓B) ∧ + A) would not be well-formed). Choosing to shift one can ascribe a negative polarisation ↑((↓A * B) ∧ + ↓A).

The above generates the set of all such polarised formulas when all possible choices are explored. The free assignment of polarity to formulas means several distinct focusing procedures are captured by the completeness theorem.

Lemma 34 (Completeness of fBI + cut). For any unfocused sequent Γ ⇒ N , if ηLBI Γ ⇒ N then fBI+cut Γ ⇒ N .

Proof. We show that every rule in ηLBI is derivable in fBI + cut, consequently every proof in ηLBI may be simulated; hence, every provable sequent has a focused proof. For unfocused rules → R , − * R , ∧ − R , ∧ + L , ∨ L , * L , ⊥ L , − R , + L , * L , this is immediate; as well as for Ax and C. Below we give an example on how to simulate a focused rule.

Where it does not matter (e.g. in the case of inactive nests), we do not distinguish the polarised and unpolarised versions; each of the simulations can be closed thanks to the presence of the P and N rules in fBI.

Theorem 35 (Completeness of fBI). For any unfocused Γ ⇒ N , if ηLBI Γ ⇒ N then fBI Γ ⇒ N .

Proof. It follows from Lemma 34 that there is a proof of Γ ⇒ N in fBI + cut, and then it follows from Lemma 32 that there is a proof of Γ ⇒ N in fBI.

Given an arbitrary sequent the above theorem guarantees the existence of a focused proof, thus the focusing principle holds for ηLBI and therefore for LBI.

By proving the completeness of a focused sequent calculus for the logic of Bunched Implications, we have demonstrated that it satisfies the focusing principle; that is, any polarisation of a BI-provable sequent can be proved following a focused search procedure. This required a careful analysis of how to restrict the usage of structural rules. In particular, we had to fully develop the congruenceinvariant representation of bunches as nested multisets (originally proposed in [12] ) to treat the exchange rule within bunched structures.

Proof-theoretically the completeness of the focused systems suggests a syntactic orderliness of LBI, though the P and N rules leave something to be desired. Computationally, these axioms are unproblematic as during search it makes sense to terminate a branch as soon as possible; however, unless they may be eliminated it means that the focusing principle holds in BI only up to a point. In related works (c.f. [6] ) the analogous problem is overcome by first considering a weak focused system; that is, one where the structural rules are not controlled and unfocused rules may be performed inside focused phases if desired. Completeness of (strong) focusing is achieved by appealing to a synthetic system. It seems reasonable to suppose the same can be done for BI, resulting in a more proof-theoretically satisfactory focused calculus, exploring this possibility is a natural extension of the work on fBI.

The methodology employed for proving the focusing principle can be interpreted as soundness and completeness of an operational semantics for goaldirected search. The robustness of this technique is demonstrated by its efficacy in modal [6, 5] and substructural logics [26] , including now bunched ones. Although BI may be the most employed bunched logic, there are a number of others, such as the family of relevant logics [36] , and the family of bunched logics [11] , for which the focusing principle should be studied. However, without the presence of a cut-free sequent calculus goal-directed search becomes unclear, and currently such calculi do not exist for the two main variants of BI: Boolean BI [33] and Classical BI [4] . On the other hand, large families of bunched and substructural logics have been given hypersequent calculi [8, 9] . Effective proof-search procedures have been established for the hypersequent calculi in the substructural case [35] , but not the bunched one, and focused proof-search for neither. There is a technical challenge in focusing these systems as one must not only decide which formula to reduce, but also which sequent.

In the future it will be especially interesting to see how focused search, when combined with the expressiveness of BI, increases its modelling capabilities. Indeed, the dynamics of proof-search can be used to represent models of computation within (propositional) logics; for example, the undecidability of Linear Logic involves simulating two-counter machines [26] . One particularly interesting direction is to see how focused proof-search in BI may prove valuable within the context of Separation Logic. Focused systems in particular have been used to emulate proofs for other logics [27] ; and to give structural operational semantics for systems used in industry, such as algorithms for solving constraint satisfaction problems [14] . A more immediate possibility though is the formulation of a theorem prover; we leave providing specific implementation or benchmarks to future research.

Logic programming with focusing proofs in linear logic

Bunched Logic Programming

A unified display proof theory for bunched logic

Classical BI: Its semantics and proof theory

Focused and synthetic nested sequents

Modular focused proof systems for intuitionistic modal logics

A logical characterization of forward and backward chaining in the inverse method

Algebraic proof theory for substructural logics: Cut-elimination and completions

Bunched hypersequent calculi for distributive substructural logics

Proving termination with multiset orderings

Bunched Logics: A Uniform Approach

The inverse method for the logic of bunched implications

LJQ: A strongly focused calculus for intuitionistic logic

A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus

Oxford Logic Guides

Semantic labelled tableaux for propositional BI

The semantics of BI and resource tableaux

Relating labelled and label-free bunched calculi in BI logic

Proof-search and countermodel generation in propositional BI Logic -extended abstract

Connection-based proof search in propositional BI logic

The Collected Papers of Gerhard Gentzen

BI as an assertion language for mutable data structures

A proof of the focalization property of linear logic

Focusing and polarization in linear, intuitionistic, and classical logics

Decision problems for propositional linear logic

A focused framework for emulating modal proof systems

Imogen: Focusing the polarized focused inverse method for intuitionistic propositional logic

Uniform proofs as a foundation for logic programming

A formal framework for specifying sequent calculus proof systems

The logic of bunched implications

Resource semantics: Logic as a modelling technology

The Semantics and Proof Theory of the Logic of Bunched Implications

Possible Worlds and Resources: the Semantics of BI

Extended Kripke lemma and decidability for hypersequent substructural logics

Relevant Logic: A Philosophical Examination of Inference

Separation logic: a logic for shared mutable data structures

), 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