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

Didier Galmiche and Daniel Méry

LORIA - Université Henri Poincaré Campus Scientifique, BP 239, 54506 Vandœuvre-lès-Nancy, France galmiche{dmery}@loria.fr

Abstract In this paper, we study proof-search in the propositional BI logic that can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. With its underlying sharing interpretation, BI has been recently used for logic programming or reasoning about mutable data structures. We propose a labelled tableau calculus for BI, the use of labels making it possible to generate countermodels. We show that, from a given formula A, a non-redundant tableau construction procedure terminates and yields either a tableau proof of A or a countermodel of A in terms of the Kripke resource monoid semantics. Moreover, we show the finite model property for BI with respect to this semantics.

1 Introduction

The logic of bunched implications, BI, freely combines a multiplicative (or linear) and an additive (or intuitionistic) implication in the same logic [12] and its propositional fragment can be viewed as a merging of intuitionistic logic (IL) and multiplicative intuitionistic linear logic (MILL) with well-defined proof-theoretic and semantic foundations [11,13]. The semantics of BI is motivated by modelling the notion of resource. With its underlying sharing interpretation, it has been recently used for logic programming [1] or reasoning about mutable data structures [8]. Our aim is to propose useful and efficient proof-search procedures for such a mixed logic. Because of the cohabitation of linear and intuitionistic connectives in a same logic and even if BI includes IL and MILL as subsystems, we cannot directly extend proof-search (sequent, tableau, or connection) calculi defined for each of them [2,4,5,14] to BI. Moreover we aim to design a BI prover that builds proofs but also generates countermodels for non-theorems. Such systems exist for IL [5] and MILL [14] and the tableau method directly provides countermodel generation for a wide range of logics, including IL, but not for substructural logics like linear logic (LL) [9,10]. An appropriate solution consists in designing calculi with labels which make it possible to generate countermodels in terms of a given semantics. Our approach is based on the Kripke resource semantics of BI where the possible worlds are justified in terms of pieces of information [15] and also on the methodology of LDS for analytic deduction [3] that has been recently used for MILL with a simple semantics [14]. In this paper, we define a labelled tableau calculus TBI for propositional BI with constraints (assertions and obligations). The provability is related to the search of a closed tableau in which the set of obligations can be verified from the assertions, following some specific conditions. We show that, for a given formula A, there exists a nonredundant tableau construction procedure for TBI that terminates and yields either a tableau proof or a countermodel for A. We prove the completeness of the calculus for BI (without ⊥) with respect to the Kripke resource semantics and also the finite model property. From these results, we will study some algorithmic aspects of proof-search and countermodel generation with this labelled calculus using appropriate structures (dependency graphs) dedicated to constraints solving. We will define a derived calculus with free variables in labels and moreover design a similar calculus with countermodel generation in BI (with ⊥) starting from Grothendieck sheaftheoretic models [12].

2 The Logic of Bunched Implications (BI)

In this section, we remind the essential features of the propositional logic of Bunched Implications (BI) [13], in which additive (intuitionistic) and multiplicative (linear) connectives cohabit.

2.1 Syntax and Proof-Theory of BI

The propositional language of BI consists of a multiplicative unit I, the multiplicative connectives ∗, −∗, the additive units ⊤, ⊥, the additive connectives ∧, →, ∨, a countable set P = A, B, … of propositional variables. Propositions over P, referred to as P, are inductively defined as follows:

P ::= P | I | P ∗ P | P −∗P | ⊤ | P ∧ P | P → P | ⊥ | P ∨ P

The additive connectives correspond to those of intuitionistic logic (IL) and the multiplicative connectives to those of multiplicative intuitionistic linear logic (MILL). The antecedents of logical consequences are not as lists but rather as bunches, in which there are two ways to combine operations that respectively display additive and multiplicative behavior.

Definition 1 (Bunches). Bunches are inductively defined as follows:

Γ ::= P | ∅_{m} | Γ, Γ | ∅_{a} | Γ; Γ

We write Γ (Δ) to represent a bunch in which Δ is a subtree. We consider “bunches” up to a structural equivalence (≡) defined as the least equivalence on “bunches” satisfying: a) commutative monoid equations for ∅_{a} and “;”, b)

– Identity and structures

\begin{aligned}& ax \\ A ⊢ A \end{aligned} \begin{aligned}Γ ⊢ A \\ & Δ ≡ Γ \\ Δ ⊢ A \end{aligned}  \begin{aligned}Γ (Δ) ⊢ A \\ & w \\ Γ (Δ; Δ′) ⊢ A \end{aligned} \begin{aligned}Γ (Δ; Δ) ⊢ A \\ & c \\ Γ (Δ) ⊢ A \end{aligned}

– Unities

\begin{aligned}& ⊥_{L} \\ ⊥ ⊢ A \end{aligned} \begin{aligned}Γ (∅_{m}) ⊢ A \\ & I_{L} \\ Γ (I) ⊢ A \end{aligned} \begin{aligned}& I_{R} \\ ∅_{m} ⊢ I \end{aligned} \begin{aligned}Γ (∅_{a}) ⊢ A \\ & ⊤_{L} \\ Γ (⊤) ⊢ A \end{aligned} \begin{aligned}& ⊤_{R} \\ ∅_{a} ⊢ ⊤ \end{aligned}

– Multiplicatives

\begin{aligned}Γ (A, B) ⊢ C \\ & ∗_{L} \\ Γ (A ∗ B) ⊢ C \end{aligned} \begin{aligned}Γ ⊢ A & Δ ⊢ B \\ & ∗_{R} \\ Γ, Δ ⊢ A ∗ B \end{aligned} \begin{aligned}Γ ⊢ A & Δ(Δ′, B) ⊢ C \\ & −∗_{L} \\ Δ(Δ′, Γ, A −∗B) ⊢ C \end{aligned} \begin{aligned}Γ, A ⊢ B \\ & −∗_{R} \\ Γ ⊢ A −∗B \end{aligned}

– Additives

\begin{aligned}Γ (A; B) ⊢ C \\ & ∧_{L} \\ Γ (A ∧ B) ⊢ C \end{aligned} \begin{aligned}Γ ⊢ A & Δ ⊢ B \\ & ∧_{R} \\ Γ; Δ ⊢ A ∧ B \end{aligned} \begin{aligned}Γ ⊢ A & Δ(Δ′; B) ⊢ C \\ & →_{L} \\ Δ(Δ′; Γ; A → B) ⊢ C \end{aligned}

\begin{aligned}Γ; A ⊢ B \\ & →_{R} \\ Γ ⊢ A → B \end{aligned} \begin{aligned}Γ (A) ⊢ C & Δ(B) ⊢ C \\ & ∨_{L} \\ Γ (A ∨ B); Δ(A ∨ B) ⊢ C \end{aligned} \begin{aligned}Γ ⊢ A_{i (i=1,2)} \\ & ∨_{R} \\ Γ ⊢ A_{1} ∨ A_{2} \end{aligned}

Figure 1. The LBI sequent calculus

commutative monoid equations for ∅_{m} and “,” and c) congruence: Δ ≡ Δ′ implies Γ (Δ) ≡ Γ (Δ′). Let us note that “;” and “,” do not distribute over one another. The judgements are expressions of the form Γ ⊢ A, where Γ is a “bunch” and A is a proposition. The LBI sequent calculus, given in figure 1, has the cutelimination property and is equivalent to a sequent calculus with the following additive rules

\begin{aligned}& ax \\ Γ; A ⊢ A \end{aligned} \begin{aligned}Γ ⊢ A & Γ ⊢ B \\ & ∧_{R} \\ Γ ⊢ A ∧ B \end{aligned} \begin{aligned}Γ ⊢ A & Δ(Γ; B) ⊢ C \\ & →_{L} \\ Δ(Γ; A → B) ⊢ C \end{aligned} \begin{aligned}Γ (A) ⊢ C & Γ (B) ⊢ C \\ & ∨_{L} \\ Γ (A ∨ B) ⊢ C \end{aligned}

that are derivable in the LBI calculus. Let us now show that the sequent A ∗ (B ∧ C) ⊢ (A ∗ B) ∧ (A ∗ C) is provable in the additive version of LBI:

\begin{matrix}A ⊢ A & \begin{aligned}B; C ⊢ B \\ & ∧_{L} \\ B ∧ C ⊢ B \end{aligned} \\ ∗_{R} \\ A ∗ (B ∧ C) ⊢ A ∗ B \end{matrix} \begin{matrix}A ⊢ A & \begin{aligned}B; C ⊢ C \\ & ∧_{L} \\ B ∧ C ⊢ C \end{aligned} \\ ∗_{R} \\ A ∗ (B ∧ C) ⊢ A ∗ C \end{matrix}
∧_{R}
A ∗ (B ∧ C) ⊢ (A ∗ B) ∧ (A ∗ C)

A proposition A is a theorem if either ∅_{a} ⊢ A, or ∅_{m} ⊢ A is provable in LBI. Moreover we have the following results Theorem 1. Γ (∅_{a}) ⊢ A (resp. Γ (∅_{m}) ⊢ A) is provable in LBI iff Γ (⊤) ⊢ A (resp. Γ (I) ⊢ A) is provable in LBI.

Corollary 1. A proposition A is a theorem iff ∅_{m} ⊢ A is provable in LBI.

As BI contains IL and MILL as subsystems it is important to remind that BI is conservative over both logics. All these results are detailed in [12].

2.2 Kripke resource semantics

BI has two natural semantics: a categorical semantics of the proof theory (interpretation of proofs) using a doubly closed category (two monoidal closed structures) that has all the structure to model both IL and MILL and a Kripke-style semantics (interpretation of formulae) which combines the Kripke semantics of IL and Urquhart’s semantics of MILL [12]. This one uses possible worlds, arranged as a commutative monoid and justified in terms of “pieces of information” [15]. In this paper we consider the second one that provides a way to read the formulae as propositions that are true or false relative to a given world. Let us summarize the main points about this semantics that is based on the notion of resource.

Definition 2. A Kripke resource monoid (Krm) M = ⟨ M, •, e, ⊑ ⟩ is a preordered monoid in which • is order preserving, i.e., m ⊑ n and m′ ⊑ n′ implies m • m′ ⊑ n • n′. Let M = ⟨ M, •, e, ⊑ ⟩ be a Krm, a forcing on M is a binary relation ⊧ on M × P satisfying the Kripke monotonicity property, i.e., m ⊧ A and m ⊑ n implies n ⊧ A.

The relation ⊧ can be extended to the set P of propositions with the following inductive definition^{1}:

- m ⊧ ⊤  always
- m ⊧ A ∧ B iff m ⊧ A and m ⊧ B
- m ⊧ ⊥  never
- m ⊧ A ∨ B iff m ⊧ A or m ⊧ B
- m ⊧ A → B iff (∀ n ∈ M / m ⊑ n)(n ⊧ A implies n ⊧ B)
- m ⊧ I  iff e ⊑ m
- m ⊧ A ∗ B iff (∃ n, n′ ∈ M / n • n′ ⊑ m)(n ⊧ A and n′ ⊧ B)
- m ⊧ A −∗B iff (∀ n ∈ M)(n ⊧ A implies m • n ⊧ B)

The monotonicity property extends to P. Moreover these clauses can be read in terms of resources. For instance, one says that a world forces A ∗ B if and only if there is a partition of that world into components which force A and B. Moreover, one can understand the formula A−∗B as follows: if m is the cost of the function and n is the cost of any argument then the cost of obtaining the application of the function to the argument is m • n. Then, the multiplicatives depend on the internal structure of worlds and the additives should be understood in terms of conservation [12].

1 Compared to the original definition we use the reverse order (m ⊑ n instead of n ⊑ m) for presentation convenience

Definition 3. A Kripke resource interpretation (Kri) I = ⟨ M, •, e, ⊑, ⊧ ⟩ is a Krm M = ⟨ M, •, e, ⊑ ⟩ together with a forcing ⊧ on M.

Let I = ⟨ M, •, e, ⊑, ⊧ ⟩ be a Kri and Γ be a “bunch”, we write m ⊧ Γ if and only if m ⊧ A_{Γ}, where A_{Γ} is the formula obtained from Γ by replacing each “;” by ∧ and each “,” by ∗ with association respecting the tree structure of Γ.

Definition 4. The sequent Γ ⊢ A is said to be valid in I = ⟨ M, •, e, ⊑, ⊧ ⟩ (notation: Γ ⊧_{I} A), if and only if for any world m ∈ M, we have that m ⊧ Γ implies m ⊧ A. The sequent Γ ⊢ A is said to be valid (notation: Γ ⊧ A), if and only if for all I, we have Γ ⊧_{I} A.

Let us remind that the completeness result w.r.t. this semantics only holds for BI without the unit ⊥, denoted BI^{⊥}[12].

Theorem 2. 1. if Γ ⊢ A is provable in LBI, then Γ ⊧ A (soundness).

2. if Γ ⊧ A in BI^{⊥}then Γ ⊢ A is provable in LBI^{⊥}(completeness).

Corollary 2. Let A be a formula of BI^{⊥}, then A is valid if and only for any ⟨ M, •, e, ⊑, ⊧ ⟩ we have e ⊧ A.

Topological Kripke models have been proposed as a solution to have completeness for BI (with ⊥) but it is out of the scope of this paper in which we focus on the Kripke resource semantics and the fragment BI^{⊥}.

2.3 Resources and sharing interpretation

We have previously mentioned a resource-based interpretation of BI but it is important to notice that BI is different from Linear Logic (LL) and does not admit the standard number-of-uses reading of linear logic [7]. For instance, A −∗B ⊬ A → B holds in BI, whereas A −∘B ⊢ A → B in LL, with A → B defined as !A −∘B. On the other hand, ⊢ A −∗(A → A → B) → B is a judgement that holds in BI but not in LL because it does not respect the number-of-uses reading. BI offers a particular resource-based interpretation called the sharing interpretation and has promising results about logic programming [1], interference in imperative programs [11] and reasoning about mutable data structures like pointers [8]. For instance, the problem that arises when dealing with pointers is that you can have several pointers referencing the same cell in the computer store. This situation, called aliasing, is typically a problem of resource sharing once one has defined the resources as being “heaps” or, in other words, “portions of the computer store”. The computer store is made of cons cells having basic data (integers, for example), or pointers to other cons cells in their components. The model proposed in [8] deals with atomic propositions are of the form (x ↦ E, F) which means that x is a location pointing to a cons cell with first and second components respectively containing E and F as values. An interesting example, which shows that −∗ is about describing fresh heaps is given by the formula (x ↦ 3, 5) ∗ ((x ↦ 7, 5) −∗P). This formula can only be satisfied by heaps which contain a location x pointing to a cons cell the content of which is 3, 5, and such that, when updating the cons cell to 7, 5, the resulting heap satisfy P. It corresponds to a description of the update operation in terms of deletion followed by extension. Similar ideas have been successfully applied to write pre and post-conditions, using BI as an assertion language, for operations such as assignment, allocation and deallocation of a cons cell [8]. In order to prove such formulae, assertions or properties expressed in BI it seems important to study proof-search methods for this logic that build proofs but also generate countermodels.

3 A Labelled Tableaux calculus for BI^{⊥}

Because of the cohabitation of linear and intuitionistic connectives in BI and even if it includes IL and MILL as subsystems, we cannot directly extend to BI the proof-search (sequent, tableau, or connection) calculi defined for both [2,4,5,14]. Here, we apply the methodology of Labelled Deductive Systems (LDS)

[3] to the tableau method in order to propose a labelled tableau calculus TBI for propositional BI^{⊥}, the use of labels making it possible to generate countermodels.

3.1 A labelling algebra

We define a set of labels and constraints and a corresponding labelling algebra, that is a partially ordered algebraic system whose elements are denoted by labels.

Definition 5. A labelling language L contains the following symbols: a unit symbol 1, a binary function symbol ∘, a binary relation symbol ≤, a countable set of constants c_{1}, c_{2}, …, c_{n}.

Definition 6. The labels on L, the set of which is denoted L_{L} (or L), are inductively defined from the unit 1, constants, and expressions of the form x ∘ y in which x and y are labels having no common constants. Atomic labels are labels which do not contain any ∘, as opposed to compound labels which contain at least one ∘. Label constraints on L, which we note K_{L} (or K), are expressions of the form x ≤ y, where x and y are labels. The set L_{L} ∪ K_{L} is denoted LK_{L}. x is a sublabel of y (notation: x ⪯ y), if there exists a label z such that y = x∘z. We note x ≺ y if x ⪯ y and x ≠ y. P(x) denotes the set of the sublabels of x.

Definition 7. The labels and constraints are interpreted onto a labelling algebra in the following way:

1. ≤ is a preordering

2. ∘ is a binary operation on L satisfying: – associativity: (x ∘ y) ∘ z ≤ x ∘ (y ∘ z) and x ∘ (y ∘ z) ≤ (x ∘ y) ∘ z – identity: x ∘ 1 ≤ 1 ∘ x ≤ 1 and 1 ≤ 1 ∘ x ≤ x ∘ 1

– commutativity: x ∘ y ≤ y ∘ x and y ∘ x ≤ x ∘ y

– compatibility: x ≤ y and x′ ≤ y′ implies x ∘ x′ ≤ y ∘ y′

Let us define a particular closure operator \overline{(L, K)} on pairs (L, K) of sets of labels and constraints.

Definition 8. The closure \overline{(L, K)} is (\overline{L}, \overline{K}) that is defined as follows:

1. L ⊂ \overline{L} and K ⊂ \overline{K}

2. x ∈ \overline{L} implies P(x) ⊂ \overline{L}

3. x ≤ y ∈ \overline{K} implies x, y ∈ \overline{L}

4. x ∈ \overline{L} implies x ≤ x ∈ \overline{K} (reflexivity)

5. x ≤ y ∈ \overline{K} and y ≤ z ∈ \overline{K} implies x ≤ z ∈ \overline{K} (transitivity)

6. x ≤ y ∈ \overline{K} and x ∘ z ∈ \overline{L} implies x ∘ z ≤ y ∘ z ∈ \overline{K} (compatibility)

7. x ≤ y ∈ \overline{K} and y ∘ z ∈ \overline{L} implies x ∘ z ≤ y ∘ z ∈ \overline{K} (compatibility)

3.2 Labelled Formulae and Configurations

In the LDS approach the basic units of a deductive process are labelled formulae with labels in a given labelling algebra [3]. The derivation rules act on the labels as well as on the formulae according to fixed rules of propagation. Let us consider such an approach for the BI logic.

Definition 9. A (labelled) signed formula is a triple ⟨ Sg, A, l ⟩, denoted Sg A : l, Sg (∈ { F, T }) being the sign of the formula A (∈ P) and l (∈ L) its label.

Definition 10. An expansion set Es is ⟨ Lf(Es), C(Es), Ass(Es), Req(Es) ⟩ where Lf(Es) is a set of signed formulae built upon a set C(Es) of constants, Lab(Es) is the set of all labels in Lf(Es). Ass(Es) and Req(Es) are constraints (on labels) built on C(Es) which are respectively called assertions and obligations of Es. A configuration t is a set of expansion sets.

We have distinguished two kinds of constraints. The assertions behave as known facts (or hypothesis) while the obligations express goals that must be satisfied (using assertions if necessary). Now, we define a set of expansion rules for a configuration. For a given configuration t_{i}, we choose an expansion set on which we apply the corresponding expansion rule and then obtain a new configuration t_{i+1}. For instance for the (T A ∗ B : l) signed formula we have the following rule

⟨ Lf( T A ∗ B : l), C, As, Rq ⟩ c_{i}, c_{j} ∉ C
∗_{T}
⟨ Lf ∪ { T A : c_{i}, T B : c_{j} }, C ∪ { c_{i}, c_{j} }, As ∪ { c_{i} ∘ c_{j} ≤ l }, Rq ⟩

that we can simply present as follows (with c_{i} and c_{j} being new constants):

\begin{matrix}T A : c_{i} \\ T B : c_{j} \end{matrix} as : c_{i} ∘ c_{j} ≤ x T A ∗ B : x

\begin{matrix}F A : x \\ F B : x \end{matrix} F A ∨ B : x  _{T A : x  T B : x} T A ∨ B : x  \begin{matrix}T A : x \\ T B : x \end{matrix} T A ∧ B : x  _{F A : x F B : x} F A ∧ B : x

\begin{matrix}_{\begin{matrix}T A : c_{i} \\ F B : c_{i} \end{matrix} as : x ≤ c_{i}} F A → B : x & _{\begin{matrix}T A : c_{i} \\ T B : c_{j} \end{matrix} as : c_{i} ∘ c_{j} ≤ x} T A ∗ B : x & \begin{matrix}T A : c_{i} \\ F B : x ∘ c_{i} \end{matrix} F A −∗B : x \\ _{_{F A : y T B : y} rq : x ≤ y} T A → B : x & _{_{F A : y F B : z} rq : y ∘ z ≤ x} F A ∗ B : x & _{F A : y T B : x ∘ y} T A −∗B : x \end{matrix}

Figure 2. Tableau Expansion Rules

A TBI tableau is in fact a rooted tree with nodes labelled with a signed formula and built according to the expansion rules of figure 2. A tableau is what we have initially called a configuration and a branch of a tableau is an expansion set of this configuration. Let us comment the rules of figure 2. The rules of the first line are the classical α and β rules. The rules of the second line (called πα rules) are such that the constants c_{i} and c_{j} are new constants and the constraints on labels are assertions. The rules of the third line (called πβ rules) are such that the labels y and z only contain existing constants (at the moment of expansion) and the constraints are obligations.

Definition 11. Let A be a proposition of BI^{⊥}, a tableau sequence for A is a sequence of tableaux (or configurations) t_{1}, t_{2}, … for which the initial one is t_{1} = { ⟨ { F A : 1 }, ∅, ∅, ∅ ⟩ } and t_{i+1} is obtained from t_{i} by application of an expansion rule of figure 2 (on branch of t_{i}).

Let us remind that we first expand the πα formulae that introduce new constants c_{i} and c_{j} and then πβ formulae^{2} using such existing constants.

Definition 12. Let Es be an expansion set, two signed formulae T A : x, F A : y of Lf(Es) are complementary in Es if and only if x ≤ y ∈ \overline{Ass}(Es), i.e., if the constraint x ≤ y belongs to the reflexive, transitive and compatible closure of the assertion set of Es.

Definition 13. A tableau (or configuration) t is closed if, for all its branches (or expansion sets) Es,

2 The πα (resp. πβ) formulae are the initial formulae of the πα (resp. πβ) rules.

1) there are two formulae T A : x and F A : y that are complementary in Es or there is F ⊤ : x in Es or F I : x in Es with 1 ≤ x ∈ \overline{Ass}(Es) or T I : x in Es with 1 ≤ x ∉ \overline{Ass}(Es); 2) ∀ x ≤ y ∈ Req(Es), x ≤ y ∈ \overline{Ass}(Es). A tableau sequence T = t_{1}, t_{2}, … is closed if it contains at least one closed tableau.

3.3 An example

Let us now present the construction of a non-closed tableau for the formula ((A ∗ B) ∧ (A ∗ C)) −∗(A ∗ (B ∧ C)). The final tableau is given in figure 3. We begin the expansion with the initial multiplicative −∗, that produces two new formulae T (A ∗ B) ∧ (A ∗ C) : c_{1} and F A ∗ (B ∧ C) : c_{1}. Step 2 deals with the additive ∧, and results in two multiplicatives: T A ∗ B : c_{1} and T A ∗ C : c_{1}. The expansion of the first ∗ in step 3 introduces two new constants c_{2}, c_{3} and the assertion as_{1} : c_{2} ∘ c_{3} ≤ c_{1}. The second ∗ is handled in step 4 and introduces two new constants c_{4}, c_{5} together with the assertion as_{2} : c_{4} ∘ c_{5} ≤ c_{1}. We are now left with the remaining πβ formula. To expand it, we must match an obligation and find a compound label y ∘ z such that y ∘ z ≤ c_{1}. From the assertions in the branch, we deduce that two instantiations are possible: either y = c_{2} and z = c_{3}, or y = c_{4} and z = c_{5}. Both instantiations must be used for the tableau expansion. Step 5 goes on with the first one, namely, rq_{1} : c_{2} ∘ c_{3} ≤ c_{1}, and splits the tableau into two new branches. The first branch is immediately closed since it contains both T A : c_{2} and F A : c_{2} and one obviously has c_{2} ≤ c_{2}. The second branch yields a ∧ connective which is immediately expanded in step 6 (remind that α and πα formulae have higher precedence than β and πβ formulae) and we obtain two new branches. Once again, the first branch is closed since it contains ⟨ T B : c_{3}, F B : c_{3} ⟩. The second branch contains a potential connection ⟨ T C : c_{5}, F C : c_{3} ⟩ but there is no way to prove c_{5} ≤ c_{3} from the closure of the assertions that are in the branch. After step 6, there are no more α or πα formulae to expand. However, the tableau is not yet completely analyzed because we have not tested the second possibility for the πβ formula, that is y = c_{4} and z = c_{5}. Therefore, step 7 expands the remaining unclosed branch with this second instantiation and yields a subtree which is similar to the one developed at step 5, except that c_{2} and c_{3} are respectively replaced by c_{4} and c_{5}. We obtain two closed branches, one with ⟨ T A : c_{4}, F A : c_{4} ⟩ and another one with ⟨ T C : c_{5}, F C : c_{5} ⟩. Thus, all formulae have been treated and the fourth branch of the tree is not closed. Indeed, we have two potential connections ⟨ T B : c_{3}, F B : c_{5} ⟩ and ⟨ T C : c_{5}, F C : c_{3} ⟩, but neither c_{3} ≤ c_{5}, nor c_{5} ≤ c_{3} can be deduced from the closure of the assertions that are in the branch.

4 Properties of the TBI calculus

In this section we prove the soundness and completeness of the TBI calculus w.r.t. the Kripke resource semantics. It provides not only a procedure for proof construction but also for countermodel generation.

\begin{matrix}√_{2} T (A ∗ B) ∧ (A ∗ C) : c_{1} \\ \begin{matrix}√_{3} T A ∗ B : c_{1} \\ _{\begin{matrix}T A : c_{2} \\ _{\begin{matrix}T A : c_{4} \\ _{_{\begin{matrix}F A : c_{2} \\ × \end{matrix} _{\begin{matrix}F B : c_{3} \\ × \end{matrix} _{_{_{\begin{matrix}F A : c_{4} \\ × \end{matrix} _{F B : c_{5}  \begin{matrix}F C : c_{5} \\ × \end{matrix}} √_{8} F B ∧ C : c_{5}} rq_{2} : c_{4} ∘ c_{5} ≤ c_{1}} F C : c_{3}}} √_{6} F B ∧ C : c_{3}} rq_{1} : c_{2} ∘ c_{3} ≤ c_{1}} & T C : c_{5} \end{matrix} as_{2} : c_{4} ∘ c_{5} ≤ c_{1}} & T B : c_{3} \end{matrix} as_{1} : c_{2} ∘ c_{3} ≤ c_{1}} & √_{4} T A ∗ C : c_{1} \end{matrix} & √_{5,7} F A ∗ (B ∧ C) : c_{1} \end{matrix} √_{1} F ((A ∗ B) ∧ (A ∗ C)) −∗(A ∗ (B ∧ C)) : 1

Figure 3. Tableau for ((A ∗ B) ∧ (A ∗ C)) −∗(A ∗ (B ∧ C))

4.1 Soundness

Definition 14. Let I = ⟨ M, •, e, ⊑, ⊧ ⟩ be a Kri and Es be an expansion set, an interpretation of Es in I is an application ∥_∥ : C(Es) → M. An interpretation ∥_∥ can straightforwardly be extended to labels and constraints as follows: ∥1∥ = e, ∥x ∘ y∥ = ∥x∥ • ∥y∥ and ∥x ≤ y∥ = ∥x∥ ⊑ ∥y∥. We say that an interpretation ∥_∥ is a realization of Es in I, or equivalently, that ∥_∥ realizes Es in I, if:

a) for any signed formula T A : x in Lf(Es) ∥x∥ ⊧ A,

b) for any signed formula F A : x in Lf(Es) ∥x∥ |̸= A,

c) for any x ≤ y in Ass(Es) ∥x∥ ⊑ ∥y∥.

Definition 15. A branch Es is realizable if there exists I = ⟨ M, •, e, ⊑, ⊧ ⟩ and a realization of Es in I. A tableau t is realizable if it contains a realizable branch.

Lemma 1. Let t be a tableau and Es a branch of t, let I = ⟨ M, •, e, ⊑, ⊧ ⟩ be a Kri and ∥_∥ be a realization of Es in I, then for all x ≤ y ∈ \overline{Ass}(Es) we have ∥x∥ ⊑ ∥y∥.

Proof. By definition, for all x ≤ y in Ass(Es) we have ∥x∥ ⊑ ∥y∥. We have to show that the operation of closure preserves the ordering and it is straightforward because ⊑ is a preorder that is compatible with •.

Theorem 3. A closed tableau cannot be realizable.

Proof. Let t be a closed tableau that is also realizable. Then, there are Es ∈ t, I = ⟨ M, •, e, ⊑, ⊧ ⟩ and ∥_∥ a realization of Es in I. By definition of closure on Es we have T A : x and F A : y such that x ≤ y ∈ \overline{Ass}(Es). Since ∥_∥ realizes t we have ∥x∥ ⊧ A and ∥y∥ |̸= A. Moreover, x ≤ y ∈ \overline{Ass}(Es) implies that ∥x∥ ⊑ ∥y∥ by lemma 1. Then, we obtain a contradiction because we should have ∥y∥ ⊧ A by monotonicity.

Theorem 4. Let t be a tableau and t′ a tableau obtained from t by application an expansion rule, if t is realizable then t′ is realizable .

Proof. By case analysis on the expansion rule. Since t is realizable, there are Es ∈ t, I = ⟨ M, •, e, ⊑, ⊧ ⟩ and ∥_∥ a realization of Es in I.

- Case T A ∗ B : z ∈ Lf(Es); Es is replaced in t′ by a new expansion set Es′ such that Lf(Es′) := Lf(Es) ∪ { T A : c_{i}, T B : c_{j} }, Ass(Es′) := Ass(Es) ∪ { c_{i} ∘ c_{j} ≤ z }, c_{i} and c_{j} being new constants. Since ∥_∥ realizes Es, we have ∥z∥ ⊧ A ∗ B. Therefore, there are m, n ∈ M such that m • n ⊑ ∥z∥ and m ⊧ A and n ⊧ B. We extend ∥_∥ with ∥c_{i}∥ = m and ∥c_{j}∥ = n. Thus, we obtain ∥c_{i}∥ ⊧ A and ∥c_{j}∥ ⊧ B. Since ∥c_{i}∥ • ∥c_{j}∥ ⊑ ∥z∥ is obtained from ∥c_{i} ∘ c_{j} ≤ z∥, we have that Es′ is realizable and, consequently, t′ is realizable.

- Case F A ∗ B : z ∈ Lf(Es); Es is replaced in t′ by two new expansion sets Es′ and Es′′ such that Lf(Es′) := Lf(Es)∪{ F A : x }, Lf(Es′′) := Lf(Es)∪{ F B : y } and Req(Es′) = Req(Es′′) := Req(Es) ∪{ x ∘ y ≤ z }. A valid application of the F ∗ expansion rule requires that the obligation x ∘ y ≤ z should be derivable from the closure of the assertions of Es. Thus, x ∘ y ≤ z ∈ \overline{Ass}(Es) and lemma 1 imply ∥x∥ • ∥y∥ ⊑ ∥z∥. Since ∥_∥ realizes Es, we have ∥z∥ |̸= A ∗ B. Therefore, for all m, n ∈ M such that m • n ⊑ ∥z∥, either m |̸= A, or n |̸= B which implies that either ∥x∥ |̸= A or ∥y∥ |̸= B. Then, either Es′, or Es′′ is realized by ∥_∥ and we can conclude that t′ is realizable.

- The other cases are similar.

Corollary 3. Let T = t_{1}, t_{2}, …, t_{n} be a tableau sequence, if t_{i} is realizable then, for j > i, t_{j} is realizable.

Theorem 5 (soundness). Let A a formula of BI^{⊥} if there exists a closed tableau T for A, then A is valid in Kripke resource semantics.

Proof. Let T = t_{1}, t_{2}, …, t_{n} be a closed tableau sequence. Let us suppose that A does not hold in Kripke resource semantics. Then, by corollary 2, there exists a Kri I = ⟨ M, •, e, ⊑, ⊧ ⟩ such that e |̸= A. Then, the configuration t_{1} = { ⟨ { F A : 1 }, ∅, ∅, ∅ ⟩ } is realizable. But theorem 4 implies that all t_{i}, for i > 1, are also realizable. It follows from theorem 3 that none of the t_{i} can be closed and consequently T cannot be closed.

4.2 A Tableau construction procedure

We introduce the notion of completed branch [3] for the TBI calculus. Moreover, we define what a redundant branch is and propose a procedure that builds a nonredundant tableau for a given formula A in a finite number of steps.

Definition 16. Let Es be a tableau branch, a signed formula F X : x is fulfilled (or completely analyzed) in Es if

1. X ≡ A ∧ B and either F A : x ∈ Es, or F B : x ∈ Es

2. X ≡ A ∨ B and both F A : x ∈ Es and F B : x ∈ Es

3. X ≡ A → B and there exists y such that x ≤ y ∈ \overline{Ass}(Es) and both T A : y ∈ Es and F B : y ∈ Es

4. X ≡ A ∗ B and for all y, z such that y ∘ z ≤ x ∈ \overline{Ass}(Es) either F A : y ∈ Es, or F B : z ∈ Es

5. X ≡ A−∗B and there exists y such that x∘y ∈ \overline{Lab}(Es) and both T A : y ∈ Es and F B : x ∘ y ∈ Es

and a signed formula T X : x is fulfilled in Es if

1. X ≡ A ∧ B and both T A : x ∈ Es and T B : x ∈ Es

2. X ≡ A ∨ B and either T A : x ∈ Es, or T B : x ∈ Es

3. X ≡ A → B and for all y such that x ≤ y ∈ \overline{Ass}(Es) either F A : y ∈ Es, or T B : y ∈ Es

4. X ≡ A ∗ B and there exists y, z such that y ∘ z ≤ x ∈ \overline{Ass}(Es) and both T A : y ∈ Es and T B : z ∈ Es

5. X ≡ A −∗B and for all y such that x ∘ y ∈ \overline{Lab}(Es) either F A : y ∈ Es, or T B : x ∘ y ∈ Es

Definition 17. A tableau branch Es is completed if every labelled signed formula Sg A : x in Es is fulfilled. A tableau is completed if it has a branch that is completed. A tableau branch Es is a H-branch if it is open and completed.

Definition 18. A tableau branch Es is redundant if it contains a signed formula T C −∗D : x which has been expanded with a label y ∘ c_{i}, where the constant c_{i} has been introduced by a signed formula F A −∗B : x ∘ y which derives from a previous expansion of T C −∗D : x with the label y. Such a signed formula T C −∗D : x that has been redundantly expanded in the branch Es is called a redundant T −∗ formula.

F Φ : y T Ψ ⊕ ((Λ ⊕ (A −∗B)) → Ω) : x ∘ y ; ⋮ ; _{F Λ ⊕ (A −∗B) : x ∘ y ; ⋮ ; T A : c_{i} ; F B : x ∘ y ∘ c_{i} ; ⋮ ; T A : c_{j} ; F B : x ∘ y ∘ c_{i} ∘ c_{j} ; ⋮ √_{l} F A −∗B : x ∘ y ∘ c_{i} √_{k} F A −∗B : x ∘ y  T Ω : x ∘ y} √_{j} T (Λ ⊕ (A −∗B)) → Ω : x ∘ y ⋮ ; √_{i} T Φ −∗(Ψ ⊕ ((Λ ⊕ (A −∗B)) → Ω)) : x

Figure 4. Schema of a redundant branch

The notion of redundancy is illustrated in figure 4 that presents the general situation in which a branch can grow infinitely. The symbol ⊕ represents an additive conjunction or disjunction. Similarly, Ψ and Λ are formulae whose outermost connectives are either additive conjunction or disjunction. In the tableau, we can see that the step i expands a formula of type T −∗ with a label y to achieve fulfillment of the formula. Then, step k expands a formula of type F −∗ which derives from the preceding expansion (after a given number of successive expansions), introducing, by the way, a new constant c_{i} and new label x ∘ y ∘ c_{i}. Therefore, to retain fulfillment for the root formula, we are obliged to apply an expansion step with label y ∘ c_{i}. It results in a redundant tableau since we already have expanded the tableau with label y and c_{i} has been introduced by the formula F A −∗B : x ∘ y which is derived from T Φ −∗(Ψ ⊕ ((Λ ⊕ (A −∗B)) → Ω)) : x. If such a redundant expansion is performed then we obtain an infinite branch with the creation of new constants c_{j},c_{k},… and new labels x ∘ y ∘ c_{j}, x ∘ y ∘ c_{j} ∘ c_{k},. . .. In the rest of the section, we will respectively note c_{i1},c_{i2}, …,c_{ij} the copies of the initial constant c_{i} that are introduced by redundant expansion steps.

Definition 19. A tableau sequence T is redundant if it contains a tableau that has at least one redundant branch. Otherwise, it is said non-redundant.

A tableau construction procedure is an algorithm which, given a formula A, builds a tableau sequence t_{1}, t_{2}, …, t_{n} until there exists a tableau t_{i} that is either closed or with a H-branch. Otherwise it does not terminate. Let us give a procedure that builds a tableau sequence T including a nonredundant tableau. The initial signed formula is F A : 1. Repeat until T is closed or completed

– choose an open branch Es

– if there is a unfulfilled α or πα formula (Sg A : x) in Es then apply the corresponding expansion rule to it else if there is an unfulfilled β or πβ formula (Sg A : x) in Es, on which one can apply an expansion rule without building a redundant tableau, then apply the corresponding expansion rule, with all labels for which the formula is not fulfilled.

Theorem 6. This procedure that builds a non-redundant tableau terminates (in finitely many steps).

Proof. To prove the termination, we must show that any expansion step performed by the procedure provides a closed tableau, or a completed tableau, or a redundant tableau. For that, we show that if a branch is open then it cannot be expanded without reaching a step where it is completed or redundant. We can define a measure of complexity of a branch as the sum of the complexities of all its signed formulae and the complexity of a signed formula is defined from the syntactic complexity of the formula and the number of labels for which it is unfulfilled. Another way to achieve termination could be to use liberalized versions of the πα rules, as explained in [3]. The πα rules require new constants and liberalized rules allow us, under given conditions, to reuse constants which have previously been introduced. Thus, they provide a way to control the syntactic complexity of the labels. For example, when expanding F A → B : x, one can simply infer F B : x, instead of introducing a new constant c such that x ≤ c, if there already exists T A : y with y ≤ x in the branch. Similar considerations can be applied to the other πα rules.

4.3 Countermodel construction

In this subsection, we describe how to construct a countermodel of A from a H-branch in a tableau for A.

Definition 20. Let Es be a H-branch, the structure M(Es) associated to Es is defined by M(Es) = ⟨ M, •, 1, ⊑ ⟩ where

i) M is the set \overline{Lab}(Es) extended with a particular element denoted by π. ii) • is a composition law defined by

x • 1 = 1 • x = x
x • y = y • x = x ∘ y  if x ∘ y ∈ \overline{Lab}(Es)
x • y = y • x = π  otherwise

iii) the relation ⊑ between elements of M is defined by

x ⊑ y if and only if x = y = π or x ≤ y ∈ \overline{Ass}(Es)

Lemma 2. Let Es be a H-branch and M(Es) = ⟨ M, •, 1, ⊑ ⟩ the M-structure associated to Es, then M(Es) is a Kripke resource monoid.

Proof. It is straightforward to show that • is a monoidal law on M. ⊑ is a preordering because of the reflexivity and transitivity of the set of assertions and it is compatible with the monoidal law • because of the closure operations performed on the assertion set.

Definition 21. Let Es be a H-branch and M(Es) = ⟨ M, •, 1, ⊑ ⟩ be the Krm built from Es, a forcing relation ⊧_{Es} on M × A, where A is the set of atomic propositions that occur in Es, is defined as follows: 1) π ⊧ A, 2) if T A : x ∈ Es then x ⊧ A and 3) if y ⊧ A and y ≤ x ∈ \overline{Ass}(Es) then x ⊧ A.

Lemma 3. Let Es be a H-branch, M(Es) = ⟨ M, •, 1, ⊑ ⟩ be the Krm built from Es and the forcing relation ⊧_{Es}, the following properties hold:

i) for any formula A, we have π ⊧ A. ii) ⟨ M, •, 1, ⊑, ⊧_{Es} ⟩ is a model of Es, i.e., T A : x ∈ Es implies x ⊧ A and F A : x ∈ Es implies x |̸= A.

Proof. see in appendix A.

Theorem 7. If Es is a H-branch then it has a Kripke resource model.

Proof. Let us consider the previous intermediate lemmas. Lemma 2 shows how to build a Kripke resource monoid from the information that is in the set \overline{Ass}(Es) of a H-branch. Lemma 3 allows to define a forcing relation on such a monoid to obtain a model of each labelled formula in the H-branch. The final result can be directly deduced.

4.4 Completeness and finite model property

Theorem 8 (completeness). If A is a proposition of BI^{⊥} which is valid in Kripke resource semantics, then there exists a closed tableau for A.

Proof. Let us suppose that there is no closed tableau for A. Then, there exists a tableau for A which contains a H-branch from which we can build a model in which A is not satisfied.

In order to analyze the finite model property, we observe that we have the following result for a redundant H-branch Es.

Theorem 9. If Es is a redundant H-branch then it has a finite Kripke resource model.

Proof. see in appendix B.

Theorem 10. If there is a tableau for A which contains a H-branch, then there is a model in which A is not satisfied. Moreover if the branch is finite then the model is finite.

Proof. From a H-branch Es, redundant or not, we can build a model (see previous results). It is obvious by the construction that the model is finite if Es is finite.

Let us suppose there is no closed tableau for A. The procedure of construction of a non-redundant tableau yields a tableau for A which contains a finite Hbranch (cf. termination result) from which we can construct a finite model in which A is not satisfied. Then, for a given A as input, the procedure yields either a closed tableau for A or a tableau for A which contains a H-branch, from which we can build a finite countermodel of A. Then we have the following result: BI^{⊥} has the finite model property with respect to Kripke resource semantics.

4.5 Extraction of a countermodel

Let us consider the formula ((A ∗ B) ∧ (A ∗ C)) −∗(A ∗ (B ∧ C)) and its complete tableau expansion given in figure 3. It contains an open branch, which means that the formula is not provable. Since all formulae in the open branch are fulfilled, we have a finite H-branch Es. We can therefore extract the corresponding countermodel following the steps of the completeness proof. First, we associate a Kripke resource monoid structure to \overline{Ass}(Es) and add a particular element π. The monoidal law • is given by the following table:

\begin{matrix}• & 1 & c_{1} & c_{2} & c_{3} & c_{4} & c_{5} & c_{2} ∘ c_{3} & c_{4} ∘ c_{5} & π \\ 1 & 1 & c_{1} & c_{2} & c_{3} & c_{4} & c_{5} & c_{2} ∘ c_{3} & c_{4} ∘ c_{5} & π \\ c_{1} & c_{1} & π & π & π & π & π & π & π & π \\ c_{2} & c_{2} & π & π & c_{2} ∘ c_{3} & π & π & π & π & π \\ c_{3} & c_{3} & π & c_{2} ∘ c_{3} & π & π & π & π & π & π \\ c_{4} & c_{4} & π & π & π & π & c_{4} ∘ c_{5} & π & π & π \\ c_{5} & c_{5} & π & π & π & c_{4} ∘ c_{5} & π & π & π & π \\ c_{2} ∘ c_{3} & c_{2} ∘ c_{3} & π & π & π & π & π & π & π & π \\ c_{4} ∘ c_{5} & c_{4} ∘ c_{5} & π & π & π & π & π & π & π & π \\ π & π & π & π & π & π & π & π & π & π \end{matrix}

The preordering relation ⊑ is simply embodied by the relation ≤ in \overline{Ass}(Es) and the atomic forcing relation ⊧ is defined as follows:

\begin{matrix}1 & c_{1} & c_{2} & c_{3} & c_{4} & c_{5} & c_{2} ∘ c_{3} & c_{4} ∘ c_{5} & π \\ − & − & A & B & A & C & − & − & A, B, C \end{matrix}

Now, we observe that c_{1} ⊧ (A ∗ B) ∧ (A ∗ C). Indeed, from c_{2} ⊧ A and c_{3} ⊧ B, we deduce c_{2} • c_{3} ⊧ A ∗ B and since c_{1} ⊑ c_{2} • c_{3} we have by Kripke monotonicity, c_{1} ⊧ A ∗ B. A similar analysis on c_{4} and c_{5} yields the second component of ∧, namely, c_{1} ⊧ A ∗ C. But, we have c_{1} |̸= A ∗ (B ∧ C) because B ∧ C is not forced by any world, other than π, and no world in relation with c_{1} can be obtained from a composition involving π. Therefore, we have a countermodel of ((A ∗ B) ∧ (A ∗ C)) −∗(A ∗ (B ∧ C)).

5 Conclusion

In this paper we have designed a labelled tableau calculus for the propositional BI logic. This new logic has been recently studied as an assertion language for reasoning about mutable data structures [8]. It could be seen as a logical foundation for new specification logics, in order to specify and prove particular properties of programs or systems. Our labelled calculus for BI yields not only proofs for theorems but also countermodels for non-theorems. The resulting countermodels are finite and thus, in addition to the completeness of the calculus, we have proved the finite model property for BI with respect to the Kripke resource semantics. Our approach is based on this semantics and on the methodology of LDS for analytic deduction [3], that has been recently used for MILL and a simple semantics [14]. Labels and constraints are appropriate for proof-search in such a mixed logic, as observed in previous work in Mixed Linear Logic [6], in order to take into account the interaction between both kinds of connectives. In further work we will study the representation and resolution of constraints during the tableau construction and also the extraction of countermodels. We will define another labelled calculus with free variables in labels and also a related connection-based characterization of provability in BI. The restriction of our calculus to IL and MILL will provide new proof-search procedures for both logics that we will study. Finally, we will develop a similar method with countermodel generation in BI (with ⊥) but starting from Grothendieck sheaf-theoretic models [12].

References

1. P.A. Armelin and D. Pym. Bunched logic programming (extended abstract). In First International Joint Conference on Automated Reasoning, IJCAR 2001, LNCS 2083, pages 289–304, Siena, Italy, 2001.

2. V. Balat and D. Galmiche. Labelled Deduction, volume 17 of Applied Logic Series, chapter Labelled Proof Systems for Intuitionistic Provability. Kluwer Academic Publishers, 2000.

3. M. D’Agostino and D.M. Gabbay. A Generalization of Analytic Deduction via Labelled Deductive Systems. Part I: Basic substructural logics. Journal of Automated Reasoning, 13:243–281, 1994.

4. D. Galmiche. Connection Methods in Linear Logic and Proof nets Construction. Theoretical Computer Science, 232(1-2):231–272, 2000.

5. D. Galmiche and D. Larchey-Wendling. Structural sharing and efficient proofsearch in propositional intuitionistic logic. In Asian Computing Science Conference, ASIAN’99, LNCS 1742, pages 101–112, Phuket, Thailand, December 1999.

6. D. Galmiche and J.M. Notin. Proof-search and proof nets in mixed linear logic. Electronic Notes in Theoretical Computer Science, 37, 2000.

7. J.Y. Girard. Linear logic: its syntax and semantics. In J.Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 1–42. Cambridge University Press, 1995.

8. S. Ishtiaq and P. O’Hearn. Bi as an assertion language for mutable data structures. In 28th ACM Symposium on Principles of Programming Languages, POPL 2001, pages 14–26, London, UK, 2001.

9. H. Mantel and J. Otten. linTAP : A tableau prover for linear logic. In Int. Conference TABLEAUX’99, LNCS 1617, pages 216–231, Saratoga Springs, NY, USA, 1999.

10. R.K. Meyer, M.A. McRobbie, and N. Belnap. Linear analytic tableaux. In Theorem proving with analytic tableaux and related methods, TABLEAUX’95, LNCS 918, pages 278–293, St Goar am Rhein, Germany, 1995.

11. P. O’Hearn. Resource interpretations, bunched implications and the αλ-calculus. In Typed Lambda Calculi and Applications, TLCA’99, LNCS 581, pages 258–279, L’Aquila, Italy, 1999.

12. P.W. O’Hearn and D. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215–244, 1999.

13. D. Pym. On bunched predicate logic. In 14h Symposium on Logic in Computer Science, pages 183–192, Trento, Italy, July 1999. IEEE Computer Society Press.

14. K. Terui. Labelled tableau calculi generating simple models for substructural logics. Technical report, ILLC publications, University of Amsterdam, 1999.

15. A. Urquhart. Semantics for relevant logic. Journal of Symbolic Logic, 37:159–169, 1972.

A Proof of lemma 3

Lemma 3. Let Es be a H-branch, M(Es) = ⟨ M, •, 1, ⊑ ⟩ be the Krm built from Es and the forcing relation ⊧_{Es}, the following properties hold:

i) for any formula A, we have π ⊧ A. ii) ⟨ M, •, 1, ⊑, ⊧_{Es} ⟩ is a model of Es.

Proof. We prove i) by induction on the degree of A.

– if A is atomic then, by definition, π ⊧ A

– if A ≡ B ∧ C then, by induction hypothesis, we have π ⊧ B and π ⊧ C, and therefore, π ⊧ B ∧ C.

– if A ≡ B ∨ C then, by induction hypothesis, we have π ⊧ B and therefore, π ⊧ B ∨ C.

– if A ≡ B → C then, by induction hypothesis, we have π ⊧ C. Since no x in M other than π verifies π ≤ x, we have π ⊧ B → C.

– if A ≡ B −∗C, then by induction hypothesis, we have π ⊧ C. Since π • x = π whatever x in M, we have π ⊧ B −∗C.

– if A ≡ B ∗ C, then by induction hypothesis, we have π ⊧ B and π ⊧ C. Since π • π = π, we have π ⊧ B ∗ C.

We prove ii) by induction on the degree of the formula Sg A : x in Es.

– if T A : x ∈ Es and A is atomic then, by definition, x ⊧ A.

– if F A : x ∈ Es and A is atomic then, since Es is an H-branch, it cannot contain an occurrence of T A : x at the same time. Moreover, since x cannot be π, we have x |̸= A.

– if T B ∧ C : x ∈ Es then, since Es is a H-branch, both T B : x ∈ Es and T C : x ∈ Es. By induction hypothesis, it follows that x ⊧ B and x ⊧ C. Thus, x ⊧ B ∧ C.

– if F B ∧ C : x ∈ Es then, since Es is a H-branch, either F B : x ∈ Es, or F C : x ∈ Es. By induction hypothesis, it follows that either x |̸= B, or x |̸= C. Thus, x |̸= B ∧ C.

– case T B ∨ C : x ∈ Es is similar to case F B ∧ C : x ∈ Es

– case F B ∨ C : x ∈ Es is similar to case T B ∧ C : x ∈ Es

– if T B → C : x ∈ Es then, since Es is a H-branch, for all y in \overline{Lab}(Es) such that x ≤ y ∈ \overline{Ass}(Es) we have either F B : y ∈ Es or T C : y ∈ Es. Since x ≤ y implies x ⊑ y, it follows from induction hypothesis that for all y ∈ M such that x ⊑ y, either y |̸= B or y ⊧ C. Thus, x ⊧ B → C.

– if F B → C : x ∈ Es, then since Es is a H-branch, there exists y in \overline{Ass}(Es) such that x ≤ y ∈ \overline{Ass}(Es) and both F B : y ∈ Es and T C : y ∈ Es. It follows from induction hypothesis that there exists y ∈ M such that x ≤ y and both y ⊧ B and y |̸= C. Thus, x |̸= B → C.

– if T B −∗C : x ∈ Es, let y ∈ M. Suppose x∘y ∈ \overline{Ass}(Es) then x•y = x∘y and since Es is a H-branch, we have that, for all y in \overline{Ass}(Es) such that x ∘ y ∈ \overline{Ass}(Es), either F B : y ∈ Es or T C : x ∘ y ∈ Es. By induction hypothesis, it follows that either y |̸= B, or x • y ⊧ C. Suppose x ∘ y ∉ \overline{Ass}(Es), then x • y = π. By property i), we can conclude that π ⊧ C. Therefore, we have shown that for all y ∈ M, either y |̸= B or x • y ⊧ C, that is, x ⊧ B −∗C.

– if F B −∗C : x ∈ Es then, since Es is a H-branch, there exists y in \overline{Ass}(Es) such that x ∘ y is in \overline{Ass}(Es) and both T B : y ∈ Es and F C : x ∘ y ∈ Es. By induction hypothesis, it follows that y ⊧ B and x ∘ y |̸= C. As x ∘ y ∈ \overline{Ass}(Es) implies x • y = x ∘ y, we have x • y |̸= C, and thus x |̸= B −∗C.

– case T B ∗ C : x ∈ Es is similar to case F B → C : x ∈ Es

– case F B ∗ C : x ∈ Es is similar to case T B → C : x ∈ Es

B Proof of theorem 9

Theorem 9. A redundant H-branch Es has a finite Kripke resource model.

Proof. The proof is by induction on the number of redundant T −∗ formulae in the H-branch. Such formulae require an infinite number of elements of the monoid to be satisfied. Base case: if there is no redundant formula, then Es is a finite H-branch and by theorem 7 we have a finite Kripke resource model of the H-branch. Induction case: we assume that the proposition holds for any redundant H-branch with less than n redundant T −∗ formulae. Let us select a redundant T −∗ formula in the H-branch. Since the H-branch is redundant, it has the form given in figure 4 and is infinite. In this case, theorem 7 provides an infinite Kripke resource model M(Es) for the H-branch. The situation in M(Es) is the following:

The infinite regression uses an infinity of copies of c_{i} to satisfy the T −∗ formula. Let us now explain how to transform M(Es) into a Kripke resource model M′(Es) in which only a finite number of copies of c_{i} are used while preserving the property of being a model of the H-branch Es. We define the composition × on M′(Es) as follows: a × b = x ∘ y ∘ c_{i} if a • b = x ∘ y ∘ c_{i} ∘ c_{i1} and a • b otherwise. In fact, we have replaced each occurrence of x ∘ y ∘ c_{i} ∘ c_{i1} in the table of • by x ∘ y ∘ c_{i}. The fact that M(Es) is a monoid and that we have replaced all occurrences at the same time is enough to ensure that M′(Es) remains a monoid. But, since the element x ∘ y ∘ c_{i} ∘ c_{i1} can no longer be obtained in M′(Es), we can remove it from the monoid and also all the elements that depend on it, that is, all subsequent copies c_{i2},c_{i3},. . .. The situation in M′(Es) then becomes the following:

We only keep one copy c_{i1} of c_{i}, meaning that all other copies are equivalent to the original one. It remains to show that M′(Es) is a Kripke resource model of the πβ formulae of Es. Since we only change the monoidal law, the only formulae that may be affected are the ones that involve the composition of the resources, that are the ones of type T −∗ and F ∗. Let us consider the formulae F A ∗ B : z, knowing that the other case is similar. If z does not contain c_{i} or copies c_{ij} then the result is immediate because × behaves like • and z |̸= A ∗ B in M(Es). Otherwise, z contains c_{i} and copies of c_{i}. All these copies reduce to c_{i1} in M′(Es). Moreover, since z contains c_{i}, all copies are absorbed by c_{i} as prescribed in the definition of ×. Thus, we need to show that x ∘ y ∘ c_{i} |̸= A ∗ B in M′(Es). Compared with what happens in M(Es), the difference is that x ∘ y ∘ c_{i} can also be obtained from compositions u × v such that u and v possibly contain copies of c_{i}. But, we necessarily have either u |̸= A or v |̸= B, otherwise we would have u • v ⊧ A ∗ B in M(Es), which is impossible because M(Es) is a Kripke resource model. Thus, we have a Hbranch Es which contains one less T −∗ redundant formula that requires an infinite set of elements to be satisfied. The induction hypothesis can therefore be applied and we conclude that Es has a model.