Semantic Labelled Tableaux for Propositional BI^{⊥}

Didier Galmiche and Daniel Méry

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

Abstract

In this paper, we study semantic labelled tableaux for the propositional Bunched Implications logic (BI) that freely combines intuitionistic logic (IL) and multiplicative intuitionistic linear logic (MILL). BI is a resource-aware logic that captures interferences between resources and it is well suited, because of its resource-based sharing interpretation, for reasoning about mutable data structures. We propose a labelled tableau calculus for BI^{⊥}^{1} based on particular labels and constraints. We prove the soundness and completeness of this calculus w.r.t. the Kripke resource semantics with an emphasis on countermodel construction. In addition, we prove the finite model property and as a consequence the decidability of BI^{⊥}. Moreover, we analyze some algorithmic aspects of the tableau construction by providing a free variable variant of the calculus. We also develop the restrictions to IL and MILL that provide new tableau methods for both logics with generation of countermodels.

1 Introduction

In this paper, we consider the propositional Bunched Implications (BI) logic, in which multiplicative (or linear) and additive (or intuitionistic) connectives cohabit [29]. This resource-aware logic can be viewed as a merging of intuitionistic logic (IL) and multiplicative intuitionistic linear logic (MILL) that allows to capture interferences between resources. It can be well understood through its Kripke resource models [21] but also proof-theoretically through its bunched sequent calculus [34] and the corresponding αλ-calculus [27]. With its so-called sharing interpretation, the BI logic appears as an appropriate logical foundation for logic programming [2], for reasoning about mutable data structures [20] and for problems dealing with interferences between resources. In this context, we aim to study proof-search methods that build proofs or countermodels in case of non-provability. There exist such methods, based on a sequent calculus [13] or a labelled tableau calculus [36], for IL and MILL. But they cannot be adapted or extended to BI and therefore specific notions and concepts seem necessary in order to capture the interferences between the different connectives which occur during the proof-search process. We know that the tableau method directly provides countermodel generation for a wide range of logics, including IL, but not for substructural logics like linear logic [25, 26]. In this work, we focus on the Kripke resource semantics of BI [21] in which the possible worlds are justified in terms of pieces of information [37]. It is important to mention that the unit ⊥ of the additive disjunction internalizes inconsistency in BI and that the Kripke resource semantics does not account for inconsistency (⊥ is nowhere forced). Accordingly, the completeness result w.r.t. this semantics only holds for BI^{⊥} [29, 35], fragment to which we initially restrict our study. A key point of our work consists in defining labels and labelled formulas, the role of which being to capture some semantical information into the syntax. Then, we propose a labelled tableau calculus for propositional BI^{⊥} with expansion rules that generate constraints on labels. Such constraints are able to capture the semantics of the connective interactions occuring in the proofsearch. Thus, we define a tableau construction procedure that is characterized by the generation of two particular kinds of label constraints, called assertions and requirements. In this context, the provability is characterized through a tableau construction with specific closure conditions in which the set of requirements has to be verified from the set of assertions. Our labelled calculus is proved sound and complete (by a countermodel construction method). For a given BI^{⊥} formula A, we provide a procedure that yields either a tableau proof or a countermodel of A. Moreover, we prove the finite model property for propositional BI^{⊥} w.r.t. Kripke resource semantics, property which is important but not trivial for substructural logics [32]. As a consequence, we give a tableau construction procedure that terminates and generates finite countermodels in case of non-provability. We observe that the set of assertions can be represented as a graph, called dependency graph, that is built in parallel with the tableau for a formula A. Then, the requirement verification corresponds to checking the existence of some paths. Moreover, if A is not provable then a countermodel can be directly extracted from the related dependency graph. Such a graph appears as an essential semantical structure that captures the interactions between additives and multiplicatives inside BI. To have efficient constraint resolution is essential for an effective use of our labelled method and thus we define a variant of it based on free variables in labels and in which we can postpone some variable instantiations until enough information is available. It gives a way to control the introduction of new labels and therefore to limit the syntactic complexity of the labels. But, as a consequence, the construction of countermodels becomes more difficult. As BI is conservative over IL and MILL [29], we have defined new labelled calculi for both logics, by some restrictions of the TBI^{⊥} calculus. Compared with other proof-search methods, these new methods for these logics provide efficient proof-search with an easy and direct generation of countermodels. Our results could be related to the Labelled Deductive Systems (LDS) methodology [10] where the deductive process manipulates labelled formulas and inference rules simultaneously act on formulas and labels. This approach has been used in order to build uniform deductive systems for a wide range of substructural logics [5, 7]. From a set of labelled rules, that is the same for all the logics under consideration, the provability in each logic is analyzed through specific label constraints. The common idea with our approach is to capture the semantics through labels and to analyze provability through constraint satisfaction, but, in our work, we deal with a specialized, and not uniform, deductive system and with particular constraints (assertions and requirements) on labels, that are generated during the tableau construction. Moreover, the closure conditions involve specific constraints and are not instantiations of some more uniform constraints. Our way for defining and managing labels and constraints is strongly related to the resource semantics of BI. Further work will be devoted to the study of such relationships in order to determine if and how similar labelled calculi could be define for logics with well-defined resource semantics.

1BI^{⊥}denotes the BI logic without ⊥, that is the unit of the additive disjunction ∨.

In section 2, we present BI with its basic proof-theory and Kripke resource semantics. The completeness w.r.t. this semantics only holds for BI^{⊥} (BI without ⊥) [34] and consequently we first deal with this fragment. In section 3, we introduce the labelled tableau calculus TBI^{⊥} with appropriate definitions of labels, labelled formulas and constraints. We define expansion rules that include the generation of two kinds of constraints called assertions and requirements. The closure condition of a labelled tableau is defined through a particular notion of complementarity and the satisfaction of requirements from the assertions. Examples illustrate the construction of labelled tableaux with constraints for BI^{⊥} and its underlying problems. In section 4, we show the main properties of the TBI^{⊥} calculus that are soundness and completeness w.r.t. the Kripke resource semantics. In order to prove completeness we introduce the notion of completed branch, show how to construct a countermodel from such a branch [30] and give a tableau construction procedure that provides either a closed tableau or a tableau with a completed branch. Moreover, we prove the finite model property w.r.t. the Kripke semantics from the introduction of the notions of liberalized expansion rules and branch redundancy. As a consequence, we show the decidability of BI^{⊥}. In section 5, we introduce the notion of dependency graph that represents the set of assertions introduced during the tableau construction. Then, the verification of requirements corresponds to the search of specific paths in such a graph. It is an essential semantical structure from which we can deduce the provability of a formula or its non-provability with the extraction of a Kripke resource countermodel following the steps of the completeness proof. In section 6, we give a free variable version of the TBI^{⊥} calculus and illustrate with examples its interest for proof-search in comparison with the initial calculus. It allows to strongly reduce the non-determinism in the choice of the labels satisfying the requirements and then to improve the efficiency of the proof-search but the construction of countermodels is more difficult. In sections 7 and 8, taking into account the conservativity theorem of BI, we restrict the TBI^{⊥} calculus respectively to IL and MILL in order to obtain, for each logic, a new tableau method based on labels and constraints with an easy generation of countermodels as a main characteristic. In section 9, we present some conclusions and perspectives.

2 The Bunched Implications Logic (BI)

In this section, we recall the essential features of the propositional logic of Bunched Implications (BI) [34], in which additive (intuitionistic) and multiplicative (linear) connectives cohabit. Such a logic requires that the antecedents of logical consequences are structured not as lists but rather as bunches.

2.1 Syntax and Proof-Theory of BI

Definition 2.1 (propositions). The propositional language of BI consists of: a multiplicative unit I, the multiplicative connectives ∗, −∗, the additive units ⊤, ⊥, the additive connectives ∧, →, ∨, a countable set L = p, q, … of propositional letters. P(L), the collection of BI propositions over L, is given by the following inductive definition: A ::= p | I | A ∗ A | A −∗ A | ⊤ | ⊥ | A ∧ A | A → A | A ∨ A.

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

Definition 2.2 (bunches). Bunches are inductively defined as follows: Γ ::= A | ∅_{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) commutative monoid equations for ∅_{m} and “,” and c) congruence: Δ ≡ Δ′ implies Γ(Δ) ≡ Γ(Δ′). Let us note that “;” and “,” do not distribute over one another. Judgements are expressions of the form Γ ⊢ A, where Γ is a “bunch” and A is a proposition. The LBI sequent calculus is given in figure 1. It has the cut-elimination property and there exists an equivalent sequent calculus with the following additive rules that are derivable in the LBI calculus.

\begin{aligned}& ax \\ Γ; A ⊢ A \end{aligned}

\begin{aligned}Γ ⊢ A & Γ ⊢ B \\ & ∧_{R} \\ Γ ⊢ A ∧ B \end{aligned}

Γ ⊢ A Δ(Γ; B) ⊢ C
→_{L}
Δ(Γ; A → B) ⊢ C

Γ(A) ⊢ C Γ(B) ⊢ C
∨_{L}
Γ(A ∨ B) ⊢ C

As an example, we give a proof in LBI of the sequent p ∗ (q ∧ r) ⊢ (p ∗ q) ∧ (p ∗ r).

p ⊢ p \begin{aligned}q; r ⊢ q \\ & ∧_{L} \\ q ∧ r ⊢ q \end{aligned}
∗_{R}
p ∗ (q ∧ r) ⊢ p ∗ q

p ⊢ p \begin{aligned}q; r ⊢ r \\ & ∧_{L} \\ q ∧ r ⊢ r \end{aligned}
∗_{R}
p ∗ (q ∧ r) ⊢ p ∗ r
∧_{R}
p ∗ (q ∧ r) ⊢ (p ∗ q) ∧ (p ∗ r)

A proposition A is a theorem if ∅_{a} ⊢ A or ∅_{m} ⊢ A is provable in LBI [29]. But the following theorem provides a more simple definition.

Theorem 2.1. ∅_{a} ⊢ A (resp. ∅_{m} ⊢ A) is provable in LBI iff ⊤ ⊢ A (resp. I ⊢ A) is provable in LBI.

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

It is important to mention the following results about conservativity over IL and MILL.

– 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}

– Units

\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

Γ(A, B) ⊢ C ; ∗_{L} ; Γ(A ∗ B) ⊢ C Γ ⊢ A Δ ⊢ B ∗_{R}

Γ, Δ ⊢ A ∗ B

Γ ⊢ A Δ(Δ′, B) ⊢ C
−∗_{L}
Δ(Δ′, Γ, A −∗ B) ⊢ C

\begin{matrix}Γ, A ⊢ B \\ −∗ & R \\ Γ ⊢ A −∗ B \end{matrix}

– Additives

Γ(A; B) ⊢ C ; ∧_{L} ; Γ(A ∧ B) ⊢ C Γ ⊢ A Δ ⊢ B

∧_{R}
Γ; Δ ⊢ A ∧ B

Γ ⊢ A Δ(Δ′; B) ⊢ C →_{L}
Δ(Δ′; Γ; A → B) ⊢ C

\begin{aligned}Γ; A ⊢ B \\ & →_{R} \\ Γ ⊢ A → B \end{aligned}

Γ(A) ⊢ C Δ(B) ⊢ C
∨_{L}
Γ(A ∨ B); Δ(A ∨ B) ⊢ C

\begin{aligned}Γ ⊢ A_{i (i=1,2)} \\ & ∨_{Ri} \\ Γ ⊢ A_{1} ∨ A_{2} \end{aligned}

Figure 1: The LBI sequent calculus

Theorem 2.2 (conservativity). BI is conservative over IL, that is, A_{1}; …; A_{n} ⊢ B is provable in LBI iff A_{1}, …, A_{n} ⊢ B is provable in IL, where the A_{i} and B are propositions built up using additive connectives only. BI is conservative over MILL, that is, A_{1}, …, A_{n} ⊢ B is provable in LBI iff A_{1}, …, A_{n} ⊢ B is provable in MILL, where the A_{i} and B are propositions built up using multiplicative connectives only and these ones are replaced by the corresponding connectives in MILL.

Let us remark that the conservativity does not extend to MAILL (MILL extended with additive connectives) that does not admit distribution, namely A ∧ (B ∨ C) ⊢ (A ∧ B) ∨ (A ∧ C) and its converse whereas BI admits it. All these results are developed and proved in [29, 35].

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 formulas) which combines the Kripke semantics of IL and Urquhart’s semantics of MILL [29] that deals with possible worlds, arranged as a commutative monoid and justified in terms of “pieces of information” [37]. Here, we consider such a semantics that provides a way to read the formulas 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.3. A Kripke resource monoid (KRM) M = ⟨ M, ⊑, •, e ⟩ is a preordered commutative monoid in which • is order preserving, i.e., (P) m ⊑ n and m′ ⊑ n′ imply m • m′ ⊑ n • n′.

Definition 2.4. Let M be a KRM and P(L) be the collection of BI propositions over a language L of propositional letters, then an elementary Kripke interpretation (EKI) is a function ⟦– ⟧ : L → P(M) that satisfies: (K) for any m, n ∈ M such that m ⊑ n, m ∈ ⟦p⟧ implies n ∈ ⟦p⟧.

Definition 2.5. An elementary Kripke model (EKM), is a triple K = ⟨ M, ⊧, ⟦– ⟧ ⟩ in which M is a KRM, ⟦– ⟧ is an EKI and ⊧ is a forcing relation on M × P(L) satisfying the following conditions:

– m ⊧ p iff m ∈ ⟦p⟧

– m ⊧ ⊤ iff always

– m ⊧ ⊥ iff never

– m ⊧ A ∧ B iff m ⊧ A and m ⊧ B

– 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 semantics of propositions given by the relation ⊧ is parametrized by the interpretation ⟦–⟧ for which the property (K) of definition 2.4 holds for atomic propositions. It is easy to prove, by structural induction on propositions, that if (K) holds for atomic propositions, then it also holds for any proposition. These semantic 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. On the other hand, 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 [29]. From this resource-based interpretation of BI, it is important to notice that BI is different from Linear Logic (LL) and does not admit its standard number-of-uses reading [19]. For instance, A −∗ B ⊢ A → B does not hold in BI, whereas A −∘ B ⊢ A → B holds in LL, in which A → B is defined as !A −∘ B. On the other hand, ⊢ A −∗ (A → A → B) → B holds in BI but not in LL because it does not respect the number-of-uses reading.

There is a recent interest in so-called resource-sensitive logics like linear logic [19] but in BI one does not regard a proposition as a resource and thus a proof as a way to manipulate resources. The reading is declarative: a proposition is a statement about the world the judgement of truth of which may involve consideration of resources. It may be seen most clearly through the term models required for the various completeness proofs and also in the sharing interpretation [35]. There are promising results about logic programming [2], interference in imperative programs [27] and reasoning about mutable data structures like pointers [20]. 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 the resources have been defined 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 [20] deals with atomic propositions 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 whose content is 3, 5 and such that, when updating the cons cell to 7, 5, the resulting heap satisfies 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 [20]. In order to prove such formulas, assertions or properties expressed in BI, it seems important to design proof-search methods for this logic that build proofs but also generate countermodels.

Definition 2.6. Let K be a EKM and Φ_{Γ} be the formula obtained from a bunch Γ by replacing each “;” by ∧ and each “,” by ∗ with association respecting the tree structure of Γ, the sequent Γ ⊢ A is said to be valid in K (notation: Γ ⊧_{K} A), if and only if, for any world m ∈ M, m ⊧ Φ_{Γ} implies m ⊧ A. The sequent Γ ⊢ A is said to be valid (notation: Γ ⊧ A), if and only if, for any EKM K, Γ ⊧_{K} A.

Theorem 2.3 (soundness). If Γ ⊢ A is provable in LBI, then Γ ⊧ A.

The unit ⊥ of the ∨ connective internalizes inconsistency in BI and the Kripke resource semantics does not account for inconsistency (⊥ is nowhere forced). Accordingly, ⊥ has to be excluded for completeness [35] and then the completeness result w.r.t. this semantics only holds for BI^{⊥} (BI without ⊥) [29].

Theorem 2.4 (completeness). If Γ ⊧ A in BI^{⊥} then Γ ⊢ A is provable in LBI^{⊥}.

Corollary 2.2. A proposition A is valid iff for any EKM K, e ⊧_{K} A.

Our goal is to define a labelled tableau method, the labels allowing to incorporate information about semantics into the syntax. In this context, the Kripke resource semantics seems to be a good starting point to define labels and labelled calculi dedicated to efficient and understandable proof-search methods. As we aim to design them from so-called completeness proofs by proof-search [30], we consider at first BI^{⊥} hoping that we could adapt our methodology and results to BI (with ⊥). Topological Kripke models and also Grothendieck Sheaf-theoretic models have been proposed as semantics to have completeness for BI [35].

3 A Labelled Tableaux Calculus for BI^{⊥}

Because of the cohabitation of multiplicative (linear) and additive (intuitionistic) connectives in BI and even if it includes IL and MILL as subsystems, we cannot directly extend proof-search (sequent, tableau, or connection) calculi defined for both sublogics to BI [3, 11, 13, 36]. We introduce labels and labelled formulas in a specific way compared to the general LDS approach of [10] in order to define a labelled tableau calculus TBI^{⊥}, for propositional BI^{⊥}, with generation of countermodels. Let us start defining this particular set of labels and constraints.

3.1 Labelled Tableaux

Definition 3.1. A labelling language consists of the following symbols: a unit symbol 1, a binary function symbol ∘, a binary relation symbol ≤, a countable set of constants c_{1}, c_{2}, … Labels are inductively defined from the unit 1 and the constants as expressions of the form x ∘ y in which x and y are labels. Atomic labels are labels which do not contain any ∘, while compound labels contain at least one ∘. Label constraints are expressions of the form x ≤ y with x and y being labels.

In order to simplify notations, we can omit the binary symbol ∘ when we write labels. Like in the LDS approach the basic units of the deductive process are labelled formulas with labels in a given labelling algebra [7]. The expansion rules act on the labels as well as on the formulas. In this context, 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(L)) and l (∈ L) being its label. A TBI^{⊥} tableau is a rooted tree, with nodes labelled with a signed formula, that is built according to the expansion rules of figure 2. The rules of the first line are the classical α and β rules, like in standard tableau methods [9]. The rules of the second line (called πα rules) are such that the labels c_{i} and c_{j} are new constants and the label constraints are called assertions. Let us note that we assume the implicit assertion c_{i} ≤ c_{i} for the F −∗ rule (not depicted on figure 2 for conciseness). The rules of the third line (called πβ rules) are such that the labels y and z only contain constants that exist at the moment of the expansion and the constraints are called requirements. For example, in the case of A ∗ B, we have the two following rules:

T A ∗ B : x ; ass : c_{i}c_{j} ≤ x ; \begin{matrix}T A : c_{i} \\ T B : c_{j} \end{matrix}  F A ∗ B : x ; req : yz ≤ x ; F A : y  F B : z

Both rules introduce constraints on the labels. The first one introduces the new constants c_{i} and c_{j} and an assertion c_{i}c_{j} ≤ x. The second one introduces the labels y and z and a requirement yz ≤ x. We have distinguished two kinds of constraints: the assertions and the requirements. In the proof-search process, the former will behave as known facts (or hypotheses) and the latter will express goals that must

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

F A → B : x ; ass : x ≤ c_{i} ^{∗} ; \begin{matrix}T A : c_{i} \\ F B : c_{i} \end{matrix}  T A ∗ B : x ; ass : c_{i}c_{j} ≤ x ^{∗} ; \begin{matrix}T A : c_{i} \\ T B : c_{j} \end{matrix}  F A −∗ B : x ; \begin{matrix}T A : c_{i} ^{∗} \\ F B : xc_{i} \end{matrix}

T A → B : x ; req : x ≤ y ; F A : y  T B : y  F A ∗ B : x ; req : yz ≤ x ; F A : y  F B : z  \begin{matrix}T A −∗ B : x \\ F A : y & T B : xy \end{matrix}

∗ c_{i}, c_{j} are new constants

Figure 2: Expansion Rules for BI^{⊥}

be satisfied from the assertions. Since there may be several labels satisfying a given requirement, the πβ rules are different from the πα rules because they can be expanded several times during a tableau expansion, much like the γ rules in the first order classical tableau method [9]. A key point is that the labels and constraints introduced in this labelled tableau calculus are interpreted in a labelling algebra.

Definition 3.2. Labels and constraints are interpreted onto a labelling algebra L = ⟨ L, ≤, ∘, 1 ⟩, which is an order-preserving preordered commutative monoid of labels, more precisely:

1. L is a set of labels

2. ≤ is a preordering

3. equality on labels is defined by : x = y iff x ≤ y and y ≤ x

4. ∘ is a binary operation on L that satisfies:

- associativity: (x ∘ y) ∘ z = x ∘ (y ∘ z)

- commutativity: x ∘ y = y ∘ x

- identity: x ∘ 1 = 1 ∘ x = x

- compatibility: x ≤ y implies x ∘ z ≤ y ∘ z

We say that 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.

Let us remark that our labelling algebra is a free monoid of labels and, consequently, it generates an infinity of labels. Indeed, once you have a constant c_{1}, you also have c_{1}c_{1}, c_{1}c_{1}c_{1} and so on. Nevertheless, the whole free monoid is often useless for verifying whether some constraints hold with respect to a given labelling algebra. This point can be justified if we consider labels as resources and formulas as statements about resources. Then, in many cases, formulas only express something about a (finite) subset of the resources. Therefore, we deal with partially defined labelling algebras which are obtained from sets of constraints by means of a specific closure operator.

Definition 3.3. The domain of a set K of label constraints is the set of all sublabels occurring in some constraint of K, i.e., D(K) = ⋃_{x≤y∈K}(P(x) ∪ P(y)). The closure \overline{K} of K is defined as follows:

1. K ⊆ \overline{K}

2. if x ∈ D(\overline{K}) then x ≤ x ∈ \overline{K} (reflexivity)

3. if x ≤ y ∈ \overline{K} and y ≤ z ∈ \overline{K} then x ≤ z ∈ \overline{K} (transitivity)

4. if y ∘ z ∈ D(\overline{K}) then x ≤ y ∈ \overline{K} implies x ∘ z ≤ y ∘ z ∈ \overline{K} (compatibility)

Any set K of constraints gives rise to a particular preordering relation and thus to a particular labelling algebra in which the constraints of K are taken as axioms. Since the two notions are closely related, we do not distinguish between the closure of a set of constraints and the (partially defined) labelling algebra it generates. Let us remark that each πβ rule admits a trivially satisfied requirement w.r.t. the underlying labelling algebra, namely, x ≤ x for T → and 1 ∘ x ≤ x for F ∗ and T −∗. Therefore, a πβ formula can always be expanded at least once. Moreover, since ∘ is assumed to be commutative, if y and z are labels such that yz ≤ x then the two following expansions are allowed for the formula F A ∗ B : x:

F A ∗ B : x ; req : yz ≤ x ; F A : y  F B : z  F A ∗ B : x ; req : zy ≤ x ; F A : z  F B : y

Moreover, each πα rule admits a special case when the multiplicative unit I is concerned:

T A ∗ I : x ; \begin{matrix}T I : 1 \\ T A : x \end{matrix}  T I ∗ A : x ; \begin{matrix}T I : 1 \\ T A : x \end{matrix}  F I −∗ A : x ; \begin{matrix}T I : 1 \\ F A : x \end{matrix}  F I → A : x ; ass : x, 1 ≤ c_{i} ; \begin{matrix}T I : c_{i} \\ F A : c_{i} \end{matrix}

The rules for T ∗ and F −∗ introduce neither new constants nor new assertions and correspond to the equivalences I ∗ A ⊣⊢ A ∗ I ⊣⊢ A and I −∗ A ⊣⊢ A in LBI. In the case of F I → A : x, a new assertion 1 ≤ c_{i}, reflecting on c_{i} the semantical satisfaction condition for I, is required in addition to the usual assertion x ≤ c_{i}. We now introduce useful notations before we define what a closed labelled tableau is. Given a branch B, we write F(B) to denote the set of its signed-formulas, Ass(B) to denote the set of its assertions and Req(B) to denote the set of its requirements. We define the domain D(B) of B as the set D(Ass(B)). Finally, C(B) is the set D(B) restricted to the constants. We can now proceed with the notion of closed tableau.

Definition 3.4. Let A be a proposition of BI^{⊥}, a tableau sequence for A is a sequence of tableaux t_{1}, t_{2}, … for which t_{1} is the one-node tree defined by F(t_{1}) = { F A : 1 }, Ass(t_{1}) = { 1 ≤ 1 }, Req(t_{1}) = ∅ and t_{i+1} is obtained from t_{i} by the application of an expansion rule of figure 2 (on a branch of t_{i}).

Definition 3.5. Let B be a tableau branch, the two signed formulas T A : x and F A : y of F(B) are complementary in B if and only if x ≤ y ∈ \overline{Ass}(B), i.e., if the constraint x ≤ y belongs to the reflexive, transitive and compatible closure of Ass(B).

Definition 3.6. A tableau t is closed if, for all its branches B,

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

Finally, let us mention that a branch can be represented as a flat structure ⟨ F(B), Ass(B), Req(B) ⟩ for which the expansion rules are easily adapted. For example, the rule for T A ∗ B : x becomes the following:

⟨ F(B) = { ..., T A ∗ B : x, ... }, Ass(B), Req(B) ⟩ c_{i}, c_{j} ∉ D(B)

T ∗ ⟨ F(B) ∪ { T A : c_{i}, T B : c_{j} }, Ass(B) ∪ { c_{i}c_{j} ≤ x }, Req(B) ⟩

Such a representation will prove useful later, when we discuss dependency graphs.

3.2 Examples

Let us illustrate the tableau method with some examples. For a better understanding of how the expansion process works, we have annotated the signed formulas with a check-symbol (√_{i}) that indicates the step i at which it has been expanded (or a list of steps if the formula has been expanded more than once). Please note that, in order to build a closed tableau sequence, we expand the formulas which introduce new constants before expanding those which reuse existing labels. We also indicate closed branches by ending them with a cross-symbol (×).

√_{1} F ((p ∗ (q −∗ r)) ∗ s) −∗ (p ∗ ((q −∗ r) ∗ s)) : 1
√_{2} T (p ∗ (q −∗ r)) ∗ s : c_{1}
√_{4} F p ∗ ((q −∗ r) ∗ s) : c_{1}

ass_{1} : c_{2}c_{3} ≤ c_{1}

\begin{matrix}√_{3} T p ∗ (q −∗ r) : c_{2} \\ T s : c_{3} \end{matrix}

ass_{2} : c_{4}c_{5} ≤ c_{2}

\begin{matrix}T p : c_{4} \\ T q −∗ r : c_{5} \end{matrix}

req_{1} : c_{3}c_{4}c_{5} ≤ c_{1}

F p : c_{4} × √_{5} F (q −∗ r) ∗ s : c_{3}c_{5}

req_{2} : c_{3}c_{5} ≤ c_{3}c_{5} ; \begin{matrix}F q −∗ r : c_{5} \\ × \end{matrix} \begin{matrix}F s : c_{3} \\ × \end{matrix}

Figure 3: Labelled Tableau for ((p ∗ (q −∗ r)) ∗ s) −∗ (p ∗ ((q −∗ r) ∗ s))

Let us consider the tableau of figure 3, we observe that we have complementary formulas in each branch: p with c_{4}, q −∗ r with c_{5} and s with c_{3}. Moreover we have two assertions, namely, ass_{1} : c_{2}c_{3} ≤ c_{1} and ass_{2} : c_{4}c_{5} ≤ c_{2}, and two requirements, namely, req_{1} : c_{3}c_{4}c_{5} ≤ c_{1} and req_{2} : c_{3}c_{5} ≤ c_{3}c_{5} that have to be satisfied from the assertions. These requirements are satisfied and thus all the branches are closed. In fact, the requirement req_{2} : c_{3}c_{5} ≤ c_{3}c_{5} is directly satisfied. From ass_{2} : c_{4}c_{5} ≤ c_{2} we can deduce by the compatibility property that we have the assertion c_{3}c_{4}c_{5} ≤ c_{3}c_{2} and with ass_{1} : c_{2}c_{3} ≤ c_{1} we deduce by transitivity that the requirement req_{1} : c_{3}c_{4}c_{5} ≤ c_{1} is also satisfied. Let us now consider the non-closed tableau of figure 4. In order to build it, we begin the expansion with the initial multiplicative −∗, producing two new formulas T (p ∗ q) ∧ (p ∗ r) : c_{1} and F p ∗ (q ∧ r) : c_{1}. Step 2 deals with the additive ∧, yielding two multiplicatives: T p ∗ q : c_{1} and T p ∗ r : c_{1}. The expansion of the first T ∗ rule in step 3 introduces two new constants c_{2}, c_{3} and the assertion ass_{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 ass_{2} : c_{4}c_{5} ≤ c_{1}. We are now left with the remaining πβ formula. To expand it, we must match a requirement and thus find a compound label yz such that yz ≤ 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 tried to achieve a completed tableau. Step 5 therefore goes on with the first one, namely, req_{1} : c_{2}c_{3} ≤ c_{1},

√_{1} F ((p ∗ q) ∧ (p ∗ r)) −∗ (p ∗ (q ∧ r)) : 1

√_{2} T (p ∗ q) ∧ (p ∗ r) : c_{1} √_{5,7} F p ∗ (q ∧ r) : c_{1}

\begin{matrix}√_{3} T p ∗ q : c_{1} \\ √_{4} T p ∗ r : c_{1} \end{matrix}

ass_{1} : c_{2}c_{3} ≤ c_{1}

\begin{matrix}T p : c_{2} \\ T q : c_{3} \end{matrix}

ass_{2} : c_{4}c_{5} ≤ c_{1}

\begin{matrix}T p : c_{4} \\ T r : c_{5} \end{matrix}

req_{1} : c_{2}c_{3} ≤ c_{1}

F p : c_{2} × √_{6} F q ∧ r : c_{3}

F q : c_{3} × F r : c_{3}

req_{2} : c_{4}c_{5} ≤ c_{1}

\begin{matrix}F p : c_{4} \\ × \end{matrix} \begin{matrix}√_{8} F q ∧ r : c_{5} \\ F q : c_{5} & \begin{matrix}F r : c_{5} \\ × \end{matrix} \end{matrix}

Figure 4: Labelled Tableau for ((p ∗ q) ∧ (p ∗ r)) −∗ (p ∗ (q ∧ r))

splitting the tableau into two new branches. The first branch is immediately closed since it contains both T p : c_{2} and F p : c_{2} and c_{2} ≤ c_{2} is trivially satisfied. The second branch yields an additive conjunction which is immediately expanded in step 6 and we have two new branches. Once again, the first branch is closed since it contains ⟨ T q : c_{3}, F q : c_{3} ⟩. The second branch contains a potential connection ⟨ T r : c_{5}, F r : c_{3} ⟩ but there is no way to show c_{5} ≤ c_{3} from the closure of the assertions in the branch. After step 6, there are no more α or πα formulas to expand. However, the tableau is not yet completed (see definition 4.3) because we have not tested the second possibility for the πβ formula, that is, y = c_{4} and z = c_{5}. Step 7 therefore 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} is replaced by c_{4} and c_{3} is replaced by c_{5}. We obtain two more closed branches, one with ⟨ T p : c_{4}, F p : c_{4} ⟩ and another one with ⟨ T r : c_{5}, F r : c_{5} ⟩. Thus, all formulas have been fulfilled and we notice that the fourth branch of the tree is not closed. Indeed, we have two potential connections ⟨ T q : c_{3}, F q : c_{5} ⟩ and ⟨ T r : c_{5}, F r : c_{3} ⟩, but neither c_{3} ≤ c_{5} nor c_{5} ≤ c_{3} can be deduced from the closure of the assertions available in the branch.

4 Properties of the TBI^{⊥} calculus

In this section, we show the soundness and completeness of the TBI^{⊥} calculus w.r.t. the Kripke resource semantics. This deductive system allows not only to build a proof but also a countermodel in case of non-provability.

4.1 Soundness

Definition 4.1. Let K = ⟨ M, ⊧, ⟦– ⟧ ⟩ be a EKM and B be a tableau branch, a realization of B in K is a mapping ∥– ∥ : D(B) → M, from the domain of B to the worlds of M, that satisfies

1. ∥1∥ = e,

2. ∥x ∘ y∥ = ∥x∥ • ∥y∥,

3. for any signed formula T A : x in B, ∥x∥ ⊧ A,

4. for any signed formula F A : x in B, ∥x∥ |̸= A,

5. for any assertion x ≤ y in Ass(B), ∥x∥ ⊑ ∥y∥ holds in K.

Let us note that ∥–∥ is completely defined by its values on the constants of B. Moreover, we have the following lemma, which states that the last condition extends to the closure of the assertions.

Lemma 4.1. Let t be a tableau, B be a branch of t and ∥– ∥ be a realization of B in some EKM K, for any x ≤ y ∈ \overline{Ass}(B), ∥x∥ ⊑ ∥y∥ holds in K.

Proof. Straightforward since • is compatible w.r.t. ⊑ in K and any assertion x ≤ y in \overline{Ass}(B) derives, by compatibility of ∘ w.r.t. ≤, from assertions of Ass(B) the realization of which holds in K by definition.

Definition 4.2. A tableau branch B is realizable if there exists a realization of B in some EKM. A tableau t is realizable if it contains a realizable branch.

Lemma 4.2. A closed tableau cannot be realizable.

Proof. Let t be a closed tableau that is also realizable. It contains a branch B which is realizable in some EKM for some realization ∥–∥. We now proceed by case analysis on the closure of the branch.

– if the branch is closed due to complementary formulas ⟨ T A : x, F A : y ⟩, then, by definition, we have x ≤ y ∈ \overline{Ass}(B) which, by lemma 4.1, implies ∥x∥ ⊑ ∥y∥. But, since ∥–∥ realizes B, we have ∥x∥ ⊧ A and ∥y∥ |̸= A. Then, we have a contradiction because, by property (K), we should have ∥y∥ ⊧ A.

– other cases are similar.

Lemma 4.3. If t′ is a tableau obtained from a tableau t by application of an expansion rule of figure 2, then, if t is realizable, t′ is also realizable.

Proof. Since t is realizable, it contains a branch B which is realizable in some EKM for some realization ∥–∥. If the signed formula Sg X : x that has been expanded to obtain t′ does not belong to B, then t′ is realizable since it still contains B. Otherwise, we show by case analysis on Sg X : x that the corresponding expansion rule preserves realizability.

– case T A ∗ B : x B is expanded into B′ with F(B′) = F(B) ∪ { T A : c_{i}, T B : c_{j} } and Ass(B′) = Ass(B) ∪ { c_{i}c_{j} ≤ x }, c_{i} and c_{j} being new constants. Since ∥–∥ realizes B, we have ∥x∥ ⊧ A ∗ B. Therefore, there exist m, n ∈ M such that m • n ⊑ ∥x∥, m ⊧ A and n ⊧ B. We simply extend ∥–∥ to c_{i}, c_{j} by setting ∥c_{i}∥ = m and ∥c_{j}∥ = n. Thus, we obtain ∥c_{i}∥ ⊧ A and ∥c_{j}∥ ⊧ B. Since ∥c_{i}∥ • ∥c_{j}∥ ⊑ ∥x∥, B′ is realizable and, consequently, t′ is realizable.

– case F A ∗ B : x B splits into B′ and B′′ such that F(B′) = F(B) ∪ { F A : y }, F(B′′) = F(B) ∪ { F B : z } and Req(B′) = Req(B′′) = Req(B) ∪ { yz ≤ x }. A valid application of the F ∗ rule requires that yz ≤ x should be in \overline{Ass}(B). Thus, lemma 4.1 implies ∥y∥ • ∥z∥ ⊑ ∥x∥. Since ∥–∥ realizes B, we have ∥x∥ |̸= A ∗ B. Therefore, for any m, n ∈ M such that m • n ⊑ ∥x∥, either m |̸= A, or n |̸= B, which implies that either ∥y∥ |̸= A, or ∥z∥ |̸= B. Then, either B′, or B′′ is realizable and, consequently, t′ is realizable.

– other cases are similar.

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

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

Proof. Let T = t_{1}, …, t_{n} be a closed tableau sequence and suppose that A does not hold in Kripke resource semantics, then, by corollary 2.2, there exists an EKM such that e |̸= A. Thus, the initial tableau t_{1} is trivially realizable and lemma 4.3 entails that all t_{i} such that i > 1 are also realizable. It follows from lemma 4.2 that none of the t_{i} can be closed and, consequently, T cannot be closed, which is a contradiction.

4.2 Completeness and Countermodel Construction

In this subsection we prove the completeness of the tableau system w.r.t. the Kripke resource semantics. For that, we first introduce the notion of completed branch [7] and then show the model existence lemma, i.e., how to construct a Kripke resource model from such a branch. We conclude the section by giving a tableau construction procedure which, for any given formula, produces either a closed tableau for it, or a tableau that contains a completed branch, thereby proving completeness.

Definition 4.3. Let B be a tableau branch, a signed formula Sg X : x is fulfilled (or completely analyzed) in B, noted B ⊩ Sg X : x, if it satisfies one of the following conditions

1. B ⊩ F ⊤ : x

2. B ⊩ F I : x iff 1 ≤ x ∉ \overline{Ass}(B)

3. B ⊩ F p : x iff there exists F p : y ∈ B such that x ≤ y ∈ \overline{Ass}(B)

4. B ⊩ F A ∧ B : x iff either B ⊩ F A : x or B ⊩ F B : x

5. B ⊩ F A ∨ B : x iff both B ⊩ F A : x and B ⊩ F B : x

6. B ⊩ F A → B : x iff there exists y ∈ D(B) such that x ≤ y ∈ \overline{Ass}(B) and both B ⊩ T A : y and B ⊩ F B : y

7. B ⊩ F A ∗ B : x iff for any y, z ∈ D(B) such that yz ≤ x ∈ \overline{Ass}(B) either B ⊩ F A : y, or B ⊩ F B : z 8. B ⊩ F A −∗ B : x iff there exist y, xy ∈ D(B) such that both B ⊩ T A : y and B ⊩ F B : xy

9. B ⊩ T ⊤ : x

10. B ⊩ T I : x iff 1 ≤ x ∈ \overline{Ass}(B)

11. B ⊩ T p : x iff there exists T p : y ∈ B such that y ≤ x ∈ \overline{Ass}(B)

12. B ⊩ T A ∧ B : x iff both B ⊩ T A : x and B ⊩ T B : x

13. B ⊩ T A ∨ B : x iff either B ⊩ T A : x, or B ⊩ T B : x

14. B ⊩ T A → B : x iff for any y ∈ D(B) such that x ≤ y ∈ \overline{Ass}(B) either B ⊩ F A : y, or B ⊩ T B : y 15. B ⊩ T A ∗ B : x iff there exist y, z ∈ D(B) such that yz ≤ x ∈ \overline{Ass}(B) and both B ⊩ T A : y and

B ⊩ T B : z

16. B ⊩ T A −∗ B : x iff for any y, xy ∈ D(B) either B ⊩ F A : y, or B ⊩ T B : xy

Definition 4.4. A tableau branch B is completed if it is open and every signed formula Sg A : x in it is fulfilled. A tableau is completed if it has a completed branch.

Lemma 4.4 (monotonicity). A completed branch B satisfies Kripke monotonicity, more precisely,

1) B ⊩ F A : x and y ≤ x ∈ \overline{Ass}(B) imply B ⊩ F A : y, and 2) B ⊩ T A : x and x ≤ y ∈ \overline{Ass}(B) imply B ⊩ T A : y.

Proof. By structural induction on Sg X : x.

Lemma 4.5 (consistency). If B is a completed branch, then, for any BI proposition A, we cannot have both B ⊩ T A : x and B ⊩ F A : x.

Proof. Let us suppose that both B ⊩ T p : x and B ⊩ F p : x. Then, T p : y ∈ B for some y such that y ≤ x ∈ \overline{Ass}(B) and F p : z ∈ B for some z such that x ≤ z ∈ \overline{Ass}(B). Therefore, by transitivity, we have y ≤ z ∈ \overline{Ass}(B), which implies that B is closed. It is a contradiction with the definition of a completed branch. The property can be easily extended to non-atomic propositions by structural induction.

4.2.1 Countermodel Construction

Countermodel generation is important in automated reasoning because a countermodel gives information about the non-provability of a formula. In this subsection, we explain how to build a countermodel of A from a completed branch in a labelled tableau of A.

Definition 4.5. Let B be a completed branch, the M-structure M(B) = ⟨ M, ⊑, •, 1 ⟩ is defined as follows i) M is the set D(B), extended with a particular element denoted by π ii) • is a composition law defined by

x • 1 = 1 • x = x
x • y = y • x = xy  if xy ∈ M
x • y = y • x = π  otherwise

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

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

Lemma 4.6. Let B be a completed branch, M(B) = ⟨ M, ⊑, •, 1 ⟩ is a Kripke resource monoid.

Proof. By definition, we have identity w.r.t. 1 and commutativity of •. It is routine to show that • is also associative. Moreover, we can deduce from the closure operations performed on the assertions that • is compatible w.r.t. ⊑.

Definition 4.6. Let M(B) = ⟨ M, ⊑, •, 1 ⟩ be the M-structure of a completed branch B and P(L) denote the collection of BI propositions over a language L of propositional letters. We define the interpretation ⟦– ⟧_{B} : L → P(M) for any atomic proposition p by ⟦p⟧_{B} = { π } ∪ { x | B ⊩ T p : x }.

Lemma 4.7 (model existence). If B is a completed branch, then, the triple ⟨ M(B), ⊧, ⟦– ⟧_{B} ⟩ is a Kripke resource model of B, i.e.,

1) ⟦– ⟧_{B} satisfies condition (K) of definition 2.4.

2) For any proposition A, we have a) π ⊧ A,

b) B ⊩ T A : x implies x ⊧ A,

c) B ⊩ F A : x implies x |̸= A.

Proof. 1) Let us suppose x ∈ ⟦p⟧_{B} and x ⊑ y. If y = π, then, π ∈ ⟦p⟧_{B} by definition. If y ≠ π, then, x ⊑ y implies x ≤ y ∈ \overline{Ass}(B) and it follows from lemma 4.4 that B ⊩ T p : y, i.e., y ∈ ⟦p⟧_{B}.

2.a) We proceed by structural induction on A.

– if A ≡ p then, π ⊧ p because π ∈ ⟦p⟧_{B}.

– if A ≡ B ∧ C then, by the induction hypothesis, π ⊧ B and π ⊧ C. Thus, π ⊧ B ∧ C.

– if A ≡ B ∨ C then, by the induction hypothesis, π ⊧ B. Thus, π ⊧ B ∨ C.

– if A ≡ B → C then, by the induction hypothesis, π ⊧ C. Since π is the only x ∈ M such that π ⊑ x, we have π ⊧ B → C.

– if A ≡ B −∗ C then, by the induction hypothesis, π ⊧ C. Since, for any x ∈ M, π • x = π, we have π ⊧ B −∗ C.

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

2.b), 2.c) We proceed by structural induction on Sg A : x.

– if B ⊩ T p : x then, by definition, x ∈ ⟦p⟧_{B}, i.e., x ⊧ p.

– if B ⊩ F p : x then, by lemma 4.5, B ⊮ T p : x. Thus, x ∉ ⟦p⟧_{B}, i.e., x |̸= p.

– if B ⊩ T B ∧ C : x then, both B ⊩ T B : x and B ⊩ T C : x. By the induction hypothesis, we have x ⊧ B and x ⊧ C, i.e., x ⊧ B ∧ C.

– if B ⊩ F B ∧ C : x then, either B ⊩ F B : x or B ⊩ F C : x. By the induction hypothesis, we have x |̸= B or x |̸= C, i.e., x |̸= B ∧ C.

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

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

– if B ⊩ T B → C : x then, for any y in D(B) such that x ≤ y ∈ \overline{Ass}(B), either B ⊩ F B : y or B ⊩ T C : y. By the induction hypothesis, we have either y |̸= B or y ⊧ C for any y ≠ π in M such that x ⊑ y. Since, by 2.a), π ⊧ C, we have x ⊧ B → C.

– if B ⊩ F B → C : x then, there exists y in D(B) such that x ≤ y ∈ \overline{Ass}(B), B ⊩ T B : y and B ⊩ F C : y. By the induction hypothesis, there exists y ∈ M such that x ⊑ y, y ⊧ B and y |̸= C, i.e., x |̸= B → C.

– if B ⊩ T B −∗ C : x then, let y ∈ M. If x • y = xy then, both y and xy are in D(B). Therefore, either B ⊩ F B : y, or B ⊩ T C : xy. By the induction hypothesis, we have either y |̸= B, or x • y ⊧ C. If x • y = π then, by 2.a), we have π ⊧ C. Thus, for any y ∈ M, either y |̸= B or x • y ⊧ C, i.e., x ⊧ B −∗ C.

– if B ⊩ F B −∗ C : x then, there exist y and xy in D(B) such that both B ⊩ T B : y and B ⊩ F C : xy. Since, xy ∈ D(B) implies x • y = xy, it follows from the induction hypothesis that there exists y ∈ M such that y ⊧ B and xy |̸= C, i.e., x |̸= B −∗ C.

– case B ⊩ T B ∗ C : x is similar to case B ⊩ F B −∗ C : x.

– case B ⊩ F B ∗ C : x is similar to case B ⊩ T B −∗ C : x.

We could argue that an interesting model is a model that is minimal in some sense. The study of model generation for substructural logics is recent and the notion of minimality itself is rather difficult to state for models of such logics.

4.2.2 A Tableau Construction Procedure

In the previous section, we have explained how to build a model from a completed branch. To show the completeness theorem, we now need a tableau construction procedure which, given a formula A, builds a tableau sequence t_{1}, t_{2}, … until there exists a tableau t_{i} that is either closed or that contains a (possibly infinite) completed branch. Giving such a procedure is routine and various strategies can be devised concerning the choice of which formula to expand at each step. The only requirement is that the strategy should be fair, that is, it should not run into a loop by always visiting the same subset of formulas while leaving some others unvisited. Let us give such a procedure. The initial signed formula is F A : 1 and it is marked unvisited. Repeat until T is closed or completed

if there is no unvisited formula Sg X : x in any open branch B then mark all πβ-formulas in all open branches as unvisited else mark Sg X : x as visited if Sg X : x is not fulfilled in B then if Sg X : x is of type πβ then expand Sg X : x with a label y for which the formula is not fulfilled else expand Sg X : x according to its type

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

Proof. Suppose there is no closed tableau sequence for A. Then, the above tableau construction procedure yields a tableau in which there is a completed branch B. Since B contains the initial formula F A : 1, lemma 4.7 implies that we can build a model ⟨ M(B), ⊧, ⟦–⟧_{B} ⟩ of B such that 1 |̸= A, which means that A is not valid in the Kripke resource semantics.

4.3 Finite Model Property and Decidability

In this subsection, we discuss the finite model property w.r.t. Kripke resource models and, as a consequence, the decidability of BI^{⊥}. For that, we investigate the situations in which a tableau may have infinite branches. We introduce two central notions which are liberalized expansion rules and branch redundancy. The former provides a way to control the syntactic complexity of the labels by restricting the introduction of new atomic labels during the tableau expansion. The latter characterizes the potential need of an infinite expansion process to achieve a completed branch and can roughly be viewed as a kind of loop-checking.

4.3.1 Liberalized Rules

The rules F →, F −∗ and T ∗ introduce new constants, and then, can lead to infinite branches. Let us consider, for example, the situation depicted in figure 5 for the formula ((q → p) → p) → p. The left-most branch of the tableau infinitely grows because the

√_{1} F ((q → p) → p) → p : 1

ass_{1} : 1 ≤ c_{1}

\begin{matrix}√_{2,4} T (q → p) → p : c_{1} \\ F p : c_{1} \end{matrix}

req_{1} : c_{1} ≤ c_{1}

√_{3} F q → p : c_{1}

ass_{2} : c_{1} ≤ c_{2}

\begin{matrix}T q : c_{2} \\ F p : c_{2} \end{matrix}

req_{2} : c_{2} ≤ c_{2}

√_{5} F q → p : c_{2} ; ass_{3} : c_{2} ≤ c_{3} ; T q : c_{3} ; F p : c_{3} ; ⋮ \begin{matrix}T p : c_{2} \\ × \end{matrix}

T p : c_{1} ×

Figure 5: Infinite Tableau F q → p formulas repeatedly create a new constant for which the parent formula T (q → p) → p must be re-expanded in order to achieve a completed branch. But let us suppose that we could reuse at step 5 the constant c_{2} introduced at step 3 (instead of creating the new constant c_{3}), then, step 5 would simply reintroduce T q : c_{2}, F p : c_{2}, which were already introduced at step 3, and also the trivial assertion c_{2} ≤ c_{2}. Thus, the branch would become completed (and finite) after step 5. The liberalized rules can be justified by the following regularity property (see [7] and also the sections on IL and MILL for more details): whenever there exists a world satisfying a proposition A, there also exists a world, called A-characteristic, which is the least to satisfy A w.r.t. the underlying preordering. Therefore, we can assume that any new constant introduced by an expansion rule refers to a characteristic world. For example, the first time F A −∗ B : x is expanded into T A : a, F B : xa, the new constant a is assumed to refer to an A-characteristic world. Consequently, if we later come across the same formula with a distinct label, e.g., F A −∗ B : y, we can reuse a and produce F B : ya instead of creating a new constant, for this new constant would also refer to an A-characteristic world, and so, be equivalent to a. Let us note that T A : a does not need to be reintroduced since it was already introduced by the expansion of F A −∗ B : x. Moreover, in the case of T A ∗ B : x, both constants a and b can be reused, and so, the expansion of a subsequent T A ∗ B : y only produces a new assertion ab ≤ y since T A : a and T B : b do not need to be reintroduced. With the liberalized rules, only finitely many distinct constants can be introduced in a tableau branch B, which solves the problem of figure 5 and the corresponding (more general) case of a branch containing formulas of the form F C_{k} → D_{k} : y_{k} (1 ≤ k ≤ p) in the scope of formulas of the form T A_{i} → B_{i} : x_{i} (1 ≤ i ≤ n) with, for any i, x_{i} ≤ y_{k} ∈ \overline{Ass}(B) for some k. However, this is not sufficient to prevent infinite branches because, even with a finite number of atomic labels, one can still generate an infinite number of non-atomic labels through composition. In order to ensure finiteness, we need the additional notion of branch redundancy.

4.3.2 Branch Redundancy

Since only finitely many atomic labels can be introduced during the expansion process, the only way for a tableau to grow infinitely is by endlessly producing new compound labels of increasing length. The tableau of figure 6 illustrates such a situation. In this tableau, we can see that step 2 expands the T −∗ formula with the only compound label available at the moment in which a occurs, namely, 1a (= a). Step 3 then expands the T → formula with the same label a since it is the only label which is greater than a, the requirement a ≤ a being trivially satisfied. But, after step 3, a formula F −∗ labelled with a is

√_{1} F (⊤ −∗ ((q −∗ p) → p)) −∗ p : 1

\begin{matrix}√_{2,5} T ⊤ −∗ ((q −∗ p) → p)) : a \\ F p : a \end{matrix}

F ⊤ : 1 × √_{3} T (q −∗ p) → p : a

req_{1} : a ≤ a

√_{4} F q −∗ p : a

\begin{matrix}T q : b \\ F p : ab \end{matrix}

F ⊤ : b × √_{6} T (q −∗ p) → p : ab

req_{2} : ab ≤ ab

√_{7} F q −∗ p : ab ; T q : b ; F p : abb ; ⋮ \begin{matrix}T p : ab \\ × \end{matrix}

T p : a ×

Figure 6: Redundant Tableau introduced in the scope of the T −∗ formula which is also labelled with a. Therefore, the expansion of the F −∗ formula at step 4 now necessarily creates a new compound label ab in which a, the label of the dominating T −∗ formula, occurs as a sublabel. Thus, we are obliged to try a new expansion of the T −∗ formula with the label ab. This is done in step 5, leading to steps 6 and 7 which are similar to step 3 and 4, except for the substitution of the label a by the compound label ab. As expected, step 7 creates the compound label abb in which a also occurs as a sublabel and, once again, we are obliged to try an expansion of the T −∗ formula with the label abb. Thus, we run into a loop F p : ab, F p : abb, F p : abbb, ... which always reproduces the same signed formula F p, but with labels that differ from each other by a single occurrence of the same constant b. The general situation that corresponds to figure 6 is the case of a branch in which some formulas of the form F C −∗ D : y occur in the scope of some formula of the form T A −∗ B : x, with x being a sublabel of y. In the example of figure 6, the addition of the extra assertion bb = b solves the problem since all labels ab^{i} (i ∈ ℕ) involving b more than once collapse (and become equivalent) to ab, making the branch finite and completed right after step 7. In the general case, the loop may reproduce the same subset of formulas, but with labels differing in more than one, though still a fixed number of occurrences of the same constant. Let us suppose for example that p is replaced in figure 6 by the non-atomic formula r ∧ s, then, when we reach the first occurence of F r ∧ s, labelled with ab, we can choose to follow the branch that contains r and, when we later encounter the second occurrence of F r ∧ s, labelled with abb, we can choose to follow the branch that contains s. Repeating such an alternating process generates the sequences F r : ab^{(2i+1)} and F s : ab^{(2i+2)} (i ≥ 0), making the repetitions of F r (resp. F s) differ in two occurrences of b from one another. Anyway, since there are only finitely many subformulas of the initial formula to prove, an open branch cannot infinitely grow without reaching a point where any newly introduced signed formula (and its related assertion) has already been introduced up to a fixed number of occurrences of the same constant. Such a branch will be said redundant, which is formalized in the following definition.

Definition 4.7 (redundancy). A completed branch B is said to be redundant for the constant c if there exists i ≥ 1 and k > i such that for any j ≥ k

1 T A : xc^{j} ∈ B implies T A : xc^{j−i} ∈ B and 2 F A : xc^{j} ∈ B implies F A : xc^{j−i} ∈ B and 3 x ≤ yc^{j} ∈ Ass(B) implies x ≤ yc^{j−i} ∈ Ass(B) and 4 xc^{j} ≤ y ∈ Ass(B) implies xc^{j−i} ≤ y ∈ Ass(B).

In order to prove the finite model property, we observe that we have the following result for a completed branch B.

Theorem 4.3 (finite model property). A completed branch B has a finite Kripke resource model.

Proof. The proof is by induction on the number of constants for which B is redundant. Base case: if there is no constant for which B is redundant then B is finite and by lemma 4.7 a Kripke resource model of B which is, by construction, obviously finite. Induction case: we assume that the proposition holds for any completed branch which is redundant for less than n constants. Let us suppose that B is redundant for n constants. We select one of those constants and denote it c. Then, we add the extra assertions c^{j} = c^{j−i} for any j ≥ k, where i, j and k refer to definition 4.7. It is routine to show that the composition modulo rewriting c^{j} = c^{j−i} preserves the properties of associativity, commutativity, and identity w.r.t. 1. Moreover, the properties 3 and 4 of definition 4.7 ensure that the branch B remains non contradictory. Since now, we cannot have more than k occurrences of c in the labels, we have treated the redundancy of B w.r.t. the constant c and we apply the induction hypothesis to obtain the result.

The finite model property w.r.t. Kripke resource models is a new result for BI^{⊥} which has significant consequences for its further applications, a major one being the decidability of BI^{⊥}. Indeed, the tableau construction procedure given in section 4.2.2, which is a semi-decision procedure, can be improved into a decision procedure by taking both the liberalized versions of the expansion rules and the notion of redundancy into account. Since, under the liberalized rules, an open branch cannot infinitely grow without becoming redundant, the termination of the procedure can be enforced by stopping the (potentially infinite) construction of a completed branch as soon as it has been recognized redundant.

5 Dependency Graphs and Provability

As explained in the previous sections, we have to deal, during the tableau construction, with two kinds of rules, namely πα and πβ. The first introduces new constants and forces, via so-called assertions, the relationships between these new constants. The second forces the introduction of labels from already existing constants. Moreover, these labels cannot be freely chosen: they must satisfy constraints called requirements, which have to be derivable from the existing assertions. In this section, we explain how the assertions can be represented through dependency graphs and how such structures can be used to determine provability.

5.1 Dependency Graphs

We give here a procedure that builds, in parallel with tableau expansions, a dependency graph which reflects the information that can be derived from a given set of assertions.

Definition 5.1. Given a branch B, the associated dependency graph DG(B) = [N(B), A(B)] is defined as the following directed graph: the set of nodes N(B) is the set of labels D(B) and the set of arrows A(B) is built from the set of assertions \overline{Ass}(B) as follows: there is an arrow x ⇾ y in A(B) iff there is an assertion x ≤ y in \overline{Ass}(B).

In order to simplify notations and because the graphs we consider are assumed to be reflexive and transitive, we do not explicitly mention, in A(B), arrows of the form x ⇾ x, or of the form x ⇾ y when there already exist x ⇾ z and z ⇾ y in A(B). Moreover, P red(B, x) will denote the set of immediate predecessors of a node x in the graph DG(B) while P red^{+}(B, x) will denote the set of all (not only immediate) predecessors. Let us remind that x is a sublabel of y (notation: x ⪯ y) if there exists a label z such that y = xz. P(x) denotes the set of all sublabels of a label x, y(x) means a label y having x as a sublabel and y[x/z] (or y[z] when clear from the context) means the substitution of x by z in y. We now define a procedure that builds the dependency graph DG(B) of a branch B. From that we can derive a procedure to compute the closure \overline{Ass}(B). Therefore, we connect to each tableau expansion rule of figure 2 a corresponding graph expansion rule. Thus, we can define expansion rules that deal with pairs ⟨ B, DG(B) ⟩ where B is a branch and DG(B) the corresponding dependency graph. The initial configuration is ⟨ B_{0}, DG(B_{0}) ⟩ defined as follows:

⟨ F(B_{0}) = { F A : 1 }, Ass(B_{0}) = { 1 ≤ 1 }, Req(B_{0}) = ∅ ⟩ , [ N(B_{0}) = { 1 }, A(B_{0}) = ∅]

The expansion rules of a dependency graph are such that the given graph is only expanded by the πα rules, all the other rules, introducing neither new constants, nor new assertions, simply leave the dependency graph unchanged. Let us give now these three expansion rules. For the rule T ∗, we have

⟨ F(B)(T A ∗ B : x), Ass(B), Req(B) ⟩ , [N(B), A(B)]

T ∗
⟨ F(B′), Ass(B′), Req(B′) ⟩ , [N(B′), A(B′)]

F(B′) := F(B) ∪ { T A : c_{i}, T B : c_{j} }

Ass(B′) := Ass(B) ∪ { c_{i} ≤ c_{i}, c_{j} ≤ c_{j}, c_{i}c_{j} ≤ x } Req(B′) := Req(B)

N(B′) := N(B) ; A(B′) := A(B)

for all y(x) in N(B) do

N(B′) := N(B′) ∪ { y[c_{i}], y[c_{j}], y[c_{i}c_{j}] } A(B′) := A(B′) ∪ { y[c_{i}c_{j}] ⇾ y[x] } for all z(x) in P red(B, y(x)) do A(B′) := A(B′) ∪ { z[c_{i}] ⇾ y[c_{i}], z[c_{j}] ⇾ y[c_{j}] } A(B′) := A(B′) ∪ { z[c_{i}c_{j}] ⇾ y[c_{i}c_{j}] } done done

For the rule F →, we have

⟨ F(B)(F A → B : x), Ass(B), Req(B) ⟩ , [N(B), A(B)]

F →
⟨ F(B′), Ass(B′), Req(B′) ⟩ , [N(B′), A(B′)]

F(B′) := F(B) ∪ { T A : c_{i}, F B : c_{i} }

Ass(B′) := Ass(B) ∪ { c_{i} ≤ c_{i}, x ≤ c_{i} }

Req(B′) := Req(B)

\begin{matrix}N(B′) := N(B) ∪ \{ c_{i} \} \\ A(B′) := A(B) ∪ \{ x ⇾ c_{i} \} \end{matrix}

For the rule F −∗, we have

⟨ F(B)(F A −∗ B : x), Ass(B), Req(B) ⟩ , [N(B), A(B)]

F −∗
⟨ F(B′), Ass(B′), Req(B′) ⟩ , [N(B′), A(B′)]

F(B′) := F(B) ∪ { T A : c_{i}, F B : xc_{i} }

Ass(B′) := Ass(B) ∪ { c_{i} ≤ c_{i} }

Req(B′) := Req(B) x^{l} := { x } ∪ P red^{+}(B, x) N(B′) := N(B) ∪ P(x^{l})c_{i} A(B′) := A(B) for all y in P(x^{l}) do

for all z in P red(B, y) do

A(B′) := A(B′) ∪ { zc_{i} ⇾ yc_{i} } done

done

Theorem 5.1. Let B be a branch and DG(B) be its associated dependency graph, the application of an expansion rule to ⟨ B, DG(B) ⟩ provides a new branch B′ and a new graph DG′ that is the dependency graph DG(B′) of B′.

Proof. In each case, we verify that the construction of DG(B′) from DG(B) by an expansion rule, leads to a graph that is a dependency graph associated to the branch B′.

5.2 Constraints and Provability

After having defined the dependency graph DG(B) associated to a given branch B, we observe that the problem of checking whether a requirement x ≤ y of Req(B) holds with respect to the set \overline{Ass}(B), can be directly solved on the corresponding dependency graph. It corresponds to checking if there exists a path in the graph DG(B) from the node x to the node y.

We illustrate the use of the dependency graph as a central semantical structure for the analysis of provability in BI^{⊥}. Thus, we consider the formula ((p ∗ (q −∗ r)) ∗ s) −∗ (p ∗ ((q −∗ r) ∗ s)) the tableau expansion of which is given on figure 3 and focus on the parallel construction of the associated dependency graph. Figure 7 presents the final dependency graph, with nodes i : c_{j} where i indicates which expansion step has introduced the node. Initially, we begin with the dependency graph DG(B_{0}) with N(B_{0}) = { 1 } and A(B_{0}) = ∅. Step 1 decomposes the outermost −∗ and, since c_{1}1 = c_{1}, the resulting graph is DG(B_{1}) where N(B_{1}) = { 1, c_{1} } and A(B_{1}) = ∅. The expansion of T (p ∗ (q −∗ r)) ∗ s : c_{1} in step 2 introduces two new constants c_{2}, c_{3} and the new assertion ass_{1} : c_{2}c_{3} ≤ c_{1}. The rule for T ∗ yields the graph DG(B_{2}) with N(B_{2}) = N(B_{1}) ∪ { c_{2}, c_{3}, c_{2}c_{3} } and A(B_{2}) = A(B_{1}) ∪ { c_{2}c_{3} ⇾ c_{1} }. Step 3 expands the signed formula T p ∗ (q −∗ r) : c_{2} which introduces two new constants c_{4}, c_{5} and the new assertion ass_{2} : c_{4}c_{5} ≤ c_{2}. The dependency graph is DG(B_{3}) with N(B_{3}) = N(B_{2}) ∪ { c_{4}, c_{5}, c_{4}c_{5} } ∪ { c_{3}c_{4}c_{5}, c_{3}c_{4}, c_{3}c_{5} } and A(B_{3}) = A(B_{2})∪ { c_{4}c_{5} ⇾ c_{2} }∪ { c_{3}c_{4}c_{5} ⇾ c_{2}c_{3} } ^{2}. We add the arrow c_{4}c_{5} ⇾ c_{2}, but since we already have a node c_{2}c_{3}, we must create a node c_{2}c_{3}[c_{2}/c_{4}c_{5}] = c_{3}c_{4}c_{5} and a new arrow c_{3}c_{4}c_{5} ⇾ c_{2}c_{3}. Moreover, as we add the node c_{3}c_{4}c_{5}, we must take care to add all nodes corresponding to the sublabels of c_{3}c_{4}c_{5} that does not already appear in the graph. It provides two more nodes, namely, c_{3}c_{4} and c_{3}c_{5}.

Figure 7: Dependency Graph for ((p ∗ (q −∗ r)) ∗ s) −∗ (p ∗ ((q −∗ r) ∗ s))

With step 4, we reach the point where we need to expand the πβ signed formula F p ∗ ((q −∗ r) ∗ s) : c_{1}. We must therefore find a compound label xy such that xy ≤ c_{1}. But, using the dependency graph, this simply means that xy should be taken among the nodes that are ancestors of the node c_{1}. Thus, we only have two possibilities, namely, c_{2}c_{3} and c_{3}c_{4}c_{5}. Only the latter contains c_{4}, which is needed to close the first branch on p, so that x = c_{4} and y = c_{3}c_{5}. The same kind of reasoning is applied at step 5 where we must find a compound label xy such that xy ≤ c_{3}c_{5}. But this time, as the node c_{3}c_{5} has no ancestors except itself (remind that the graph is implicitly reflexive), the only possible value for xy is c_{3}c_{5}. However, the choice of the branch on which to spread c_{3} still remains. Here, looking upward in the branch suggests that spreading c_{3} in the right branch allows us to close it with s and, at the same time, to close the left branch with q −∗ r.

5.3 Countermodel Extraction

We explain here how to extract a countermodel from a dependency graph when the formula is not provable. In fact, we observe that the dependency graph could be directly seen as (a representation of) a countermodel. But let us illustrate this point with the formula ((p ∗ q) ∧ (p ∗ r)) −∗ (p ∗ (q ∧ r)). Figure 8 shows its dependency graph. Compared with our previous example, steps 1 to 4 are quite similar and lead to the dependency graph DG(B_{4}) whose nodes are N(B_{4}) = { 1, c_{1}, c_{2}, c_{3}, c_{4}, c_{5}, c_{2}c_{3}, c_{4}c_{5} } and arrows are A(B_{4}) = { c_{2}c_{3} ⇾ c_{1}, c_{4}c_{5} ⇾ c_{1} }. Once again, when we must expand the πβ formula, we have to find a compound label yz such that yz ≤ c_{1}. From the dependency graph, we see that there are two possibilities, namely, c_{2}c_{3} and c_{4}c_{5}. We first try an expansion with the former one. Since the right branch is not closed, we go through step 6. After step 6, all πα formulas have been treated and the right-most branch is still open. Then, we must try the second possibility, c_{4}c_{5}, for the πβ formula (step 7). Since the right-most branch is still open, we continue with step 8, by developing the additive conjunct. After that, the right-most remains open, but this time, we can say from the dependency graph that all possibilities have been tried for the πβ formula. Therefore, the tableau expansion is completed and contains an open branch, which means that the formula is unprovable. Since all formulas in the open branch are fulfilled, we have a finite completed branch. We can therefore extract the corresponding countermodel following the different steps of the completeness proof. For that, we take the nodes of the dependency graph, to which we add the particular element π, as the set of worlds M. The preordering relation ⊑ is simply induced by the arrows of the dependency graph, which gives c_{2}c_{3} ⊑ c_{1}, c_{4}c_{5} ⊑ c_{1} and m ⊑ π for any m ∈ M.

2We have written the resulting graph using two unions in order to distinguish what directly comes from the tableau rule and what comes from the closure.

Figure 8: Dependency Graph for ((p ∗ q) ∧ (p ∗ r)) −∗ (p ∗ (q ∧ r))

The • operation is defined 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 forcing relation ⊧ is parametrized by the following atomic interpretation:

\begin{matrix}x & p & q & r \\ ⟦x⟧ & \{ π, c_{2}, c_{4} \} & \{ π, c_{3} \} & \{ π, c_{5} \} \end{matrix}

Now, we verify that we actually built a countermodel by checking that, on one hand, c_{1} ⊧ (p ∗ q) ∧ (p ∗ r) and, on the other hand, c_{1} |̸= p ∗ (q ∧ r). First, we have c_{2} • c_{3} ⊧ p ∗ q because, by definition, c_{2} ⊧ p and c_{3} ⊧ q. Since c_{2} • c_{3} ⊑ c_{1}, it follows from (K) that c_{1} ⊧ (p ∗ q). Similarly, we can prove c_{1} ⊧ (p ∗ r). Thus, c_{1} ⊧ (p ∗ q) ∧ (p ∗ r). Second, we observe that no world other than π satisfies q and r at the same time. Thus, π is the only world satisfying q ∧ r. Since c_{1} cannot be obtained by any composition with π, c_{1} |̸= p ∗ (q ∧ r).

The dependency graph, that we could also call Kripke resource graph (because of the direct relationship with the Kripke resource semantics), is a central concept in this labelled tableau method. It captures the semantics and the interactions between additive and multiplicative connectives and allows to check if the initial formula is provable or not. It is important to notice that we aim to generate countermodels that could be helpful for the analysis of the proof failure. In addition to an efficient generation, we need also to have a good representation of countermodels and, in this context, a dependency graph can be directly seen as the essential graphical representation of a countermodel, from which we can generate a countermodel in the given semantics. Moreover, the question of the minimality of a countermodel could be studied by from refinements of this semantic graph structure.

6 A Free Variable Labelled Tableau for BI^{⊥}

In the TBI^{⊥} calculus we have two kinds of constrained rules. The F −∗, F → and T ∗ rules create new (atomic) labels and new assertions which are used as hypotheses in the proof-search process. On the contrary, the T −∗, T → and F ∗ rules introduce labels which are supposed to satisfy a specific requirement w.r.t. the assertions. Therefore, making clever choices for these labels is a critical issue for the efficiency of the tableau method. This difficulty can be partially overcome by stating free variable versions of these rules which allow to postpone the choice of suitable labels for a given requirement until enough information is available [7].

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

F A → B : x ; ass : x ≤ c_{i} ^{∗} ; \begin{matrix}T A : c_{i} \\ F B : c_{i} \end{matrix}  T A ∗ B : x ; ass : c_{i}c_{j} ≤ x ^{∗} ; \begin{matrix}T A : c_{i} \\ T B : c_{j} \end{matrix}  F A −∗ B : x ; \begin{matrix}T A : c_{i} ^{∗} \\ F B : xc_{i} \end{matrix}

T A → B : x ; \begin{matrix}req : x ≤ v_{i} & ∗∗ \\ F A : v_{i} & T B : v_{i} \end{matrix}  F A ∗ B : x ; \begin{matrix}req : v_{i}v_{j} ≤ x & ∗∗ \\ F A : v_{i} & F B : v_{j} \end{matrix}  \begin{matrix}T A −∗ B : x \\ F A : v_{i} & T B : xv_{i} ^{∗∗} \end{matrix}

∗ c_{i}, c_{j} are new constants
∗∗ v_{i}, v_{j} are new variables

Figure 9: Expansion Rules with Free Variables

6.1 A Free Variable Calculus

We enrich the labelling language with a denumerable set of variables v_{1},v_{2},...,v_{n}. All the previous notions (labelling algebra, labelled formulas, expansion set, configurations) are extended to labels with variables.

Definition 6.1. A label schema α is a label that contains variables. A ground label is a label that only contains constants. We note L^{†} the restriction of L to ground labels.

We extend the expansion rules to label schemas, then, in addition to the set C(B), we consider the set V (B) of the variables occurring in a branch B.

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

Definition 6.3. Let V be a set of variables, a ground substitution σ is an application from V → L^{†}, where L^{†} is the set of ground labels; a ground substitution σ for a branch B is a ground substitution the domain of which is V (B).

Definition 6.4. Let B be a tableau branch, two signed formulas T A : x, F A : y of F(B) are said σcomplementary in B if and only if σ(x) ≤ σ(y) ∈ \overline{σ(Ass(B))}, i.e., if the ground constraint σ(x) ≤ σ(y) belongs to the reflexive, transitive and compatible closure of the ground assertions σ(Ass(B)).

Definition 6.5. A tableau t is σ-closed if there exists a ground substitution σ whose domain is ⋃_{B∈t} V (B) and such that for any B in t,

i) there are two formulas T A : x and F A : y that are σ-complementary in B or there is F ⊤ : x in B or there is F I : x in B with 1 ≤ σ(x) ∈ \overline{σ(Ass(B))}, or there is T I : x in B with 1 ≤ σ(x) ∉ \overline{σ(Ass(B))}; ii) for all x ≤ y ∈ Req(B) σ(x) ≤ σ(y) ∈ \overline{σ(Ass(B))}.

Definition 6.6. A tableau sequence T = t_{1}, t_{2}, … is σ-closed if it contains at least one σ-closed tableau t_{i} and σ is such that any variable v is mapped to a ground label which is built using exclusively constants that were introduced before v in the sequence t_{1}, …, t_{i}.

√_{1} F ((p ∗ (q −∗ r)) ∗ s) −∗ (p ∗ ((q −∗ r) ∗ s)) : 1

√_{2} T (p ∗ (q −∗ r)) ∗ s : c_{1} √_{4} F p ∗ ((q −∗ r) ∗ s) : c_{1}

ass_{1} : c_{2}c_{3} ≤ c_{1}

\begin{matrix}√_{3} T p ∗ (q −∗ r) : c_{2} \\ T s : c_{3} \end{matrix}

ass_{2} : c_{4}c_{5} ≤ c_{2}

\begin{matrix}T p : c_{4} \\ √_{7} T q −∗ r : c_{5} \end{matrix}

req_{1} : v_{1}v_{2} ≤ c_{1}

F p : v_{1}_{F q : v_{5} T r : c_{5}v_{5}} √_{5} F (q −∗ r) ∗ s : v_{2}

req_{2} : v_{3}v_{4} ≤ v_{2}

√_{6} F q −∗ r : v_{3}

\begin{matrix}T q : c_{5} \\ F r : c_{5}v_{3} \end{matrix}

F q : v_{6}  T r : c_{5}v_{6}

F s : v_{4}_{F q : v_{7} T r : c_{5}v_{7}}

Figure 10: Free Variable Tableau for (p ∗ (q −∗ r)) ∗ s) −∗ (p ∗ ((q −∗ r) ∗ s)

From these definitions, we can directly prove, like in section 4, the properties of soundness, completeness and finite model property of a free variable version of TBI^{⊥}.

6.2 Examples of free variable tableaux

Let us consider the formula ((p∗(q−∗r))∗s)−∗(p∗((q−∗r)∗s)), on figure 10, using our free variable labelled tableau system. Compared to the initial system, tableau expansions go through without change until step 3. The key difference appears at step 4, when decomposing the πβ formula F p ∗ ((q −∗ r) ∗ s) : c_{1}. Previously, we had to find a compound label yz such that yz ≤ c_{1}. Now, we simply introduce two new variables v_{1}, v_{2}, together with a new requirement req_{1} : v_{1}v_{2} ≤ c_{1} expressing a constraint which, once ground, they are supposed to match if we aim a sound expansion step. We proceed with step 5, which is just similar, introducing new variables v_{3}, v_{4} and the corresponding requirement req_{2} : v_{3}v_{4} ≤ v_{2}. Since the formula F q −∗ r : v_{3} introduced in the last step is a πα formula, it is immediately expanded in step 6. Finally, step 7 develops the πβ formula T q −∗ r : c_{5}, introducing by the way three new variables (one for each extended branch), namely, v_{5}, v_{6} and v_{7}. After step 7, the tableau is completed. The problem is now to find a ground substitution that allows us to close each branch of the tableau. We only have one potential connection, namely, ⟨ T p : c_{4}, F p : v_{1} ⟩, to close the first and the second branch at the same time. Setting v_{1} ↦ c_{4} does the job, making v_{5} useless by the way. For the third branch, the only possible connection is ⟨ T q : c_{5}, F q : v_{6} ⟩, giving v_{6} ↦ c_{5}. Considering ⟨ T r : c_{5}v_{6}, F r : c_{5}v_{3} ⟩ on the fourth branch suggests v_{3} ↦ v_{6}. The last two branches, once again, contain only one potential connection, namely, ⟨ T s : c_{3}, F s : v_{4} ⟩, which yields v_{4} ↦ c_{3} and makes v_{7} useless. We therefore have found a partial (v_{2} is yet undefined) ground substitution that closes each branch of the tableau. In order to verify that this substitution is an admissible solution, we must also check, branch by branch, whether the requirements can be satisfied from the assertions. Beginning with req_{2} : v_{3}v_{4} ≤ v_{2} will allow us to fix a value for v_{2}. Indeed, simply choosing v_{2} ↦ c_{3}c_{5} makes the requirement trivially satisfied. It remains to ensure that req_{1} : v_{1}v_{2} ≤ c_{1} also holds. More precisely, what we need to show is that req_{1} : c_{3}c_{4}c_{5} ≤ c_{1} can be derived from the reflexive, transitive and compatible closure of the assertions ass_{1} : c_{2}c_{3} ≤ c_{1} and ass_{2} : c_{4}c_{5} ≤ c_{2}. But this requirement is simply obtained by first applying compatibility on ass_{2} and c_{3} ≤ c_{3}, which yields c_{3}c_{4}c_{5} ≤ c_{2}c_{3}, and then using transitivity on ass_{1}. Thus, our ground substitution closes each branch of the tableau and, moreover, satisfies all requirements. The conclusion is therefore that the formula is provable.

√_{1} F ((p ∗ q) ∧ (p ∗ r)) −∗ (p ∗ (q ∧ r)) : 1
√_{2} T (p ∗ q) ∧ (p ∗ r) : c_{1}

√_{5} F p ∗ (q ∧ r) : c_{1}

\begin{matrix}√_{3} T p ∗ q : c_{1} \\ √_{4} T p ∗ r : c_{1} \end{matrix}

ass_{1} : c_{2}c_{3} ≤ c_{1}

\begin{matrix}T p : c_{2} \\ T q : c_{3} \end{matrix}

ass_{2} : c_{4}c_{5} ≤ c_{1}

\begin{matrix}T p : c_{4} \\ T r : c_{5} \end{matrix}

req_{1} : v_{1}v_{2} ≤ c_{1}

F p : v_{1}  \begin{matrix}√_{6} F q ∧ r : v_{2} \\ F q : v_{2} & F r : v_{2} \end{matrix}

Figure 11: Free variable tableau for (p ∗ q) ∧ (p ∗ r)) −∗ (p ∗ (q ∧ r)

We now reconsider our second example in figure 11. There is no change until step 4. Step 5, on the contrary, introduces two new variables v_{1}, v_{2} and the new requirement req_{1} : v_{1}v_{2} ≤ c_{1}. Step 6 simply spreads variable v_{2} in both branches of the additive conjunct. After step 6, the tableau expansion is completed. At this step, it is important to mention that, in the free variable version, one first tries to close branches and checks, afterwards, if the requirements are satisfied from the assertions, while in the initial version, one tries to solve requirements as they are introduced by each πβ expansion step in order to perform a valid expansion. Let us come back to our example. Once again, we are faced with the problem of finding a ground substitution that closes each branch of the tableau. We begin with the first branch and notice that there are two potential connections ⟨ T p : c_{2}, F p : v_{1} ⟩ and ⟨ T p : c_{4}, F p : v_{1} ⟩. The first connection yields v_{1} ↦ c_{2}, but then, we must match the requirement req_{1} : v_{1}v_{2} ≤ c_{1}. From the assertion ass_{1} : c_{2}c_{3} ≤ c_{1}, it is clear that the only possibility for v_{2} is v_{2} ↦ c_{3}, which closes the second branch with ⟨ T q : c_{3}, F q : c_{3} ⟩ but leaves the third one open since c_{5} ≤ c_{3} cannot be proved for ⟨ T r : c_{5}, F r : c_{3} ⟩. We must therefore try the other possibility, that is, v_{1} ↦ c_{4}. It leads, by assertion ass_{2} : c_{4}c_{5} ≤ c_{1}, to set v_{2} ↦ c_{5}, which allows us to close the first and the third branches of the tableau. But then, the second branch remains open since c_{3} ≤ c_{5} cannot be proved for ⟨ T q : c_{3}, F q : c_{5} ⟩. Thus, whatever admissible ground substitution

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

\begin{matrix}F A ∧ B : x \\ F A : x & F B : x \end{matrix}  F A → B : x ; ass : x ≤ c_{i} ^{∗} ; \begin{matrix}T A : c_{i} \\ F B : c_{i} \end{matrix}  T A → B : x ; req : x ≤ y ; F A : y  T B : y

∗ c_{i} is a new constant

Figure 12: Expansion Rules for IL

we may choose, we are left with an open branch and the resulting conclusion is that the formula is not provable. These examples illustrate the actual interest to introduce free variables into labels. In general, the use of free variables rules is crucial for efficient implementation [9]. They reduce at each step the number of possible next steps in the construction of the tableau proof and thus the size of the search space. Free variables can later be instantiated when a tableau is closed. These characteristics can be used for our labelled tableau calculus in order to optimize proof search in BI^{⊥}. Free variables help us to improve efficiency of the proof-search since they remove many irrelevant πβ expansion steps by introducing variables whose evaluation is postponed until enough information is available. However, the countermodels become more difficult to generate because multiple πβ extensions in the initial system correspond, in the free variable version, to distinct variable instantiations. In fact, the introduction of variables involves a kind of branches “factorization”. Therefore, countermodels must be built by recomposition from distinct open branches in several steps, in fact, one step for each admissible valuation of the variables, i.e., valuations which make the requirements hold w.r.t. (ground) assertions. Another difficulty that arises with free variables is how to limit the application of the πβ rules, i.e., the ones that introduce variables, while still retaining completeness. In [7], it is claimed that such rules need only be expanded once, but this point has to be thoroughly and carefully studied. Our feeling is that some formulas(like ((((p → q) → p) → p) → q) → q, for example) may require several expansions of the same πβ formula, which could be handled by assigning multiplicities to πβ much like in matrix-based methods. Further work will focus on this point.

7 A New Tableau Method for IL

From the conservativity result of theorem 2.2, we can see intuitionistic logic (IL) as a subsystem of BI. Consequently, the restriction of the initial TBI^{⊥} calculus to the additive connectives, i.e., the expansion rules of figure 12, directly provides a new tableau method for IL. Compared to LDS works [5] and also to standard tableaux methods [9] for IL this new method is based on an original and powerful treatment of the Kripke semantics through labels and constraints. It naturally leads to a direct construction of countermodels. The introduction of assertions and requirements improves proof-search by capturing the necessary and sufficient semantical information into a dependency graph. This structure allows to analyze provability through the verification of requirements on a finite portion of the underlying infinite labelling algebra. In case of non-provability, the countermodel can be immediately generated from an open branch without any further recomposition (by instantation) from other open branches like in standard methods [9]. In order to emphasize the characteristics of this new tableau method for IL, we develop and analyze it in details in this section.

All definitions (complementary formulas, closed tableau, fulfilled formula, etc...) given for BI^{⊥} are restricted to IL by simply discarding statements involving either multiplicative connectives, or the multiplicative unit I, or the ∘ connective. As an immediate consequence of this restriction, the resulting labelling algebra is only composed of atomic labels and the constraints are preordering relations between such atomic labels. As we consider BI^{⊥}, the direct restriction to IL does not include the ⊥ unit. Nevertheless, since Kripke models are complete for IL (with ⊥), the restriction can be straightforwardly extended to ⊥ by adding T ⊥ : x in the definition of closure and B ⊩ F ⊥ : x in the definition of fulfillment.

Definition 7.1. Let B be an tableau branch, two signed formulas T A : x, F A : y of F(B) are said complementary in B if and only if x ≤ y ∈ \overline{Ass}(B).

Definition 7.2. A tableau t is closed if, for all its branches B,

i) there are two formulas T A : x and F A : y that are complementary in B or there is F ⊤ : x in B or T ⊥ : x in B; ii) for all x ≤ y ∈ Req(B), we have x ≤ y ∈ \overline{Ass}(B). A tableau sequence T = t_{1}, t_{2}, …, t_{n} is closed if it contains at least one closed tableau.

7.1 A Tableau Construction Procedure for IL

Let us recall the main definitions in order to define a procedure for the tableau construction in IL.

Definition 7.3. Let B be a tableau branch, a signed formula Sg X : x is fulfilled (or completely analyzed) in B, noted B ⊩ Sg X : x, if it satisfies one of the following conditions

1. B ⊩ F ⊥ : x

2. B ⊩ F ⊤ : x

3. B ⊩ F p : x iff there exists F p : y ∈ B such that x ≤ y ∈ \overline{Ass}(B)

4. B ⊩ F A ∧ B : x iff either B ⊩ F A : x or B ⊩ F B : x

5. B ⊩ F A ∨ B : x iff both B ⊩ F A : x and B ⊩ F B : x

6. B ⊩ F A → B : x iff there exists y ∈ D(B) such that x ≤ y ∈ \overline{Ass}(B) and both B ⊩ T A : y and B ⊩ F B : y

7. B ⊩ T ⊤ : x

8. B ⊩ T p : x iff there exists T p : y ∈ B such that y ≤ x ∈ \overline{Ass}(B)

9. B ⊩ T A ∧ B : x iff both B ⊩ T A : x and B ⊩ T B : x

10. B ⊩ T A ∨ B : x iff either B ⊩ T A : x, or B ⊩ T B : x

11. B ⊩ T A → B : x iff for any y ∈ D(B) such that x ≤ y ∈ \overline{Ass}(B) either B ⊩ F A : y, or B ⊩ T B : y

Definition 7.4. A tableau branch B is completed if it is open and every signed formula Sg A : x of B is fulfilled. A tableau is completed if it has a completed branch.

Lemma 7.1 (monotonicity). A completed branch B satisfies Kripke monotonicity, more precisely,

1) B ⊩ F A : x and y ≤ x ∈ \overline{Ass}(B) imply B ⊩ F A : y, and

2) B ⊩ T A : x and x ≤ y ∈ \overline{Ass}(B) imply B ⊩ T A : y.

Proof. By structural induction on Sg X : x.

Lemma 7.2 (consistency). If B is a completed branch, then, for any IL proposition A, we cannot have both B ⊩ T A : x and B ⊩ F A : x.

Proof. See the proof of lemma 4.5.

We give a tableau construction procedure that is an algorithm that, for a given formula A, builds a tableau sequence t_{1}, t_{2}, …, t_{n} until there exists a tableau t_{i} that is either closed or includes a completed branch. This procedure for IL, that is called TBI/IL, is the following:

The initial signed formula is F A : 1 and it is marked unvisited. Repeat until T is closed or completed

if there is no unvisited formula Sg X : x in any open branch B then mark all πβ-formulas in all open branches as unvisited else mark Sg X : x as visited if Sg X : x is not fulfilled in B then if Sg X : x is of type πβ then expand Sg X : x with a label y for which the formula is not fulfilled else expand Sg X : x according to its type

An important result is the termination of this procedure. First, let us remark that the F → rule is the only one that introduces new atomic labels and its application can potentially lead to infinite branches. In order to have a terminating procedure, we give a liberalized version of the F → rule that allows, under given conditions, to reuse existing constants.

Lemma 7.3. Let B be a branch and F A → B : x be a signed formula in B, the following rule

F A → B : x ; \begin{matrix}T A : x \\ F B : x \end{matrix}

is admissible provided there exists T A : y in B such that y ≤ x ∈ \overline{Ass}(B).

Proof. Let K = ⟨ M, ⊧, ⟦–⟧ ⟩ be a Kripke model and ∥–∥ be a realization of B in K. Let us suppose that ∥x∥ = m and ∥y∥ = n, then, by definition of a realization, F A → B : x, T A : y ∈ B and y ≤ x ∈ \overline{Ass}(B) imply m |̸= A → B, n ⊧ A and n ⊑ m. Since n ⊧ A and n ⊑ m, it follows from property (K) of definition 2.4 that m ⊧ A. On the other hand, m |̸= A → B implies that there exists n′ such that m ⊑ n′, n′ ⊧ A and n′ |̸= B, which, by contraposition of condition (K), yields m |̸= B.

Theorem 7.1 (termination). The tableau construction procedure, including the liberalized version of the F → rule, terminates.

Proof. We only give the sketch of the proof. For that, we slightly modify our notation for constants. When we expand a labelled signed formula F A → B : x, we suppose, instead of introducing a new constant c_{i} and a new assertion x ≤ c_{i}, that we simply introduce a term c_{i}(x), with the meaning that c_{i} depends on x in such a way that the assertion x ≤ c_{i} is implicitly verified. Then, starting from the the initial formula to prove, we associate to each subformula of the form F A → B a unique functor symbol which will be used, parametrized with the corresponding label, by each expansion of F A → B. For example, if c_{i} is the functor symbol associated to F A → B, then, the expansion of F A → B : x introduces the term c_{i}(x) and, if we later expand F A → B : y, we simply reuse the same functor symbol c_{i}, but parametrized with the label y, i.e., c_{i}(y). This roughly corresponds to a kind of skolemization of the initial formula, and thus, we only have one “real” atomic label left, namely, the unit 1. The other labels are terms of the form c_{i1}(c_{i2}(⋯ c_{ik}(1) ⋯)), or c_{i1}c_{i2} ⋯ c_{ik}(1) for brevity. Moreover, if s is a subterm of t, we implicitly have s ≤ t. Now, we suppose that we need to expand a formula F A → B : c_{i1} ⋯ c_{ik}(1), with some c_{ij(j∈[1..k])} being the functor symbol corresponding to F A → B. Then, F A → B previously occured in the branch with the label c_{i(j+1)} ⋯ c_{ik}(1) and has been expanded to produce T A : c_{ij} ⋯ c_{ik}(1). Besides, since c_{ij} ⋯ c_{ik}(1) is a subterm of c_{i1} ⋯ c_{ik}(1), we also have c_{ij} ⋯ c_{ik}(1) ≤ c_{i1} ⋯ c_{ik}(1). Therefore, we are in the situation required by the liberalized F → rule to be applicable and we can perform our expansion step by simply reusing the term c_{i1} ⋯ c_{ik}(1) instead of introducing a new composition c_{ij}c_{i1} ⋯ c_{ik}(1). This shows that, if we use the liberalized version of F →, the only terms that can occur in a tableau branch are terms which do not contain the same functor symbol twice. Now, let us remark that since there are obviously finitely many distinct subformulas of the initial formula to prove, there are also finitely many associated functor symbols. Consequently, there are finitely many possibilities to combine those functors so that each of them occurs at most once in the combination, which means that the F → expansion steps √_{1} F ((p → q) ∨ (p → r)) → (p → (q ∨ r)) : 1

ass_{1} : 1 ≤ c_{1}

√_{4} T (p → q) ∨ (p → r) : c_{1} √_{2} F p → (q ∨ r) : c_{1}

ass_{1} : c_{1} ≤ c_{2}

\begin{matrix}T p : c_{2} \\ √_{3} F q ∨ r : c_{2} \end{matrix}

\begin{matrix}F q : c_{2} \\ F r : c_{2} \end{matrix}

√_{5} T p → q : c_{2} ; req_{1} : c_{1} ≤ c_{2} ; \begin{matrix}F p : c_{2} \\ × \end{matrix}  \begin{matrix}T q : c_{2} \\ × \end{matrix}  √_{5} T p → r : c_{2} ; req_{1} : c_{1} ≤ c_{2} ; \begin{matrix}F p : c_{2} \\ × \end{matrix}  \begin{matrix}T r : c_{2} \\ × \end{matrix}

Figure 13: Labelled Tableau for ((p → q) ∨ (p → r)) → (p → (q ∨ r))

cannot infinitely produce new compositions during a branch expansion. The termination property then directly follows.

7.2 Proof and Countermodel Construction

In this subsection, we illustrate how to build proofs and countermodels in our new calculus for IL. There exist several deduction systems for (propositional) IL that build proofs but also countermodels in case of non-provability [8, 13, 24, 33]. The specificity of our method is the use of labels in order to improve proof-search. The example, given in figure 13, with the formula ((p → q) ∨ (p → r)) → (p → (q ∨ r)) well illustrates how the TBI/IL calculus works. In this example, the tableau is closed and consequently the given formula is provable in IL. In a second example, given in figure 14, we consider the formula (p → (q ∨ r)) → ((p → q) ∨ (p → r)) that leads to an unclosed tableau. As one can notice, the πβ signed formula T p → (q ∨ r) : c_{1} has been expanded twice: a first time in step 5 with the constant c_{2} and a second time in step 7 with the constant c_{3} because both c_{1} ≤ c_{2} and c_{1} ≤ c_{3} belong to the closure of the assertions. As in TBI^{⊥} such multiple expansions are necessary in order to have a completed tableau. With our tableau system, we can directly generate countermodels from open branches. Since we do not deal with the ∘ connective, the expansion of a tableau branch provides, via its assertions, a preordering relation from which, in the case of the existence of a completed branch, we can directly define a Kripke model in the following way.

Definition 7.5. Let B be a completed branch, the structure M(B) is defined by M(B) = ⟨ M, ⊑ ⟩ where i) M is the set D(B), ii) the relation ⊑ is defined by: x ⊑ y if and only if x ≤ y ∈ \overline{Ass}(B).

Definition 7.6. Let M(B) = ⟨ M, ⊑ ⟩ be the M-structure of a completed branch B and P(L) denote the collection of IL propositions over a language L of propositional letters. We define the interpretation √_{1} F (p → (q ∨ r)) → ((p → q) ∨ (p → r)) : 1

ass_{1} : 1 ≤ c_{1}

√_{7,5} T p → (q ∨ r) : c_{1} √_{2} F (p → q) ∨ (p → r) : c_{1}

\begin{matrix}√_{3} F p → q : c_{1} \\ √_{4} F p → r : c_{1} \end{matrix}

ass_{2} : c_{1} ≤ c_{2}

\begin{matrix}T p : c_{2} \\ F q : c_{2} \end{matrix}

ass_{3} : c_{1} ≤ c_{3}

\begin{matrix}T p : c_{3} \\ F r : c_{3} \end{matrix}

req_{1} : c_{1} ≤ c_{2}

F p : c_{2} × √_{6} T q ∨ r : c_{2}

T q : c_{2} × T r : c_{2}

req_{2} : c_{1} ≤ c_{3}

\begin{matrix}F p : c_{3} \\ × \end{matrix}  \begin{matrix}√_{8} T q ∨ r : c_{3} \\ T q : c_{3} & \begin{matrix}T r : c_{3} \\ × \end{matrix} \end{matrix}

Figure 14: Labelled Tableau for (p → (q ∨ r)) → ((p → q) ∨ (p → r))

⟦– ⟧_{B} : L → P(M), for any atomic proposition p, by ⟦p⟧_{B} = { x | B ⊩ T p : x }.

Theorem 7.2. Let B be a completed branch, the triple ⟨ M(B), ⊧, ⟦– ⟧_{B} ⟩ is a Kripke model of B, i.e.,

1) ⟦– ⟧_{B} satisfies the (K) condition of definition 2.4;

2) for any proposition A, we have a) B ⊩ T A : x implies x ⊧ A,

b) B ⊩ F A : x implies x |̸= A.

Proof.

1) We suppose x ∈ ⟦p⟧_{B} and x ⊑ y. Then, B ⊩ T p : x and x ≤ y ∈ \overline{Ass}(B). Therefore, by lemma 7.1, B ⊩ T p : y, i.e., y ∈ ⟦p⟧_{B}.

2.a), 2.b) We proceed by structural induction on Sg A : x.

– if B ⊩ T p : x then, by definition, x ∈ ⟦p⟧_{B}, i.e., x ⊧ p.

– if B ⊩ F p : x then, by lemma 7.2, B ⊮ T p : x. Thus, x ∉ ⟦p⟧_{B}, i.e., x |̸= p.

– if B ⊩ T B ∧ C : x then, both B ⊩ T B : x and B ⊩ T C : x. By the induction hypothesis, it follows that x ⊧ B and x ⊧ C, i.e., x ⊧ B ∧ C.

Figure 15: Kripke Countermodel for (p → (q ∨ r)) → ((p → q) ∨ (p → r))

– if B ⊩ F B ∧ C : x then, either B ⊩ F B : x or B ⊩ F C : x. By the induction hypothesis, it follows that x |̸= B or x |̸= C, i.e., x |̸= B ∧ C.

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

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

– if B ⊩ T B → C : x then, for any y in D(B) such that x ≤ y ∈ \overline{Ass}(B), either B ⊩ F B : y or B ⊩ T C : y. By the induction hypothesis, it follows that either y |̸= B or y ⊧ C for any y in M such that x ⊑ y, i.e., x ⊧ B → C.

– if B ⊩ F B → C : x then, there exists y in D(B) such that x ≤ y ∈ \overline{Ass}(B), B ⊩ F B : y and B ⊩ T C : y. By the induction hypothesis, it follows that there exists y ∈ M such that x ⊑ y, y ⊧ B and y |̸= C, i.e., x |̸= B → C.

For the example of figure 14, in which the fourth branch is open, theorem 7.2 yields the countermodel ⟨ M(B), ⊧, ⟦–⟧ ⟩ where M = { 1, c_{1}, c_{2}, c_{3} }, ⊑ is defined by 1 ⊑ c_{1} ⊑ c_{2}, c_{3} and ⊧ is given by the table

\begin{matrix}x & p & q & r \\ ⟦x⟧ & \{ c_{2}, c_{3} \} & \{ c_{2} \} & \{ c_{3} \} \end{matrix}

It corresponds to the Kripke tree given in figure 7.2, on which we can verify that c_{1} ⊧ p → (q ∨ r), since c_{2} ⊧ q ∨ r and c_{3} ⊧ q ∨ r. Moreover, c_{1} |̸= (p → q) ∨ (p → r) because c_{2} |̸= p → r and c_{3} |̸= p → q.

Let us make some remarks on the countermodel generation. Firstly, we can easily notice that the countermodels we obtain are in fact Kripke trees with 1 as the root. Furthermore, such Kripke trees are so-called strong countermodels since the root is precisely the node at which the initial tableau formula is not forced. Secondly, the countermodels are directly obtained from a completed branch without performing any backtracking or further computations like in standard methods dedicated to IL. Indeed, backtracking has been internalized in the multiple T → expansions. In practice, these rules can be more efficiently handled by using free variables in order to delay the choice of labels used to close branches and then avoid to test all possibilities.

7.3 Properties of the IL Labelled Calculus

We can refine the properties of the TBI^{⊥} calculus and then obtain the following:

Theorem 7.3 (soundness). Let A be a proposition of IL, if there exists a closed tableau sequence for A in TBI/IL, then A is valid in Kripke semantics.

Proof. See the proof of theorem 4.1 with restriction to IL.

Theorem 7.4 (completeness). Let A be a IL formula, if A is valid in Kripke semantics, then there exists a closed tableau sequence for A in TBI/IL.

Proof. Let us suppose that there is no closed tableau sequence for A. Then, by theorem 7.1, the tableau construction procedure given in subsection 7.1 terminates with a tableau which contains a completed branch. From this branch we can build, following theorem 7.2, a Kripke model in which A is not satisfied. Therefore, A is not valid in the Kripke semantics.

Theorem 7.5 (finite model property). Let A be a proposition of IL, if A is not valid in Kripke semantics, then, there exists a finite Kripke model in which A is not satisfied.

Proof. Let us assume that A is not valid in the Kripke semantics. From theorem 7.1, we deduce that the tableau construction procedure terminates by providing a tableau with a completed branch that is necessarily finite. The construction given in definition 7.5 results in a finite Kripke model.

Further work will be devoted to efficient constraint satisfaction in IL. This new method emphasizes that, in a logic with a resource semantics, labels and constraints can be used in order to capture its consequence relation. It appears as a more general approach than trying to capture the right order of rules applications in the sequent calculus, with prefixes for instance. This point will be more deeply analyzed in comparison with other constraint-based proof calculi for IL [38]. In case of the definition of a free variable variant, we have the same problems that we already mentioned in the case of BI. Compared to other proof-search methods based on specific sequent calculi with countermodel generation facility [24, 33], our labelled tableau method is efficient and avoids many backtrackings. As said before, the notion of minimality is difficult to state for the models of such substructural logics and further work will be also devoted to it from this study.

8 A New Tableau Method for MILL

From the conservativity result we previously mentioned in theorem 2.2, we can see multiplicative intuitionistic linear logic (MILL) as a subsystem of BI. Consequently, the restriction of the initial TBI system to the multiplicative connectives, i.e., the expansion rules of figure 16, directly provides a tableau method for MILL. There exist proof-search methods for (propositional) multiplicative linear logic (MLL) based on different notions like connections [11, 22], tableaux [25, 26] with prefixes or canonical proofs [1, 18]. They cannot be easily extended to MILL and the design of a tableau method with labels from the Urquhart’s semantics appears as an appropriate solution. The restriction of TBI to the multiplicatives leads to a suitable tableau system for MILL. It can be related to a tableau formulation of D’Agostino and Gabbay’s LKE tableau for the (I, ⊗, −∘) fragment[7]. As it corresponds to a first tableau method for MILL, we present the main points into details.

All definitions (complementary formulas, closed tableau, fulfilled formula, etc...) given for BI are restricted to MILL by discarding statements involving either the additive connectives, or the additive units. Since we keep the ∘ connective, the TBI/MILL calculus is mostly based on a restriction on propositions, i.e., propositions containing only multiplicatives. Therefore, as opposed to TBI/IL, the labelling algebra and the corresponding closure operator remain unchanged w.r.t. BI. The main difference is that we now deal with assertions whose left-hand side is necessarily a composition of two atomic labels. This comes from that the T ∗ rule is now the only rule that introduces assertions.

8.1 A tableau construction procedure for MILL

Let us recall the main definitions in the case of this restriction to MILL.

Definition 8.1. Let B be a tableau branch, a signed formula Sg X : x is fulfilled (or completely analyzed) in B, noted B ⊩ Sg X : x, if it satisfies one of the following conditions

1. B ⊩ F I : x iff 1 ≤ x ∉ \overline{Ass}(B)

2. B ⊩ F A ∗ B : x iff for any y, z ∈ D(B) such that yz ≤ x ∈ \overline{Ass}(B) either B ⊩ F A : y, or B ⊩ F B : z 3. B ⊩ F A −∗ B : x iff there exist y, xy ∈ D(B) such that both B ⊩ T A : y and B ⊩ F B : xy

4. B ⊩ T I : x iff 1 ≤ x ∈ \overline{Ass}(B)

5. B ⊩ T A ∗ B : x iff there exist y, z ∈ D(B) such that yz ≤ x ∈ \overline{Ass}(B) and both B ⊩ T A : y and B ⊩ T B : z

6. B ⊩ T A −∗ B : x iff for any y, xy ∈ D(B) either B ⊩ F A : y, or B ⊩ T B : xy

T A ∗ B : x ; ass : c_{i}c_{j} ≤ x ^{∗} ; \begin{matrix}T A : c_{i} \\ T B : c_{j} \end{matrix}  F A −∗ B : x ; \begin{matrix}T A : c_{i} \\ F B : xc_{i} \end{matrix}

F A ∗ B : x ; req : yz ≤ x ; F A : y  F B : z  \begin{matrix}T A −∗ B : x \\ F A : y & T B : xy \end{matrix}

∗ c_{i}, c_{j} are new constants

Figure 16: Expansion Rules for MILL

Definition 8.2. A tableau branch B is completed if it is open and every signed formula Sg A : x of B is fulfilled. A tableau is completed if it has a completed branch.

Lemma 8.1 (monotonicity). A completed branch B satisfies Kripke monotonicity, more precisely,

1) B ⊩ F A : x and y ≤ x ∈ \overline{Ass}(B) imply B ⊩ F A : y, and

2) B ⊩ T A : x and x ≤ y ∈ \overline{Ass}(B) imply B ⊩ T A : y.

Proof. By structural induction on Sg A : x.

Lemma 8.2 (consistency). If B is a completed branch, then, for any BI proposition A, we cannot have both B ⊩ T A : x and B ⊩ F A : x.

Proof. See the proof of lemma 4.5.

We give a tableau construction procedure that is an algorithm that, for a given formula A, builds a tableau sequence t_{1}, t_{2}, …, t_{n} until there exists a tableau t_{i} that is either closed or includes a completed branch. This procedure for MILL, that is called TBI/MILL, is the following: The initial signed formula is F A : 1 and it is marked unvisited. Repeat until T is closed or completed

if there is no unvisited formula Sg X : x in any open branch B then mark all πβ-formulas in all open branches as unvisited else mark Sg X : x as visited if Sg X : x is not fulfilled in B then if Sg X : x is of type πβ then expand Sg X : x with a label y for which the formula is not fulfilled else expand Sg X : x according to its type

As in TBI/IL, the πα rules, namely the F −∗ and T ∗ rules, require the introduction of new constants that can lead to infinite branches. Again, a key point is to propose liberalized versions of those rules which are justified by the completeness of MILL with respect to regular Kripke resource models, i.e., models for which the forcing relation satisfies the following regularity property [7]: whenever there exists a world satisfying a proposition A, there also exists a world, called A-characteristic, which is the least, w.r.t. the underlying preordering, to satisfy A. In this context, for the realization of a tableau branch in some Kripke resource model, we can assume that every constant introduced in a tableau branch refers to a characteristic world. For example, the √_{1} F ((p ∗ q) −∗ r)) −∗ (q −∗ (p −∗ r)) : 1

√_{4} T (p −∗ q) −∗ r : c_{1} √_{2} F q −∗ (p −∗ r) : c_{1}

\begin{matrix}T q : c_{2} \\ √_{3} F p −∗ r : c_{1}c_{2} \end{matrix}

\begin{matrix}T p : c_{3} \\ F r : c_{1}c_{2}c_{3} \end{matrix}

√_{5} F p ∗ q : c_{2}c_{3} ; req_{1} : c_{3}c_{2} ≤ c_{2}c_{3} ; \begin{matrix}F p : c_{3} \\ × \end{matrix}  \begin{matrix}F q : c_{2} \\ × \end{matrix}  \begin{matrix}T r : c_{1}c_{2}c_{3} \\ × \end{matrix}

Figure 17: Labelled Tableau for ((p ∗ q) −∗ r)) −∗ (q −∗ (p −∗ r))

constant a introduced in T A : a, F B : xa by the expansion of F A −∗ B : x is assumed to refer to an A-characteristic world.

Lemma 8.3. Let B be a tableau branch. The following liberalized rules,

F A −∗ B : x ; \begin{matrix}T A : a \\ F B : xa \end{matrix}  T A ∗ B : x ; ass : ab ≤ x ; \begin{matrix}T A : a \\ T B : b \end{matrix}

in which a (resp. b) is not new if T A : a (resp. T B : b) has been already introduced in B by a previous πα tableau expansion, are admissible in TBI/MILL.

Proof. Let K be a regular Kripke resource model ⟨ M, ⊧, ⟦–⟧ ⟩, we only prove the result for F −∗, the other case being similar. The soundness of the liberalized F −∗ is justified by the following semantical equivalence : x |̸= A −∗ B iff there exists an A-characteristic world a such that x • a |̸= B. The if case is obvious. For the only-if case, let us suppose that x |̸= A −∗ B. Then, there exists y such that y ⊧ A and x • y |̸= B. Since y ⊧ A, the regularity of ⊧ implies that there exists an A-characteristic world a, which implies a ⊑ y and, by order preservation, x • a ⊑ x • y. By Kripke monotonicity we finally have x • a |̸= B. Now, suppose that we have a realization ∥–∥ of B in K with T A : a and F A −∗ B : x in B. Then, ∥a∥ ⊧ A and ∥x∥ |̸= A −∗ B. Since ∥a∥ is assumed to be A-characteristic, it follows from ∥x∥ |̸= A −∗ B and our previous remarks that ∥x∥ • ∥a∥(= ∥xa∥) |̸= B, and then the expansion of a liberalized F −∗ preserves realizability.

Let us remark that, in the case of T A ∗ B : x, either the constant for A, or the one for B, or both can be reused. The assertion associated to the rule is not discarded. On the contrary, it adds more constraints on the reused constants. Let us also remark that lemma 8.3 implies that, once a πα formula has been expanded with some constant a, this constant can be reused for every subsequent occurrence of the same πα formula. For example, if we have already expanded F A −∗ B : x with T A : a, F B : xa, and we, later on, reach a point where we need to expand F A −∗ B : y, we can simply reuse a to produce F B : ya instead of introducing a new constant b. Then, by using the same constant for distinct occurrences of the same πα formula and distinct constants for distinct πα formulas, we can keep track of the expansion process inside the labels since then, the constants composing the label of a signed formula clearly identify the πα formulas from which it derives. As for BI^{⊥}, the semi-decision procedure given in subsection 8.1 can be improved into a decision procedure by taking both the liberalized rules and the notion of redundancy given in definition 4.7 into account.

8.2 Examples

In this section, we illustrate how to build proofs and countermodels in TBI/MILL. It is a new tableau method for MILL that allows to directly build countermodels in case of non-provability.

Let us illustrate its characteristics with the following examples. Figure 17 gives a tableau for the formula ((p∗q)−∗r))−∗(q−∗(p−∗r)). We obtain a tableau in which the three branches are closed and the formula is therefore provable in MILL. The first branch is closed due to the connection ⟨ T p : c_{3}, F p : c_{3} ⟩, the second is closed due to ⟨ T q : c_{2}, F q : c_{2} ⟩ and the third is closed due to ⟨ T r : c_{1}c_{2}c_{3}, F r : c_{1}c_{2}c_{3} ⟩. The second example, given in figure 18, gives an open tableau for the formula ((p∗q)−∗r))−∗(q−∗(p−∗r)), which means that it is not provable in MILL. Since we have no πβ formulas in the tableau, every formula is immediately fulfilled after it has been decomposed, and we finally obtain an open branch which is therefore also a finite completed branch.

√_{1} F p −∗ ((p ∗ q) −∗ p) : 1

\begin{matrix}T p : c_{1} \\ √_{2} F (p ∗ q) −∗ p : c_{1} \end{matrix}

\begin{matrix}√_{3} T p ∗ q : c_{2} \\ F p : c_{1}c_{2} \end{matrix}

ass_{1} : c_{3}c_{4} ≤ c_{2} ; \begin{matrix}T p : c_{3} \\ T q : c_{4} \end{matrix}

Figure 18: Labelled Tableau for p −∗ ((p ∗ q) −∗ p)

Let us see how to construct a countermodel from such a completed branch. Such a construction, in the case of MILL, exactly follows the steps given for BI^{⊥} in definition 4.5. For the example of figure 18, the construction results in the set of worlds.

M = { 1, c_{1}, c_{2}, c_{3}, c_{4}, c_{1}c_{2}, c_{1}c_{3}, c_{1}c_{4}, c_{3}c_{4}, c_{1}c_{3}c_{4}, π }

The preordering ⊑ is defined by c_{3}c_{4} ⊑ c_{2}, c_{1}c_{3}c_{4} ⊑ c_{1}c_{2} and (∀m ∈ M)(m ⊑ π).

Moreover, the • operation is defined by the following table

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

The forcing relation ⊧ is parametrized by the following atomic interpretation

\begin{matrix}x & p & q \\ ⟦x⟧ & \{ c_{1}, c_{3}, π \} & \{ c_{4}, π \} \end{matrix}

It is routine to check that c_{1} ⊧ p (1) and c_{1} |̸= (p ∗ q) −∗ p (2).

(1) is immediate by definition of the forcing relation. For (2), on one hand, we have that c_{2} ⊧ p ∗ q because c_{3} ⊧ p, c_{4} ⊧ q and c_{3}c_{4} ⊑ c_{2}. On the other hand, we have c_{1}c_{2} |̸= p because c_{1}c_{2} ∉ ⟦p⟧. Therefore, c_{1} |̸= (p ∗ q) −∗ p. In further work, we aim to compare our semantic tableau method with other recent proof-search methods that build countermodels in ILL but also to deal with different semantics of ILL that are based on monoids, Petri nets or resources [12, 14]. Proof-search in MILL has been recently studied with labelled proof nets [3] and also related to connection methods in linear logic [11]. These new (resource) semantics could lead to new definitions of labels and then improve such labelled proof-search methods. Moreover, we will analyze the relationships, mainly from a countermodel construction perspective with the labelled tableau method for MILL based on the so-called simple semantics [36]. Both methods emphasize the power of labels to capture semantical interactions between connectives. We could propose some refinements of the semantics from the study of this labelled method that emphasizes the role of requirements and assertions on labels. The requirements, respectively the assertions could be seen as questions, respectively answers that have to interact and could be related to game semantics proposals for linear logic [4]. We will study the actual impact of the choice of different semantics for the countermodel generation process and thus propose new appropriate resource semantics for proof-search with countermodel generation facility in such substructural logics.

8.3 Properties of the MILL labelled calculus

Theorem 8.1 (soundness). Let A be a proposition of MILL, if there exists a closed tableau sequence for A in TBI/MILL, then A is valid in Urquhart semantics.

Proof. See the proof of theorem 4.1 with restrictions to MILL.

Theorem 8.2 (completeness). Let A be a proposition of MILL, if A is valid in Urquhart semantics then, there exists a closed tableau sequence for A in TBI/MILL.

Proof. See the proof of theorem 4.2 with restrictions to MILL.

Theorem 8.3 (finite model property). Let A be a proposition of MILL, if A is not valid in Urquhart semantics then there exists a finite model in which A is not satisfied.

Proof. See the proof of theorem 4.3 with restrictions to MILL.

There have been several attempts to show the finite model property for fragments of some substructural logics, for example, for fragments of intuitionistic linear logic [6, 31] like MILL. For instance, the method of logical congruence [23] has been adapted to intuitionistic phase semantics [31]. Here we have deduced a new result that is the finite model property of MILL w.r.t. Urquhart semantics, the labels allowing to directly generate countermodels in terms of this “resource semantics”. Let us mention that a similar approach has been recently developed with respect to a monoid-based semantics [36].

Both adaptations of TBI^{⊥} to IL and MILL illustrate that the use of labelled deductive systems and then the study of appropriate resource semantics are good starting points to study the countermodel generation for substructural and mixed logics like BI. Further works will be devoted to the definition of new resource semantics for such logics with completeness proofs by proof-search and generation of usable countermodels [14].

9 Conclusion

In this paper we have designed a labelled tableau calculus for the propositional BI logic, more precisely BI^{⊥}. This new logic is a resource-aware logic with an emphasis on interferences between resources that has been recently studied as an assertion language for reasoning about mutable data structures [20] and also for logic programming [2]. It seems to be a well suited logical foundation, in order to specify and prove some particular properties of programs or systems. Here we focus on proof-search in BI logic and define a labelled calculus for BI^{⊥} that 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^{⊥} w.r.t. the Kripke resource semantics. The proof-search method is mainly based on the BI resource semantics and the introduction of specific labels and constraints that capture the essence of this semantics into the proof-search process. Moreover, these concepts allow to generate countermodels in a simple way. Similar work has been recently done for MILL with another simple semantics [36]. Moreover, we have adapted, by restriction, our labelled tableau method to IL and MILL logics, and thus obtained new semantic tableaux methods for both logics with easy countermodel construction. Comparisons with other proof-search methods confirm the power and the usefulness of such labelled calculi tailored from a given resource semantics. In fact, labels and constraints are appropriate for proofsearch in such a mixed logic, taking into account the interaction and interference between different kinds of connectives. We have studied the representation and resolution of label constraints during the tableau construction by defining and using dependency graphs from which countermodels can be extracted. We have also recently defined labelled calculi for Mixed Linear Logic in which commutative and noncommutative connectives cohabit [17] and also used labels and dependency graphs as key structures for semantic proof-search. In this context, such structures are also appropriate to capture the interactions between different kinds of connectives. In order to analyze some algorithmic aspects of our semantics method, we have proposed another labelled calculus with free variables in labels. It provides a way to control the introduction of new constants, and thus, to limit the syntactic complexity of the labels. It leads to a better efficiency of the proof-search but to a more difficult generation of countermodels. Recently, we have studied how to extend these labelled calculi to propositional BI (with ⊥) including the countermodel generation facility. A potential difficulty consists in relating labels with the topological resource models or the Grothendieck sheaf-theoretic models for which completeness of BI has been proved [35]. In fact, we have defined a labelled tableau method for BI, that extends the presented one and thus to prove the decidability of the propositional BI logic and the finite model property w.r.t. the above mentioned semantics [16]. Moreover, we have also recently shown that our approach based on labels and constraints can also be applied to design a connection method for BI logic [15]. The study of labels, constraints and dependency graphs will lead to further works in order to define new resource semantics for BI and its subsystems. Moreover, we will study such new semantic proof-search methods for a classical version of BI that has been proposed as an assertion language for mutable data structures [20] and the possible connections with recent verification formalisms that capture the informal local reasoning in pointer programs [28]. The idea of dealing with labelled formulas is related to the LDS methodology that has been devised to provide uniform deductive systems [10] for a wide range of substructural logics like linear, relevance and intuitionistic logics [5, 7]. But, so far, the problem of generating countermodels in such frameworks has not been studied. In contrast with this approach, we have designed, starting from a given resource semantics, a specialized labelled tableau framework, for BI and its subsystems IL and MILL, based on particular labels and constraints for which the countermodel construction is an integrated part of the proof-search process. An interesting point will be to study, in other logics, the relationships resource semantics and corresponding labelled proof-search methods and, more precisely, if our approach could be applied or generalized to other logics for which well-defined resource semantics are defined.

References

[1] J.M. Andreoli. Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation, 2(3):297–347, 1992.

[2] 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.

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

[4] A. Blass. A Game Semantics for Linear Logic. Annals of Pure and Applied Logic, 56:183–220, 1992.

[5] K. Broda, M. Finger, and A. Russo. Labelled Natural Deduction for Substructural Logics. Logic Journal of the IGPL, 7(3):283–318, 1999.

[6] W. Buszkowski. The finite model property for BCI and related systems. Studia Logica, 57:303–323, 1996.

[7] 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.

[8] R. Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57:795–807, 1992.

[9] M. Fitting. First-Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer Verlag, 1990.

[10] D.M. Gabbay. Labelled Deductive Systems, Volume I - Foundations. Oxford University Press, 1996.

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

[12] D. Galmiche and D. Larchey-Wendling. Provability in Intuitionistic Linear Logic from a New Interpretation on Petri Nets - extended abstract. Electronic Notes in Theoretical Computer Science, 17, 1998.

[13] D. Galmiche and D. Larchey-Wendling. Structural Sharing and Efficient Proof-search in Propositional Intuitionistic Logic. In Asian Computing Science Conference, ASIAN’99, LNCS 1742, pages 101–112, Phuket, Thailand, December 1999.

[14] D. Galmiche and D. Larchey-Wendling. Quantales as completions of ordered monoids: revised semantics for Intuitionistic Linear Logic. Electronic Notes in Theoretical Computer Science, 35, 2000.

[15] D. Galmiche and D. Méry. Connection-based proof search in propositional BI logic. In 18th Int. Conference on Automated Deduction, CADE-18, LNAI 2392, pages 111–128, 2002. Copenhagen, Danemark.

[16] D. Galmiche, D. Méry, and D. Pym. Resource Tableaux (extended abstract). In 16th Int. Workshop on Computer Science Logic, CSL 2002, LNCS 2471, pages 183–199, September 2002. Edinburgh, Scotland.

[17] D. Galmiche and J.M. Notin. Calculi with Dependency Relations for Mixed Linear Logic. In International Workshop on Logic and Complexity in Computer Science, LCCS’2001, pages 81–102, Créteil, France, 2001.

[18] D. Galmiche and G. Perrier. On Proof Normalization in Linear Logic. Theoretical Computer Science, 135(1):67–110, 1994.

[19] 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.

[20] 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.

[21] S. Ishtiaq and D. Pym. Kripke resources models of a dependently-typed bunched λ-calculus. In 13th Int. Workshop on Computer Science Logic, CSL’99, LNCS 1683, pages 235–249, Madrid, Spain, 1999. September.

[22] C. Kreitz, H. Mantel, J. Otten, and S. Schmitt. Connection-based proof construction in Linear Logic. In 14th Int. Conference on Automated Deduction, CADE-14, LNCS 1249, pages 207–221, Townsville, North Queensland, Australia, 1997.

[23] Y. Lafont. The finite model property for various fragments of linear logic. Journal of Symbolic Logic, 62(4):1202–1208, 1997.

[24] D. Larchey-Wendling, D. Méry, and D. Galmiche. STRIP: Structural sharing for efficient proofsearch. In First International Joint Conference on Automated Reasoning, IJCAR 2001, LNCS 2083, pages 696–700, Siena, Italy, 2001.

[25] H. Mantel and J. Otten. linTAP : A Tableau Prover for Linear Logic. In Int. Conference on Analytic Tableaux and Related Methods, TABLEAUX’99, LNCS 1617, pages 216–231, Saratoga Springs, NY, USA, 1999.

[26] R.K. Meyer, M.A. McRobbie, and N. Belnap. Linear Analytic Tableaux. In 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNCS 918, pages 278–293, St Goar am Rhein, Germany, 1995.

[27] P. O’Hearn. Resource interpretations, bunched implications and the αλ-calculus. In 4th Int. Conference on Typed Lambda Calculi and Applications, TLCA’99, LNCS 1581, pages 258–279, L’Aquila, Italy, 1999.

[28] P. O’Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In 15th Int. Workshop on Computer Science Logic, CSL 2001, LNCS 2142, pages 1–19, Paris, France, 2001.

[29] P.W. O’Hearn and D. Pym. The Logic of Bunched Implications. Bulletin of Symbolic Logic, 5(2):215– 244, 1999.

[30] M. Okada and K. Terui. Completeness proofs for linear logic based on proof search method (preliminary report). In Type theory and its applications to computer systems, pages 57–75, RIMS, Kyoto University, 1998.

[31] M. Okada and K. Terui. The finite model property for various fragments of intuitionistic linear logic. Journal of Symbolic Logic, 64(2):790–802, 1999.

[32] H. Ono. Decidability and Finite Model Property of Substructural Logics. In The Tbilisi Symposium on Logic, Language and Computation, pages 262–274. CSLI Publications, 1997.

[33] L. Pinto and R. Dyckhoff. Loop-free construction of counter-models for intuitionistic propositional logic. In Behara and al., editors, Symposia Gaussiana, pages 225–232, 1995.

[34] 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.

[35] D.J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications, volume 26 of Applied Logic Series. Kluwer Academic Publishers, 2002.

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

[37] A. Urquhart. Semantics for Relevant Logic. Journal of Symbolic Logic, 37:159–169, 1972.

[38] A. Voronkov. Proof-search in intuitionistic logic based on constraint satisfaction. In 5th Int. Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 1071, pages 312–327, Terrasini, Italy, May 1996.