*Example 7 (Structural variants of* iMALL*).* Adding combinations of contraction C and / or weakening W for *arbitrary formulas* to additive-multiplicative intuitionistic linear logic (iMALL) yields, respectively, propositional intuitionistic logic ILP = iMALL + {C, W}, and the intuitionistic versions of affine linear logic aLL = iMALL + W and relevant logic R = iMALL + C. For the sake of presentation we overload the notation and use the connectives of linear logic also for these logics. In order to embed the logics above into acLLΣ, let α ∈ {ILP, aLL, R} and consider modalities ! α with f(α) = {E,A1,A2} ∪ A where A ⊆ {C, W} is the set of axioms whose corresponding rules are in α. The translation τα prefixes *every subformula* with the modality ! α . For L ∈ {ILP, aLL, R} it is then straightforward to show that a structured sequent S is cut-free derivable in L iff its translation τα(S) is cut-free derivable in the logic described by ({α}, -, f) with the obvious relation, and f as given above.

*Example 8 (Structural variants of* FNL*).* Following the same script as above and starting from FNL:

	- If A = {A1,A2}, then we obtain the system FL;
	- If A = {E,A1,A2} then the resulting system corresponds to iMALL.
	- Adding C, W as options to A will result the affine/relevant versions of the systems above.

#### **2.2 An Example in Linguistics**

Since its inception, Lambek calculus [29] has been applied to the modeling of natural language syntax by means of categorial grammars. In a categorial grammar, each word is assigned one or several Lambek formulas, which serve as syntactic categories. For a simple example, John and Mary are assigned np ("noun phrase") and lovesgets

(np → s) ← np. Here s stands for "sentence", and loves is a transitive verb, which lacks noun phrases on both sides to become a sentence. Grammatical validity of "John loves Mary" is supported by derivability of the sequent np,(np → s) ← np, np ⇒ s. Notice that this derivability keeps valid also in the non-associative setting, if the correct nested structure is provided: (np,((np → s) ← np, np)) ⇒ s.

The original Lambek calculus L is associative. In some cases, however, associativity leads to over-generation, *i.e.*, validation of grammatically incorrect sentences. Lambek himself realized this and proposed the non-associative calculus NL in [30]. We will illustrate this issue with the example given in [38, Sect. 4.2.2]. The syntactic category assignment is as follows (where n stands for "noun"):

$$\begin{array}{c} \text{Words} \mid \text{Types} \\ \text{the } np \leftarrow n \\ \text{Hulk } n \\ \text{is } (np \rightarrow s) \leftarrow (n \leftarrow n) \\ \text{green, irreducible } n \leftarrow n \end{array}$$

With this assignment, sentences "The Hulk is green" and "The Hulk is incredible" are correctly marked as valid, by deriving the sequent

$$(np \gets n, n), ((np \to s) \gets (n \gets n), n \gets n) \Rightarrow s$$

However, in the associative setting the sequent for the phrase "The Hulk is green incredible,"which is grammatically incorrect, also becomes derivable:

$$(np \leftarrow n, n, (np \rightarrow s) \leftarrow (n \leftarrow n), n \leftarrow n, n \leftarrow n \Rightarrow s, )$$

essentially due to derivability of n ← n, n ← n ⇒ n ← n.

In other situations, however, associativity is useful. Standard examples include handling of dependent clauses, *e.g.*, "the girl whom John loves," which is validated as a noun phrase by the following derivable sequent:

$$np \leftarrow n, n, (n \rightarrow n) \leftarrow (s \leftarrow np), np, (np \rightarrow s) \leftarrow np \Rightarrow np$$

Here (n → n) ← (s ← np) is the syntactic category for who.

Our subexponential extension of NL, however, handles this case using local associativity instead of the global one. Namely, the category for whom now becomes (n → n) ← (s ← ! anp), where ! a is a subexponential which allows the A2 rule, and the following sequent is happily derivable:

$$np \gets n, (n, ((n \to n) \gets (s \gets ! ^
perp), (np, (np \to s) \gets np))) \Rightarrow np$$

The necessity of this more fine-grained control of associativity, instead of a global associativity rule, is seen via a combination of these examples. Namely, we talk about sentences like "The superhero whom Hawkeye killed was incredible" and "... was green". With ! a, each of them is handled in the same way as the previous examples:

$$\begin{aligned} ((np \leftarrow n, (n, ((n \rightarrow n) \leftarrow (s \leftarrow ! "np), (np, (np \rightarrow s) \leftarrow np)))),\\ ((np \rightarrow s) \leftarrow (n \leftarrow n), n \leftarrow n) \Rightarrow s. \end{aligned}$$

On one hand, without ! a this sequent cannot be derived in the non-associative system. On the other hand, if we make the system globally associative, it would validate incorrect sentences like "The superhero whom Hawkeye killed was green incredible."

### **3 Some Undecidability Results**

Non-associativity makes a significant difference in decidability and complexity matters. For example, while L is NP-complete [47], NL is decidable in polynomial time [1,14].

For our system acLLΣ, its decidability or undecidability depends on its signature Σ. In fact, we have a family of different systems acLLΣ, with Σ as a parameter. Recall that the subexponential signature Σ controls not just the number of subexponentials and the preorder among them. More importantly, it dictates, for each subexponential, which structural rules this subexponential licenses. If for every i ∈ I we have C ∈/ f(s), that is, no subexponential allows contraction, then acLLΣ is clearly decidable, since the cut-free proof search space is finite. Therefore, for undecidability it is necessary to have at least one subexponential which allows contraction.

For a non-associative system with only one fully-powered exponential modality s (that is, f(s) = {E, C, W,A1,A2}), undecidability was proven in a preprint by Tanaka [51], based on Chvalovsky's [ ´ 11] result on undecidability of the finitary consequence relation in FNL.

In this section, we prove two undecidability results. The first one is a refinement of Tanaka's result: We establish undecidability with at least one subexponential which allows contraction and weakening (commutativity/associativity are optional), in a subsystem containing only the additive connective ⊕ and the multiplicatives ⊗ and →.

The second undecidability result is for the minimalistic, purely multiplicative fragment, which includes only → (not even ⊗). As a trade-off, however, it requires two subexponentials: the "main" one, which allows contraction, exchange, and associativity (weakening is optional), and an "auxiliary" one, which allows only associativity.

It should be noted that this undecidability result is orthogonal to Tanaka's [51], and the proof technique is essentially different. Indeed, Chvalovsky's undecidability ´ theorem does not hold for the non-associative Lambek calculus without additives, where the consequence relation is decidable [7].

Finally, we observe that *if* the intersection of these systems is decidable (which is still an open question), then our two undecidability results are *incomparable:* we have two undecidable fragments of acLLΣ, but their common part, which includes only divisions and one exponential, would be decidable.

#### **3.1 Undecidability with Additives and One Subexponential**

We are going to derive the next theorem from undecidability of the finitary consequence relation in FNL [11]. Recall that FNL is, in fact, the fragment of acLLΣ without subexponentials (that is, with an empty I).

**Theorem 9.** *If there exists such* s ∈ I *that* f(s) ⊇ {C, W}*, then the derivability problem in* acLLΣ *is undecidable. Moreover, this holds for the fragment with only* ⊗*,* →*,* ⊕, ! s *.*

In fact, using C and W, one can also derive A1, A2, E1, and E2. Therefore, if f(s) ⊇ {C, W}, then ! s is actually a full-power exponential modality. (In the proof of Theorem 9 below, we use only W and C rules, in order to avoid confusion.) However, Theorem 9 does not directly follow from undecidability of propositional linear logic [32], because here the basic system is non-associative and non-commutative, while linear logic is both associative and commutative. Thus, we need a different encoding for undecidability.

Let **Φ** be a finite set of FNL sequents. By FNL(**Φ**) let us denote FNL extended by adding sequents from **Φ** as additional (non-logical) axioms. In general, FNL(**Φ**) does not enjoy cut-elimination, so mcut is kept as a rule of inference in FNL(**Φ**). A sequent Γ ⇒ F is called *a consequence of* **Φ** if this sequent is derivable in FNL(**Φ**).

**Theorem 10 (Chvalovsky´** [11]**).** *The consequence relation in* FNL *is undecidable, that is, there exists no algorithm which, given* **Φ** *and* Γ ⇒ F*, determines whether* Γ ⇒ F *is a consequence of* **Φ***. Moreover, undecidability keeps valid when* **Φ** *and* Γ ⇒ F *are built from variables using only* ⊗ *and* ⊕*.*

Now, in order to prove Theorem 9, we internalize **Φ** into the sequent using ! s , assuming f(s) ⊇ {C, W}.

First we notice that we may suppose, without loss of generality, that all sequents in **Φ** are of the form ⇒ A, that is, have empty antecedents. Namely, each sequent of the form Π ⇒ B can be replaced by ⇒ ( Π) → B, where Π is obtained from Π by replacing each comma with ⊗. Indeed, these sequents are derivable from one another: from Π ⇒ B to ⇒ ( Π) → B we apply a sequence of ⊗L followed by → R, and for the other direction we apply a series of cuts, first with ( Π,( Π) → B) ⇒ B, and then with (F, G) ⇒ F ⊗ G several times, for the corresponding subformulas of Π. The following embedding lemma ("modalized deduction theorem") holds.

  Notice that C and W can be applied to !Φ as a whole; this is easily proven by induction on n.

For the "only if" direction let us take the derivation of Γ ⇒ F in FNL(**Φ**) (with cuts) and replace each sequent of the form Δ ⇒ G in it with (!Φ, Δ) ⇒ G, and each sequent of the form ⇒ G with !Φ ⇒ G. The translations of non-logical axioms from **Φ** are derived as follows:

$$\begin{array}{c} \overline{A\_i \Rightarrow A\_i} \quad \text{init} \\ \frac{!^s A\_i \Rightarrow A\_i}{!^\Phi \Rightarrow A\_i} \text{ } \mathsf{W}, \ n-1 \text{ times} \end{array}$$

Translations of axioms init and 1R are derived from the corresponding original axioms by W, n times; -R remains valid.

Rules ⊗L, ⊕L, ⊕Ri, &Li, &R, and 1L remain valid. For → L, ← L, and mcut we contract !Φ as a whole:

$$\frac{\begin{array}{l} (\!\langle \Phi, \Delta \rangle \Rightarrow F \quad \langle !\Phi, \varGamma \{ \!\langle \Phi \rangle \} \Rightarrow H \end{array}}{\begin{array}{l} (\!\langle \Phi, \varGamma \{ \!\langle \langle \Phi, \Delta \rangle, F \to G \rangle \} \rangle \Rightarrow H \end{array}} \rightarrow L \quad \frac{\begin{array}{l} (\!\langle \Phi, \Delta \rangle \Rightarrow F \quad \langle !\Phi, \varGamma \{ \!\langle \Phi, \varGamma \{ \!\langle \Phi, \bot \} \rangle \} \Rightarrow C \end{array}}{\begin{array}{l} (\!\langle \Phi, \varGamma \{ \!\langle \!\langle \Phi, \Delta \rangle \} \ldots \, \{ \!\langle \!\langle \Phi, \bot \rangle \} \} \Rightarrow C \end{array}} \begin{array}{l} \mathfrak{m} \text{cut} \\ \text{ $\langle \Phi, \varGamma \{ \!\langle \Phi, \bot \} \rangle \exists \, \langle \!\langle \Phi, \bot \rangle \rangle$ } \\ \mathfrak{m} \text{cut} \end{array}$$

For ⊗R, → R, and ← R, we combine contraction and weakening:

$$\frac{\frac{(!\Phi,\varGamma\_{1})\Rightarrow F}{((!\Phi,\varGamma\_{1}),(!\Phi,\varGamma\_{2}))\Rightarrow F\otimes G}\circledast R}{\frac{(!\Phi,(!\Phi,\varGamma\_{1}),(!\Phi,\varGamma\_{2}))\Rightarrow F\otimes G}{(!\Phi,((!\Phi,\varGamma\_{1}),(!\Phi,\varGamma\_{2})))\Rightarrow F\otimes G}\hph\_{1}}\hph\_{1}\quad\frac{\frac{(!\Phi,(F,\varGamma))\Rightarrow G}{(!\Phi,(F,(!\Phi,\varGamma))\Rightarrow G}}{\mathsf{C}}\hph\_{1}}{\mathsf{C}}\hph\_{1}$$

Notice that our original derivation was in FNL(**Φ**), so it does not include rules operating subexponentials.

For the "if" direction we take a cut-free proof of (!Φ, Γ) ⇒ F in acLLΣ and erase all formulas which include the subexponential. In the resulting derivation tree all rules and axioms, except those which operate ! s , remain valid. Structural rules for ! s trivialize (since the !-formula was erased). The ! s R rule could not have been used, since we do not have positive occurrences of ! s F, and our proof is cut-free.

Finally, der translates into

$$\frac{\Gamma\{A\_i\} \Rightarrow G}{\Gamma\{\} \Rightarrow G}$$

This is modeled by cut with one of the sequents from **Φ**:

$$\frac{\Rightarrow A\_i \quad \Gamma\{A\_i\} \Rightarrow G}{\Gamma\{\} \Rightarrow G} \text{ און} \text{ און}$$

Thus, we get a correct derivation in FNL(**Φ**).

Theorem 10 and Lemma 11 immediately yield Theorem 9.

#### **3.2 Undecidability Without Additives and with Two Subexponentials**

**Theorem 12.** *If there are* a, c ∈ I *such that* f(a) = {A1,A2} *and* f(c) ⊇ {C, E,A1,A2}*, then the derivability problem in* acLLΣ *is undecidable. Moreover, this holds for the fragment with only* →*,* ! a*, and* ! c *.*

Remember from Example 8 that SMALCΣ [21] denotes the extension of FL with subexponentials. The undecidability theorem above is proved by encoding the one-division fragment of SMALCΣ containing one exponential c such that f(c) ⊇ {C, E}. It turns out that that such a system is undecidable.

**Theorem 13 (Kanovich et al.** [22,23]**).** *If there exists such* c ∈ I *that* f(c) ⊇ {C, E}*, then the derivability problem in* SMALCΣ *is undecidable. Moreover, this holds for the fragment with only* → *and* ! c *.*

Observe that SMALCΣ can be obtained from acLLΣ by adding "global" associativity rules:

$$\frac{\Gamma\{ ( (\Delta\_1, \Delta\_2), \Delta\_3 ) \} \Rightarrow G}{\Gamma\{ (\Delta\_1, (\Delta\_2, \Delta\_3)) \} \Rightarrow G} \qquad \frac{\Gamma\{ (\Delta\_1, (\Delta\_2, \Delta\_3)) \} \Rightarrow G}{\Gamma\{ ( (\Delta\_1, \Delta\_2), \Delta\_3) \} \Rightarrow G}$$

The usual formulation of SMALCΣ, of course, uses sequences of formulas instead of nested structures as antecedents. The alternative formulation, however, would be more convenient for us now. It will be also convenient for us to regard all subexponentials in SMALCΣ to be associative, that is, f(s) ⊇ {A1,A2} for each s ∈ I.

In order to embed SMALCΣ into acLLΣ, we define two translations, A!− and A!+, by mutual recursion:

$$\begin{aligned} &z^{!-} = !^{a}z & \qquad z^{!+} = z & \text{where } z \text{ is a variable, } 1, \text{ or } \top\\ &(A \to B)^{!-} = !^{a}(A^{!+} \to B^{!-}) & (A \to B)^{!+} = A^{!-} \to B^{!+}\\ &(B \gets A)^{!-} = !^{a}(B^{!-} \gets A^{!+}) & (B \gets A)^{!+} = B^{!+} \gets A^{!-}\\ &(A \oplus B)^{!-} = !^{a}(A^{!-} \oplus B^{!-}) & (A \oplus B)^{!+} = A^{!+} \oplus B^{!+} & \text{where } \oplus \in \{\otimes, \oplus, \&\}\\ &(!^{a}A)^{!-} = !^{a}(A^{!-}) & (!^{a}A)^{!+} = !^{a}(A^{!+}) \end{aligned}$$

Informally, our translation adds a ! a over any formula (not only over atoms) of negative polarity, unless this formula was already marked with a ! s . Thus, all formulae in antecedents would begin with either the new subexponential ! a or one of the old subexponentials ! s , and all these subexponentials allow associativity rules A1 and A2.

**Lemma 14.** *A sequent* A1,...,An ⇒ B *is derivable in* SMALCΣ *if and only if its translation* (...(A!− 1 , A!− 2 ),...,A!− n ) ⇒ B!+ *is derivable in* acLLΣ*.*

*Proof.* For the "only if" part, let us first note that each formula A!− i is of the form ! s F and A1,A2 ∈ f(s). Indeed, either s is an "old" subexponential label (for which we added A1,A2) or s = a. Thus brackets can be freely rearranged in the antecedent.

Now we take a cut-free proof of A1,...,An ⇒ B in SMALCΣ and replace each sequent in it with its translation. Right rules for connectives other than subexponentials, i.e., ⊗R, ⊕Ri, &R, → R, and ← R, remain valid as they are, up to rearranging brackets in antecedents. For ! i R, we notice that the translation of a formula of the form ! j F, where j i, is also a formula of the form ! j F . Thus, this rule also remains valid. The same holds for the dereliction rule der, because (!i F)!− is exactly ! i (F!−). Finally, the "old" structural rules (exchange, contraction, weakening) also remain valid (up to rearranging of brackets), since ! i F gets translated into ! i (F!−), which enjoys the same structural rules.

For the other left rules, we need to derelict ! a first, and then perform the corresponding rule application. Rearrangement of brackets, if needed, is performed below dereliction or above the application of the rule in question.

The "if" part is easier. Given a derivation of (...(A!− 1 , A!− 2 ),...,A!− n ) ⇒ B!+ in acLLΣ, we erase ! a everywhere, and consider it as a derivation in SMALCΣ. Associativity rules for the erased ! a (which are the only structural rules for this subexponential) keep valid, because now associativity is global. Dereliction and right introduction for ! a trivialize. All other rules, which do not operate ! a, remain as they are. Thus, we get a derivation of A1,...,An ⇒ B in SMALCΣ, since erasing ! a makes our translations just identical.

#### **4 Related Work and Conclusion**

In this paper, we have presented acLLΣ, a sequent-based system for non-associative, non-commutative linear logic with subexponentials. Starting form FNL, we modularly and uniformly added rules for exchange, associativity, weakening and contraction, which can be applied with the subexponentials having with the respective features. This allows for the application of structural rules locally, and it conservatively extends well known systems in the literature, continuing the path of controlling structural properties started by Girard himself [16].

Another approach to combining associative and non-associative behavior in Lambek-style grammars is the framework of *the Lambek calculus with brackets* by Morrill [39,40] and Moortgat [34]. The bracket approach is dual to ours: there the base system is associative, and brackets, which are controlled by bracket modalities, introduce local non-associativity. Both the associative Lambek calculus and the nonassociative Lambek calculus can be embedded into the Lambek calculus with brackets: the former is just by design of the system and the latter was shown by Kurtonina [26] by constructing a translation.

From the point of view of generative power, however, the (associative) Lambek calculus with brackets is weaker than the non-associative system with subexponentials, which is presented in this paper. Namely, as shown by Kanazawa [19], grammars based on the Lambek calculus with brackets can generate only context-free languages. In contrast, grammars based on our system with subexponentials go beyond context-free languages, even when no subexponential allows contraction (subexponentials allowing contraction may lead to undecidability, as shown in the last section).

As a quick example, let us consider a subexponential ! ae which allows both associativity (A1 and A2) and exchange (E). If we put this subexponential over any (sub)formula, the system becomes associative and commutative. Using this system, one can describe the non context-free language MIX3, which contains all non-empty words over {a, b, c}, in which the numbers of a, b, and c are equal. Indeed, MIX3 is the permutation closure of the language {(abc)n | n ≥ 1}. The latter is regular, therefore context-free, and therefore definable by a Lambek grammar. The ability of our system to go beyond context-free languages is important from the point of view of applications, since there are known linguistic phenomena which are essentially non-context-free [49].

Regarding decidability, let us compare our results with the more well-known associative non-commutative and associative commutative cases.

In the associative and commutative case the situation is as follows. In the presence of additives, the system is known to be undecidable with one exponential modality [32]. Without additives, we get MELL, the (un)decidability of which is a well-known open problem [50]. However, with two subexponentials MELL again becomes undecidable [9]. Thus, we have the same trade-off as in our non-associative non-commutative case: for undecidability one needs either additives, or two subexponentials.

Our results help to shed some light in the (un)decidability problem for the spectrum of logical systems surrounding MELL/FNL, allowing for a fine-grained analysis of the problem, specially the trade-offs on connectives and subexponentials for guaranteeing (un)decidability.

There is a lot to be done from now on. First of all, we would like to analyze better the minimalist fragment of acLLΣ containing only implication and one fully-powered subexponential, as it seems to be crucial for understanding the lower bound of undecidability (or the upper bound of decidability). Second, one should definitely explore more the use of acLLΣ in modeling natural language syntax. The examples in Sect. 2.2 show how to locally combine sentences with different grammatical characteristics, and the MIX3 example above illustrates how that can be of importance. That is, it would be interesting to have a formal study about acLLΣ and categorial grammars. Third, we plan to investigate the connections between our work and Adjoint logic [48] as well as with Display calculus [5,12]. Finally, we intend to study proof-theoretic properties of acLLΣ, such as normalization of proofs (*e.g.* via focusing) and interpolation.

**Acknowledgements.** We are grateful for the useful suggestions from the anonymous referees. We would like to thank L. Beklemishev, M. Moortgat, and C. Retore for their inspiring and ´ helpful comments regarding an approach based on non-associativity.

# **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# **Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices**

Ori Lahav1 and Yoni Zohar2(B)

1 Tel Aviv University, Tel Aviv-Yafo, Israel 2 Bar Ilan University, Ramat Gan, Israel<EMAIL_ADDRESS>
**Abstract.** A four-valued semantics for the modal logic K is introduced. Possible worlds are replaced by a hierarchy of four-valued valuations, where the valuations of the first level correspond to valuations that are legal w.r.t. a basic non-deterministic matrix, and each level further restricts its set of valuations. The semantics is proven to be effective, and to precisely capture derivations in a sequent calculus for K of a certain form. Similar results are then obtained for the modal logic KT, by simply deleting one of the truth values.

## **1 Introduction**

Propositional modal logics extend classical logic with *modalities*, intuitively interpreted as necessity, knowledge, or temporal operators. Such extensions have several applications in computer science and artificial intelligence (see, e.g., [7,9,13]).

The most common and successful semantic framework for modal logics is the so called *possible worlds semantics*, in which each world is equipped with a twovalued valuation, and the semantic constraints regarding the modal operators consider the valuations in *accessible* worlds. While this has been the gold standard for modal logic semantics for many years, alternative semantic frameworks have been proposed. One of these approaches, initiated by Kearns [10], is based on an infinite sequence of sets of valuations in a non-deterministic many-valued semantics. Since then, several non-deterministic many-valued semantics, without possible worlds, were developed for modal logics (see, e.g., [4,8,12,14]). The current paper is a part of that body of work. Having an alternative semantic framework for modal logics, different than the common possible worlds semantics, has the potential of exposing new intuitions and understandings of modal logics, and also to form the basis to new decision procedures.

Our main contribution is a four-valued semantics for the modal logic K. The key characteristic of the semantics that we present is *effectiveness*: when checking

We thank the anonymous reviewers for their useful feedback. This research was supported by NSF-BSF (grant number 2020704), ISF (grant numbers 619/21 and 1566/18), and the Alon Young Faculty Fellowship.

c The Author(s) 2022

J. Blanchette et al. (Eds.): IJCAR 2022, LNAI 13385, pp. 468–485, 2022. https://doi.org/10.1007/978-3-031-10769-6\_28

for the entailment of a formula ϕ from a set Γ of formulas in K, it suffices to only consider *partial* models, defined over the subformulas of Γ and ϕ. To the best of our knowledge, this is the first effective Nmatrices-based semantics for K. Such a semantics has the potential of being subject to reductions to classical satisfiability [3], as it is based on finite-valued truth tables, and thus improving the performance of solvers for modal logic by utilizing off-the-shelf SAT solvers. Another advantage of this semantics is that it precisely captures derivations in a sequent calculus for K that admit a certain property. Following Kearns, models of this semantics are based on the concept of *levels*—valuations of level 0 are the ordinary valuations of Nmatrices, while each level m > 0 introduces more constraints. We show that valuations of level m correspond to derivations in the calculus whose largest number of applications of the rule that correspond to the axiom (K) in any branch of the derivation is at most m. Our restrictions between the levels are more complex than the original restrictions in Kearns' work, in order to obtain effectiveness. Another precise correspondence between the semantics and the proof system that we prove, is between the domains of valuations and the formulas allowed to be used in derivations.

Finally, we observe that by deleting one of the truth values, a three-valued semantics for the modal logic KT is obtained, which is similar to the one presented in [8]. Like the case of K, the resulting semantics is effective, and tightly correspond to derivations in a sequent calculus for KT.

*Outline.* The paper is organized as follows: Sect. 2 reviews standard notions in non-deterministic matrices. In Sect. 3, we present our semantics for the modal logic K, as well as the sequent calculus our investigation will be based on, which is coupled with the notion of (K)-depth of derivations. In Sect. 4, we prove soundness and completeness theorems between the sequent calculus and the semantics. In Sect. 5, we prove that the semantics that we provide is effective, not only for deciding entailment, but also for producing countermodels when an entailment does not hold. In Sect. 6 we establish similar results for the modal logic KT. We conclude with §7, where directions for future research are outlined.

*Related Work.* In [10], Kearns initiated the study of modal semantics without possible worlds. This work was recently revisited by Skurt and Omori [14], who generalized Kearns' work and reframed his framework within the framework of logical Non-deterministic matrices. As indicated in [14], it was not clear how to make this semantics effective, as it requires checking truth values of infinitely many formulas when considering the validity of a given formula (see, e.g., Remark 42 of [14]). In [4], Coniglio et al. develop a similar framework for modal logics, and some bound over the formulas that need to be considered was achieved. However, in [5], the authors clarified that it is unclear how to effectively use the resulting semantics. A semantics based on Nmatrices for the modal logics KT and S4 was presented in [8] by Gr¨atz, that includes a method to extend a partial model in that semantics into a total one, which results in an effective semantics. We chose here to focus on K, which is a weaker logic, forming a common basis to all other normal modal logics. By deleting one out of four truth values, we obtain corresponding results for KT as well. The semantics that we present here is similar in nature to the one presented in [8], however: (i) the truth tables are different, as we intentionally enforced the many-valued tables of the classical connectives to be obtained by a straightforward duplication of truth values from the original two-valued truth tables; and (ii) the semantic condition for levels of valuations that we define here is inductive, where each level relies on lower levels (thus refraining from a definition of a more cyclic nature as the one in [8], that is better understood operationally). A variant of the semantics from [14] was also introduced and studied in [12], but without considering the ability to perform effective automated reasoning but instead focusing on infinite valuations rather than on partial ones. A complete proof theoretic characterization in terms of sequent calculi to the various levels of valuations was not given in any of the above works. Also, an effective semantics for K, which is the most basic modal logic, was not given in any of the above works.

Non-deterministic matrices were introduced in [2], and have since became a useful tool for investigating non-classical logics and proof systems (see [1] for a survey). They generalize (deterministic) matrices [15] by allowing a nondeterministic choice of truth values in the truth tables. Like matrices, Nmatrices enjoy the semantic *analyticity* property, which allows one to extend a partial valuation into a full one. Our semantic framework can be viewed as a further refinement of non-deterministic matrices, namely *restricted* non-deterministic matrices, introduced in [6].

# **2 Preliminaries**

In this section we provide the necessary definitions about Nmatrices following [1]. We assume a propositional language L with countably infinitely many atomic variables p1, p2,.... When there is no room for confusion, we identify L with its set of well-formed formulas (e.g., when writing ϕ ∈ L). We write *sub*(ϕ) for the set of subformulas of a formula ϕ. This notation is extended to sets of formulas in the natural way.

*Valuations.* In the context of a set V of "truth values", a *valuation* is a function v from some domain Dom(v) ⊆ L to V. For a set F⊆L, an F-*valuation* is a valuation with domain F. (In particular, an L-valuation is defined on all formulas.) For X ⊆ V, we write v−1[X] for the set {ϕ | v(ϕ) ∈ X}. For x ∈ V, we also write v−1[x] for the set {ϕ | v(ϕ) = x}.

**Definition 1.** Let D⊆V be a set of "designated truth values". A valuation v D-*satisfies* a formula ϕ, denoted by v |=D ϕ, if v(ϕ) ∈ D. For a set Σ of formulas, we write v |=D Σ if v |=D ϕ for every ϕ ∈ Σ.

**Notation 2.** Let D⊆V be a set of designated truth values and V be a set of valuations. For sets L, R of formulas, we write L V D R if for every v ∈ V, v |=D L implies that v |=D ϕ for some ϕ ∈ R. We omit L or R in this notation when they are empty (e.g., when writing V D R), and set parentheses for singletons (e.g., when writing L V D ϕ).

*Nmatrices.* An Nmatrix M for L is a triple of the form V, D, O, where V is a set of *truth values*, D⊆V is a set of *designated truth values*, and O is a function assigning a *truth table* Vn → P(V)\ {∅} to every n-ary connective of L (which assigns a set of possible values to each tuple of values). In the context of an Nmatrix M = V, D, O, we often denote O( ) by ˜ .

An F-valuation v is M-*legal* if v(ϕ) ∈ pos-val(ϕ, M, v) for every formula ϕ ∈ F whose immediate subformulas are contained in F, where pos-val(ϕ, M, v) is defined by:

In other words, there is no restriction regarding the values assigned to atomic formulas, whereas the values of compound formulas should respect the truth tables.

**Lemma 1 (**[1]**).** *Let* F⊆L *be a set closed under subformulas and* M *an Nmatrix for* L*. Then every* M*-legal* F*-valuation* v *can be extended to an* M*-legal* L*-valuation.*

# **3 The Modal Logic** K

In this section we introduce a novel effective semantics for the model logic K. We first present a known proof system for this logic (Sect. 3.1), and then our semantics (Sect. 3.2). From here on, we assume that the language L consists of the connectives ⊃, ∧, ∨, ¬ and with their usual arities. The standard ♦ operator can be defined as a macro ♦ϕ def = ¬-¬ϕ. Obviously, using De-Morgan rules, fewer connectives can be used. However, we chose this set of connectives in order to have a primitive language rich enough for the examples that we include along the paper.

#### **3.1 Proof System**

Figure 1 presents a Gentzen-style calculus, denoted by GK, for the modal logic K that was proven to be equivalent to the original formulation of the logic as a Hilbert system (see, e.g., [16]). We take *sequents* to be pairs Γ,Δ of finite *sets* of formulas. For readability, we write Γ ⇒ Δ instead of Γ,Δ and use standard notations such as Γ, ϕ ⇒ ψ instead of (Γ ∪ {ϕ}) ⇒ {ψ}.

The (cut) rule is included in GK for convenience, but applications of (cut) can be eliminated from derivations (see, e.g., [11]). Since the focus of this paper is semantics rather than cut-elimination, we allow ourselves to use cut freely and do not distinguish derivations that use it from derivations that do not. We write GK Γ ⇒ Δ if there is a derivation of a sequent Γ ⇒ Δ in the calculus GK.

In the sequel, we provide a semantic characterization of GK . It is based on a more refined notion of derivability that takes into account: (i) the set F of formulas used in the derivation; and (ii) the (K)-*depth* of the derivation, as defined next.

$$\begin{array}{llll} \left( \text{(WEAK)} \right) \frac{\Gamma \Rightarrow \Delta}{\Gamma, \Gamma' \Rightarrow \Delta, \Delta'} & \quad \left( \text{(D)} \right) \frac{\Gamma \Rightarrow \varphi, \Delta}{\Gamma, \varphi \Rightarrow \varphi, \Delta} & \quad \left( K \right) \frac{\Gamma \Rightarrow \varphi}{\Box \Gamma \Rightarrow \Box \varphi} \\\\ \left( \begin{array}{ll} \Gamma \Rightarrow \varphi, \Delta \\ \Gamma, \neg \varphi \Rightarrow \Delta \end{array} & \left( \Rightarrow \text{)} \end{array} \right) \begin{array}{llll} \Gamma \Rightarrow \varphi, \Delta \\ \left( \begin{array}{ll} \Gamma \Rightarrow \varphi, \Delta \\ \Gamma \Rightarrow \neg \varphi, \Delta \end{array} & \left( \begin{array}{ll} \Gamma \Rightarrow \varphi, \Delta \\ \Gamma \Rightarrow \neg \varphi, \Delta \end{array} \right) \begin{array}{llll} \Gamma, \forall \Rightarrow \varphi \\ \Gamma, \forall \Rightarrow \Delta \\ \Gamma, \varphi \Rightarrow \psi, \Delta \end{array} \\\\ \left( \begin{array}{ll} \Gamma \Rightarrow \varphi, \Delta \\ \Gamma, \varphi \Rightarrow \Delta \end{array} & \left( \begin{array}{ll} \Gamma \Rightarrow \varphi, \Delta \\ \Gamma \Rightarrow \varphi \land \psi, \Delta \end{array} \right) \begin{array}{llll} \Gamma, \varphi \Rightarrow \psi, \Delta \\ \Gamma \Rightarrow \varphi \Rightarrow \psi, \Delta \\ \Gamma \Rightarrow \varphi \Rightarrow \psi, \Delta \end{array} \\\\ \left( \begin{array}{ll} \Gamma \Rightarrow \varphi, \Delta \\ \Gamma, \varphi \Rightarrow \psi, \Delta \end{array} \right) \begin{array}{llll} \Gamma \Rightarrow \varphi, \Delta \\ \Gamma \Rightarrow \varphi \Rightarrow \psi, \Delta \end{array} \end{array}$$

**Fig. 1.** The sequent calculus GK

**Definition 3.** A *derivation* of a sequent Γ ⇒ Δ in GK is a tree in which the nodes are labeled with sequents, the root is labeled with Γ ⇒ Δ, and every node is the result of an application of some rule of GK where the premises are the labels of its children in the tree. A derivation is called an F-*derivation* if it employs only sequents composed of formulas from F. The (K)-*depth* of a derivation is the maximal number of applications of rule (K) in any of the branches of the derivation.

**Notation 4.** We write F,m GK Γ ⇒ Δ if there is a derivation of Γ ⇒ Δ in GK in which only F-sequents occur and that has (K)-depth at most m. We drop F from this notation when F = L; and drop m to dismiss the restriction regarding the (K)-depth.

*Example 1.* Let ϕ def = -(p1 ∧ p2) ⊃ (p1 ∧ p2) and F = *sub*(ϕ). The following is a derivation of ⇒ ϕ in GK that only uses F-formulas and has (K)-depth of 1 (though the number of applications of (K) in the derivation is 2):

$$\begin{array}{c} \overline{\frac{p\_1, p\_2 \Rightarrow p\_1}{p\_1 \land p\_2 \Rightarrow p\_1}}(\land\Rightarrow) \qquad \overline{\frac{p\_1, p\_2 \Rightarrow p\_2}{p\_1 \land p\_2 \Rightarrow p\_2}}(\land\Rightarrow) \\ \overline{\frac{\Box(p\_1 \land p\_2) \Rightarrow \Box p\_1}{\Box(p\_1 \land p\_2) \Rightarrow \Box p\_1 \land \Box p\_2}}(\land\Rightarrow) \qquad \overline{\frac{\Box(p\_1 \land p\_2) \Rightarrow \Box p\_2}{\Box(p\_1 \land p\_2) \Rightarrow \Box p\_2}}(\text{K}) \\ \hline \end{array}$$

#### **3.2 Semantics**

The semantics is based on a four-valued Nmatrix stratified with "levels", where for every m, legal valuations of level m + 1 are a subset of legal valuations of level m. The underlying Nmatrix, denoted by MK, is obtained by duplicating the classical truth values. Thus, the sets of truth values and of designated truth values are given by:

$$\mathcal{V}\_4 \stackrel{\text{def}}{=} \{ \mathsf{T}, \mathsf{t}, \mathsf{f}, \mathsf{F} \} \qquad \qquad \mathcal{D} \stackrel{\text{def}}{=} \{ \mathsf{T}, \mathsf{t} \}.$$

The truth tables are as follows (we have D = {f, F}):

We employ the following notations for subsets of truth values:

$$\mathsf{TF} \stackrel{\mathsf{a}\*}{=} \{\mathsf{T}, \mathsf{F}\} \qquad \mathsf{tf} \stackrel{\mathsf{a}\*}{=} \{\mathsf{t}, \mathsf{f}\}$$

For the classical connectives, the truth tables of MK treat t just like T, and f just like F, and are essentially two-valued—the result is either D or D, and it depends solely on whether the inputs are elements of D or D. Thus, for the language without -, this Nmatrix provides a (non-economic) four-valued semantics for classical logic.

While the output for is also always D or D, it differentiates between T (that results in D) and t (that results in D), and similarly between F and f. In fact, this table is captured by the condition: -˜ (x) ∈ D iff x ∈ TF.

*Example 2.* Let F = *sub*(ϕ) where ϕ is the formula from Example 1. The following valuation v is an F-valuation that is MK-legal:

$$v(p\_1) = v(p\_2) = \mathsf{f} \quad v(p\_1 \wedge p\_2) = \mathsf{F} \quad v(\Box p\_1) = v(\Box p\_2) = v(\Box p\_1 \wedge \Box p\_2) = \mathsf{F}$$

$$v(\Box (p\_1 \wedge p\_2)) = \mathsf{T} \quad v(\Box (p\_1 \wedge p\_2) \supset (\Box p\_1 \wedge \Box p\_2)) = \mathsf{F}$$

To show that it is MK-legal, one needs to verify that v(ψ) ∈ pos-val(ψ, MK, v) for each ψ ∈ F. For example, v(p1) = f ∈ V4 = pos-val(p1, MK, v). As another example, since v(p1) = f, we have that pos-val(p1, MK, v) = -˜ (f) = {F, f}, and hence v(p1) = F ∈ pos-val(p1, MK, v). Notice that v does not satisfy ϕ.

The truth table for can be understood via "possible worlds" intuition. Our four truth values are intuitively captured as follows, assuming a given formula ψ and a world w:

In the possible worlds semantics, ψ holds in some world w iff ψ holds in every world that is accessible from w, which intuitively explains the table for -. Note that non-determinism is inherent here. For example, if ψ holds in w and in every world accessible from w (i.e., ψ has value T), we know that ψ holds in w, but we do not know whether ψ holds in every world accessible from w (thus ψ has value T or t).

Now, the Nmatrix MK by itself is not adequate for the modal logic K (as Examples 1 and 2 demonstrate). What is missing is the relation between the choices we make to resolve non-determinism for different formulas. Continuing with the possible worlds intuition, we observe that if a formula ϕ follows from a set of formulas Σ that hold in all accessible worlds (i.e., ϕ follows from formulas whose truth value is T or F), then ϕ itself should hold in all accessible worlds (i.e., ϕ's truth value should be T or F). Directly encoding this condition requires us to consider a set V of MK-legal F-valuations for which the following holds (recall Notation 2 from Sect. 2):

$$\forall v \in \mathbb{V}. \forall \varphi \in \mathcal{F}. (v^{-1}[\mathbb{T}] \vdash\_{\mathcal{D}}^{\mathbb{V}} \varphi \implies v(\varphi) \in \mathbb{T}) \tag{neressation} \text{ } (nessisation)$$

In turn, to obtain completeness we take a maximal set V that satisfies the *necessitation* condition. While it is possible to define this set of valuations as the greatest fixpoint of *necessitation*, following previous work, we find it convenient to reach this set using "levels":

**Definition 5.** The set VF,m K is inductively defined as follows:

– VF,0 K is the set of MK-legal F-valuations. – VF,m+1 K def = - v ∈ VF,m K | ∀ϕ ∈ F. v−1[TF] VF,m K D ϕ =⇒ v(ϕ) ∈ TF

We also define:

$$\mathbb{V}\_{\mathsf{K}}^{\mathcal{F}} \stackrel{\scriptstyle \mathsf{def}}{=} \bigcap\_{m \geq 0} \mathbb{V}\_{\mathsf{K}}^{\mathcal{F}, m} \qquad \qquad \mathbb{V}\_{\mathsf{K}}^{m \stackrel{\scriptstyle \mathsf{def}}{=}} \mathbb{V}\_{\mathsf{K}}^{\mathcal{L}, m} \qquad \qquad \mathbb{V}\_{\mathsf{K}} \stackrel{\scriptstyle \mathsf{def}}{=} \bigcap\_{m \geq 0} \mathbb{V}\_{\mathsf{K}}^{\mathcal{L}, m}$$

Similarly to the idea originated by Kearns in [10], valuations are partitioned into *levels*, which are inductively defined. The first level, VF,0 K , consists solely of the MK-legal valuations with domain F. For each m > 0, the m'th level is defined as a subset of the (m − 1)'th level, with an additional constraint: a valuation v from level m − 1 remains in level m, only if every formula ϕ ∈ F entailed (at the m − 1 level) from the set of formulas that were assigned a value from TF by v, is itself assigned a value from TF by v. As we show below, in the "end" of this process, by taking m≥0 VF,m K , one obtains the greatest set V satisfying the *necessitation* condition

*Remark 1.* The *necessitation* condition is similar to the one provided in [8] to the modal logics KT and S4. In contrast, the condition from [4,10,14] is simpler and does not involve v−1[TF] at all, but also does not give rise to decision procedures.

*Example 3.* Following Example 2, while the formula ϕ is not satisfied by all valuations in VF,0 K , it is satisfied by all valuations in VF,m K for every m > 0. In particular, the valuation v from Example 2 is not in VF,1 K : we have p1∧p2 VF,0 K D p1 and v(p1 ∧ p2) = F (so p1 ∧ p2 ∈ v−1[TF]), but v(p1) = f ∈/ TF.

For each set F⊆L and m ≥ 0, we obtain a consequence relation VF,m K D between sets of F-formulas. Disregarding m, we also obtain the relation VF K D (for every F), which we will show to be sound and complete for K. We note that all these relations are compact. The proof of the following theorem relies on the completeness theorems that we prove in Sect. 4.

#### **Theorem 1 (Compactness).**

*1. For every* m ≥ 0*, if* L VF,m *K* D R*, then* Γ VF,m *K* D Δ *for some finite* Γ ⊆ L *and* Δ ⊆ R*. 2. If* L VF *K* D R*, then* Γ VF *K* D Δ *for some finite* Γ ⊆ L *and* Δ ⊆ R*.*

Now, to show that VF K is indeed the largest set V of MK-legal F-valuations that satisfies *necessitation*, we use the following two lemmas. The first is a general construction that relies only on the use of *finite-valued* valuation functions.

**Lemma 2.** *Let* v0, v1, v2,... *be an infinite sequence of valuations over a common domain* F*. Then, there exists some* v *such that for every finite set* F ⊆ F *of formulas and* m ≥ 0*, we have* v|F- = vk|F*for some* k ≥ m*.*

*Proof (Outline).* First, if F is finite, then there is only a finite number of Fvaluations, and there must exists some F-valuation vm that occurs infinitely often in the sequence v0, v1,.... We take v = vm, and the required property trivially holds. Now, assume that F is infinite, and let ϕ0, ϕ1,... be an enumeration of the formulas in F. For every i ≥ 0, let Fi = {ϕ0,...,ϕi}. We construct a sequence of infinite sets A0, A1,... ⊆ N such that:

– For every i ≥ 0, Ai+1 ⊆ Ai.

– For every 0 ≤ j ≤ i, a ∈ Aj , and b ∈ Ai, va(ϕj ) = vb(ϕj ).

To do so, take some infinite set A0 ⊆ N such that va(ϕ0) = vb(ϕ0) for every a, b ∈ A0 (such set must exist since we have a finite number of truth values). Then, given Ai, we let Ai+1 be some infinite subset of Ai such that va(ϕi+1) = vb(ϕi+1) for every a, b ∈ Ai+1. The valuation v is defined by v(ϕi) = va(ϕi) for some a ∈ Ai. The properties of the Ai's ensure that v is well defined, and it can be shown that it also satisfies the required property.

Using Lemma 2 and the compactness property, we can show the following:

**Lemma 3.** *Let* v0, v1,... *be a sequence of valuations over a common domain* F *such that* vm ∈ VF,m *K for every* m ≥ 0*. Then, there exists some* v ∈ VF *K such that for every* ϕ ∈ F*,* v(ϕ) = vm(ϕ) *for some* m ≥ 0*.*

*Proof (Outline).* By Lemma 2, there exists some v such that for every finite set F of formulas, v|F- = vm|F for some m ≥ 0. It is easy to verify that v satisfies the required properties. In particular, one shows that v ∈ VF,m K for every m ≥ 0 by induction on m. In that proof we use Theorem 1 to obtain a finite Γ ⊆ v−1[TF] such that Γ VF,m−1 K D ϕ from the assumption that v−1[TF] VF,m−1 K D ϕ. Then, the above property of v is applied with F = Γ ∪ {ϕ}. Now, our characterization theorem easily follows:

**Theorem 2.** *The set* VF *K is the largest set* V *of* M*K-legal* F*-valuations that satisfies necessitation.*

*Proof (Outline).* To prove that VF K satisfies *necessitation*, one needs to prove that if v−1[TF] VF K D ϕ, then also v−1[TF] VF,m K D ϕ for some m ≥ 0. This is done using Lemma 3. For maximality, given a set V, we assume by contradiction that there is some m such that V ⊆ VF,m K , take a minimal such m, and show that it cannot be 0. Then, from V ⊆ VF K m − 1, it follows that actually V ⊆ VF,m K , and thus we obtain a contradiction.

**Finite Domain.** By definition we have VF,0 K ⊇ VF,1 K ⊇ VF,2 K ⊇ ... (and so, VF,0 K D ⊆ VF,1 K D ⊆ VF,2 K D ⊆ ...). Next, we show that when F is finite, then this sequence must converge.

**Lemma 4.** *Suppose that* VF,m *K* = VF,m+1 *K for some* m ≥ 0*. Then,* VF *K* = VF,m *K .* **Lemma 5.** *For a* finite *set* F *of formulas,* VF *K* = VF,4|F| *K .*

*Proof.* The left-to-right inclusion follows from our definitions. For the right-toleft inclusion, note that by Lemma 4, VF,m K = VF,m+1 K implies that VF,m K = VF,k K for every k ≥ m. Thus, it suffices to show that VF,m K = VF,m+1 K for some 0 ≤ m ≤ 4|F | + 1. Indeed, otherwise we have VF,0 K ⊃ VF,1 K ⊃ VF,2 K ⊃ ... ⊃ VF,4|F|+1 K , but this is impossible since there are only 4|F | functions from F to V4.

**Optimized Tables.** Starting from level 1, the condition on valuations allows us to refine the truth tables of MK, and reduce the search space for countermodels. For instance, since ψ VF,0 K D ϕ ⊃ ψ (for every F with {ψ, ϕ, ϕ ⊃ ψ}⊆F), at level 1 we have that if ψ ∈ v−1[TF], then v(ϕ ⊃ ψ) ∈ TF. This allows us to remove t and f from the first and third columns (when y ∈ TF) in the table presenting ⊃˜ . The following entailments (at level 0), all with a single occurrence of some connective, lead to similar refinements, resulting in the optimized tables below for ⊃, ∧ and ∨:

$$\begin{array}{ccccc} \varphi,\varphi\supset\psi \vdash\_{\mathcal{D}}^{\mathsf{V}^{\mathsf{F}},0}\psi & \varphi,\psi \vdash\_{\mathcal{D}}^{\mathsf{V}^{\mathsf{F}},0}\varphi\wedge\psi & \varphi\wedge\psi \vdash\_{\mathcal{D}}^{\mathsf{V}^{\mathsf{F}},0}\varphi & \varphi\wedge\psi \vdash\_{\mathcal{D}}^{\mathsf{V}^{\mathsf{F}},0}\psi\\\\ \varphi\vdash\_{\mathcal{D}}^{\mathsf{V}^{\mathsf{F}},0}\varphi\vee\psi & \psi \vdash\_{\mathcal{D}}^{\mathsf{V}^{\mathsf{F}},0}\varphi\vee\psi \end{array}$$

We note that level 1 valuations are not fully captured by these tables. For example, they must assign T to every formula of the form ϕ ⊃ ϕ, while the table above allows also t when v(ϕ) ∈ tf. A decision procedure for K can benefit from relying on these optimized tables instead of the original ones, starting from level 1.

## **4 Soundness and Completeness**

In this section we establish the soundness and completeness of the proposed semantics. For that matter, we first extend the notion of satisfaction to sequents:

**Definition 6.**

To prove soundness, we first note that except for (K), the soundness of each derivation rule easily follows from the Nmatrix semantics:

**Lemma 6 (Local Soundness).** *Consider an application of a rule of* G*K other than* (K) *deriving a sequent* Γ ⇒ Δ *from sequents* Γ1 ⇒ Δ1,...,Γn ⇒ Δn*, such that* Γ ∪ Γ1 ∪ ... ∪ Γn ∪ Δ ∪ Δ1 ∪ ... ∪ Δn ⊆ F*. Let* v ∈ VF,m *K for some* m ≥ 0*.

For (K), we make use of the level requirement, and prove the following lemma.

**Lemma 7 (Soundness of (K)).** *Suppose that* Γ ∪ -Γ ∪ {ϕ, ϕ}⊆F*, and* Γ VF,m−1 *K* D ϕ*. Then,* -Γ VF,m *K* D ϕ*.*

*Proof.* Let v ∈ VF,m K such that v |=D -Γ. We prove that v |=D ϕ. By the truth table of -, we have that v(ψ) ∈ TF for every ψ ∈ Γ, and we need to show that v(ϕ) ∈ TF. Since v(ψ) ∈ TF for every ψ ∈ Γ, we have Γ ⊆ v−1[TF]. Since Γ VF,m−1 K D ϕ, we have v−1[TF] VF,m−1 K D ϕ. Since v ∈ VF,m K , it follows that v(ϕ) ∈ TF.

The above two lemmas together establish soundness, and from soundness for each level, we easily derive soundness for arbitrary (K)-depth.

**Theorem 3 (Soundness for** m**).** *If* F,m G*K* Γ ⇒ Δ*, then* Γ VF,m *K* D Δ*.*

**Theorem 4 (Soundness without** m**).** *If* F G*K* Γ ⇒ Δ*, then* Γ VF *K* D Δ*.*

By taking F = L in Theorem 4 we get that if GK Γ ⇒ Δ, then Γ VK D Δ. Next, we prove the following two completeness theorems:

**Theorem 5 (Completeness for** m**).** *Let* F⊆L *closed under subformulas and* Γ ⇒ Δ *an* F*-sequent. If* Γ VF,m *K* D Δ*, then* F,m G*K* Γ ⇒ Δ*.*

**Theorem 6 (Completeness without** m**).** *Let* F⊆L *closed under subformulas and* Γ ⇒ Δ *an* F*-sequent. If* Γ VF *K* D Δ*, then* F G*K* Γ ⇒ Δ*.*

In fact, since F may be infinite, we need to prove stronger theorems than Theorems 5 and 6, that incorporate infinite sequents.

**Definition 7.** An ω-sequent is a pair L, R, denoted by L ⇒ R, such that L and R are (possibly infinite) sets of formulas. We write F,m GK L ⇒ R if F,m GK Γ ⇒ Δ for some finite Γ ⊆ L and Δ ⊆ R.

Other notions for sequents (e.g., being an F-sequent) are extended to ωsequents in the obvious way. In particular, v |=D L ⇒ R if v(ψ) ∈ D/ for some ψ ∈ L or v(ψ) ∈ D for some ψ ∈ R.

**Theorem 7 (**ω**-Completeness for** m**).** *Let* F⊆L *closed under subformulas and* L ⇒ R *an* ω*-*F*-sequent. If* L VF,m *K* D R*, then* F,m G*K* L ⇒ R*.*

**Theorem 8 (**ω**-Completeness without** m**).** *Let* F⊆L *closed under subformulas and* L ⇒ R *an* ω*-*F*-sequent. If* L VF *K* D R*, then* F G*K* L ⇒ R*.*

Theorem 5 is a consequence of Theorem 7. Indeed, by Theorem 7, Γ VF,m K D Δ implies that F,m GK Γ ⇒ Δ for some (finite) Γ ⊆ Γ and Δ ⊆ Δ. Using (weak), we obtain that F,m GK Γ ⇒ Δ. Similarly, Theorem 6 is a consequence of Theorem 8. Also, using Lemma 3, we obtain Theorem 8 from Theorem 7. Hence in the remainder of this section we focus on the proof of Theorem 7.

**Proof of Theorem** 7**.** We start by defining maximal and consistent ω-sequents, and proving their existence.

**Definition 8 (Maximal and consistent** ω**-sequent).** Let F⊆L and m ≥ 0. An F-ω-sequent L ⇒ R is called:

**Lemma 8.** *Let* F⊆L *and* L ⇒ R *an* F*-*ω*-sequent. Suppose that* F,m G*K* L ⇒ R*. Then, there exist sets* LMC(G*K*,F,m,L⇒R) *and* RMC(G*K*,F,m,L⇒R) *such that the following hold:*

Thus, given an underivable ω-sequent, we can extend it to a GK, F, m-maxcon ω-sequent. This ω-sequent induces the canonical countermodel, as defined next.

#### **Algorithm 1.** Deciding Γ VK D ϕ.

1: F ← *sub*(Γ ∪ {ϕ}) 2: m ← 4|F | 3: **for** v ∈ VF*,m* K **do** 4: **if** v |=D Γ and v |=D ϕ **then** 5: **return** ("NO", v) 6: **return** "YES"

**Notation 9.** We denote the set {ψ ∈F | ψ ∈ X} by BX F .

**Definition 10.** Suppose that L R = F. The *canonical model w.r.t.* L ⇒ R*,* F*, and* m, denoted by v(F, L ⇒ R, m), is the F-valuation defined as follows (in λ notation):

$$\begin{aligned} & \text{For } m=0: & \quad \text{For } m>0:\\ & \lambda \varphi \in \mathcal{F}. \begin{cases} \mathsf{T} & \varphi \in L \text{ and } \Box \varphi \in L \\ \mathbf{t} & \varphi \in L \text{ and } \Box \varphi \notin L \\ \mathsf{F} & \varphi \in R \text{ and } \Box \varphi \in L \\ \mathbf{f} & \varphi \in R \text{ and } \Box \varphi \notin L \end{cases} & \lambda \varphi \in \mathcal{F}. \begin{cases} \mathsf{T} & \varphi \in L \text{ and } \|\!^{\mathcal{F}, m-1} \mathbb{B}\!^{L}\_{\mathcal{F}} \Rightarrow \varphi \\ \mathsf{t} & \varphi \in L \text{ and } \|\!^{\mathcal{F}, m-1} \mathbb{B}\!^{L}\_{\mathcal{F}} \Rightarrow \varphi \\ \mathsf{F} & \varphi \in R \text{ and } \|\!^{\mathcal{F}} \!^{\mathcal{G}, m-1} \mathbb{B}\!^{L}\_{\mathcal{F}} \Rightarrow \varphi \\ \mathsf{f} & \varphi \in R \text{ and } \|\!^{\mathcal{F}} \!^{\mathcal{G}, m-1} \mathbb{B}\!^{L}\_{\mathcal{F}} \Rightarrow \varphi \end{aligned} \end{aligned}$$

Clearly, v(F, L ⇒ R, m) |=D L ⇒ R. The proof of Theorem 7 is done by induction on m, and then carries on by showing that if L ⇒ R is GK, F, m max-con, then v(F, L ⇒ R, m) belongs to VF,m K for every m.

Concretely, let v def = v(F, L ⇒ R, m). We show that v ∈ VF,k K for every k ≤ m by induction on k. The base case k = 0 is straightforward. For k > 0, we have v ∈ VF,k−1 K by the induction hypothesis. Let ϕ ∈ F, and suppose that v−1[TF] VF,k−1 K D ϕ. To show that v(ϕ) ∈ TF, we prove that F,m−1 GK BL F ⇒ ϕ. By the outer induction hypothesis (regarding the completeness theorem itself), v−1[TF] VF,k−1 K D ϕ implies that F,k−1 GK v−1[TF] ⇒ ϕ, which implies that F,m−1 GK v−1[TF] ⇒ ϕ. Hence, there is a finite set {ϕ1,...,ϕn} ⊆ v−1[TF] such that F,m−1 GK {ϕ1,...,ϕn} ⇒ ϕ. For every 1 ≤ i ≤ n, since ϕi ∈ v−1[TF], we have that F,m−1 GK BL F ⇒ ϕi and hence F,m−1 GK Γi ⇒ ϕi for some Γi ⊆ BL F . Using n applications of (cut) on these sequents and F,m−1 GK {ϕ1,...,ϕn} ⇒ ϕ, we obtain that F,m−1 GK Γ1,...,Γn ⇒ ϕ, and so F,m−1 GK BL F ⇒ ϕ.

#### **5 Effectiveness of the Semantics**

In this section we study the effectiveness of the semantics introduced in Definition 5 for deciding MK . Roughly speaking, a semantic framework is said to be *effective* if it induces a decision procedure that decides its underlying logic.

Consider Algorithm 1. Given a finite set Γ of formulas and a formula ϕ, it checks whether any valuations in VF,m K is a countermodel. The correctness of this algorithm relies on the analyticity of GK, namely:

**Lemma 9 (**[11]**).** *If* G*K* Γ ⇒ Δ*, then sub*(Γ∪{ϕ}) G*K* Γ ⇒ Δ*.*

Using Lemma 9, we show that the algorithm is correct.

#### **Lemma 10.** *Algorithm 1 always terminates, and returns "YES" iff* Γ V*K* D ϕ*.*

*Proof.* Termination follows from the fact that VF,m K is finite. Suppose that the result is "YES" and assume for contradiction that Γ VK D ϕ. Hence, there exists some u ∈ VK such that u |=D Γ and u |=D ϕ. Consider v def = u|F . Then, v ∈ VF K ⊆ VF,m K , which contradicts the fact that the algorithm returns "YES". Now, suppose that the result is "NO". Then, there exists some v ∈ VF,m K such that v |=D Γ and v |=D ϕ. By Lemma 5, v ∈ VF K . Hence, Γ VF K D ϕ. By Theorem 3, we have F GK Γ ⇒ ϕ. By Lemma 9, we have GK Γ ⇒ ϕ. By Theorem 6, we have Γ VK D ϕ.

Lemma 10 shows that Algorithm 1 is a decision procedure for MK , when ignoring the additional output provided in Line 5. However, it is typical in applications that a "YES" or "NO" answer is not enough, and often it is expected that a "NO" result is accompanied with a countermodel. Algorithm 1 returns a valuation v in case the answer is "NO", but Lemma 10 does not ensure that v is indeed a countermodel for Γ VK D ϕ. The issue is that the valuation v from the proof of Lemma 10 witnesses the fact that VK D only in a non-constructive way. Indeed, using the soundness and completeness theorems, we are able to deduce that v |=D Γ and v |=D ϕ for some v ∈ VK, but the relation between v and v is unclear. Most importantly, it is not clear whether v and v agree on F-formulas. In the remainder of this section we prove that v extends v, and so the returned countermodel of Line 5 can be trusted.

We say that a valuation v *extends* a valuation v if Dom(v) ⊆ Dom(v ) and v (ϕ) = v(ϕ) for every ϕ ∈ Dom(v) (identifying functions with sets of pairs, this means v ⊆ v ). Clearly, for a Dom(v)-formula ψ we have that v |=D ψ iff v |=D ψ. We first show how to extend a given valuation v ∈ VF,m K by a single formula ψ such that *sub*(ψ)\ {ψ}⊆F, obtaining a valuation v ∈ VF∪{ψ},m K that agrees with v on all formulas in F.

**Lemma 11.** *Let* m ≥ 0*,* F⊆L*, and* v ∈ VF,m *K . Let* ψ ∈ L\F *such that sub*(ψ)\ {ψ}⊆F*. Then,* v *can be extended to some* v ∈ VF∪{ψ},m *K .*

We sketch the proof of Lemma 11.

When m = 0, v exists from Lemma 1. For m > 0, we define v as follows:1

$$v' \stackrel{\text{def}}{=} \lambda \varphi \in \mathcal{F} \cup \{\psi\} \cdot \begin{cases} v(\varphi) & \varphi \in \mathcal{F} \\ \min(\mathsf{pos-val}(\psi, \mathsf{M}\_{\mathbb{K}}, v) \cap \mathsf{TF}) & \varphi = \psi \wedge v^{-1}[\mathsf{TF}] \vdash\_{\mathcal{D}}^{\mathsf{V}\cup\{\psi\}, m-1} \psi \\ \min(\mathsf{pos-val}(\psi, \mathsf{M}\_{\mathbb{K}}, v) \cap \mathsf{tf}) & \text{otherwise} \end{cases}$$

1 The use of min here assumes an arbitrary order on truth values. It is used here only to choose *some* element from a non-empty set of truth values.

The proof of Lemma 11 then carries on by showing that v ∈ VF∪{ψ},m K . Next, Lemma 11 is used in order to extend partial valuations into total ones.

**Lemma 12.** *Let* v ∈ VF,m *K for some* F *closed under subformulas. Then,* v *can be extended to some* v ∈ Vm *K .*

Finally, Lemmas 3 and 12 can be used in order to extend any partial valuation in VF K into a total one.

**Lemma 13.** *Let* v ∈ VF *K for some set* F *closed under subformulas. Then,* v *can be extended to some* v ∈ V*K.*

We conclude by showing that when Algorithm 1 returns ("NO", v), then v is a finite representation of a true countermodel for Γ MK ϕ.

**Corollary 1.** *If* Γ V*K* D ϕ*.  Suppose that Γ VK D ϕ. Then by Lemma 10, Algorithm 1 does not return "YES". Therefore, it returns ("NO", v) for some v ∈ VF,m K such that v |=D Γ and v |=D ϕ, where F = *sub*(Γ ∪ {ϕ}) and m = 4|F |. By Lemma 5, v ∈ VKF. By Lemma 13, v can be extended to some v ∈ VK.

*Remark 2.* Notice that in scenarios where model generation is not important, m can be set to a much smaller number in Line 2 of Algorithm 1, namely, the "modal depth" of the input.2 The reason for that is that for such m, it can be shown that F,m GK Γ ⇒ ϕ iff F GK Γ ⇒ ϕ, by reasoning about the applications of rule (K). Using the soundness and completeness theorems, we can get Γ VF,m K D ϕ iff Γ VF K D ϕ, and so limiting to such m is enough. Notice however, that we do not necessarily get VF,m K = VF K for such m, and so the valuation returned in Line 5 might not be an element of VF K .

#### **6 The Modal Logic** KT

In this section we obtain similar results for the modal logic KT. First, the calculus GKT is obtained from GK by adding the following rule (see, e.g., [16]):

$$(T)\;\frac{\Gamma,\varphi\Rightarrow\Delta}{\Gamma,\square\varphi\Rightarrow\Delta}$$

Derivations are defined as before. (In particular, the (K)-depth of a derivation still depends on applications of rule (K), not of rule (T).) We write F,m GKT Γ ⇒ Δ

2 The *modal depth* of an atomic formula p is 0. The modal depth of ϕ is the modal depth of ϕ plus 1. The modal depth of (ϕ1,...,ϕ*n*) for = is the maximum among the modal depths of ϕ1,...,ϕ*n*.

if there is a derivation of Γ ⇒ Δ in GKT in which only F-sequents occur and that has (K)-depth at most m.

Next, we consider the semantics. For a valuation v ∈ VK to respect rule (T), we must have that if v |=D Γ, ϕ ⇒ Δ, then v |=D Γ, ϕ ⇒ Δ. In particular, when v |=D Γ ⇒ Δ, we get that if v(ϕ) ∈ D/ , then v(ϕ) ∈ D/ . Now, if v(ϕ) = F, then v(ϕ) ∈ D according to the truth table of in MK. But, we must have v(ϕ) ∈ D/ . This leads us to remove F from MK.

We thus obtain the following Nmatrix MKT: The sets of truth values and of designated truth values are given by3

$$\mathcal{V}\_3 \stackrel{\text{def}}{=} \{\mathsf{T}, \mathsf{t}, \mathsf{f}\} \qquad \qquad \mathcal{D} \stackrel{\text{def}}{=} \{\mathsf{T}, \mathsf{t}\}$$

and the truth tables are as follows:

Again, one may gain intuition from the possible worlds semantics. There, the logic KT is characterized by frames with *reflexive* accessibility relation. Thus, for instance, if ψ holds in w but not in some world accessible from w (i.e., ψ has value t), we know that ψ does not hold in w, and the reflexivity of the accessibility relation implies that ψ does not hold in some world accessible from w (thus ψ has value f).

*Example 4.* Let ϕ def = --(p1 ∧ p2) ⊃ p1 and F def = *sub*(ϕ). The sequent ⇒ ϕ has a derivation in GKT using only F formulas of (K)-depth of 1. However, it is not satisfied by all MKT-legal F-valuations. For example, the following valuation is an MKT-legal valuation that does not satisfy ϕ:

$$v(p\_1) = v(p\_2) = \mathbf{t} \quad v(\Box p\_1) = \mathbf{f}$$

$$v(p\_1 \wedge p\_2) = v(\Box (p\_1 \wedge p\_2)) = v(\Box \Box (p\_1 \wedge p\_2)) = \mathbf{\sf T} \quad v(\varphi) = \mathbf{f}$$

Next, we define the levels of valuations for MKT. These are obtained from Definition 5 by removing the value F:

**Definition 11.** The set VF,m KT is recursively defined as follows:

– VF,0 KT is the set of MKT-legal F-valuations. – VF,m+1 KT def = - v ∈ VF,m KT | ∀ϕ ∈ F. v−1[T] VF,m KT D ϕ =⇒ v(ϕ) = T

We also define:

$$\mathbb{V}\_{\mathsf{KT}}^{\mathcal{F}} \stackrel{\scriptstyle \mathsf{def}}{=} \bigcap\_{m \geq 0} \mathbb{V}\_{\mathsf{KT}}^{\mathcal{F}, m} \qquad\qquad\qquad \mathbb{V}\_{\mathsf{KT}}^{m} \stackrel{\scriptstyle \mathsf{def}}{=} \mathbb{V}\_{\mathsf{KT}}^{\mathcal{L}, m} \qquad\qquad \mathbb{V}\_{\mathsf{KT}} \stackrel{\scriptstyle \mathsf{def}}{=} \bigcap\_{m \geq 0} \mathbb{V}\_{\mathsf{KT}}^{\mathcal{L}, m}$$

3 In this section we denote the set {T} by TF.

*Example 5.* Following Example 4, we note that for every v ∈ VF,m KT with m > 0, we have v |=D ϕ. In particular, the valuation v from Example 4 does not belong to VF,m KT : -(p1 ∧ p2) ∈ v−1[T], -(p1 ∧ p2) VF,0 KT D p1, but v(p1) = t.

Similarly to Theorem 2, the levels of valuations converge to a maximal set that satisfies the following condition:

$$\forall v \in \mathbb{V}. \forall \varphi \in \mathcal{F}. v^{-1}[\mathsf{T}] \vdash\_{\mathcal{D}}^{\mathsf{V}} \varphi \implies v(\varphi) = \mathsf{T} \qquad \qquad (recesisation\_{\mathsf{KT}})$$

**Theorem 9.** *The set* VF *KT is the largest set* V *of* M*KT-legal* F*-valuations that satisfies necessitationKT.*

The proof of Theorem 9 is analogous to that of Theorem 2.

*Remark 3.* The *necessitation*KT condition is equivalent to the one given in [8], except that the underlying truth table is different. Theorem 9 proves that our gradual way of defining VF KT via levels coincides with the semantic condition from [8].

As we demonstrated for K, starting from level 1, the condition on valuations allows us to refine the truth tables of MKT, and reduce the search space. Simple entailments (at level 0) lead to the optimized tables below for ⊃, ∧ and ∨:

Soundness and completeness for GKT are obtained analogously to GK, keeping in mind that MKT is obtained from MK by deleting the value F. For soundness, this is captured by the rule (T). For completeness, the same construction of a countermodel is performed , while rule (T) ensures that it is three-valued.

**Theorem 10 (Soundness and Completeness).** *Let* F⊆L *closed under subformulas and* Γ ⇒ Δ *an* F*-sequent.*

*1. For every* m ≥ 0*,* Γ VF,m *KT* D Δ *iff* F,m G*KT* Γ ⇒ Δ*. 2.* Γ VF *KT* D Δ *iff* F G*KT* Γ ⇒ Δ*.*

Effectiveness is also shown similarly to K. For that matter, we use the following main lemma, whose proof is similar to Lemma 13. The only component that is added to that proof is making sure that the constructed model is three-valued.

**Lemma 14.** *Let* v ∈ VF *KT for some set* F *closed under subformulas. Then,* v *can be extended to some* v ∈ V*KT.*

Let Algorithm 2 be obtained from Algorithm 1 by setting m to 3|F | in Line 2, and taking v ∈ VF,m KT in Line 3. Similarly to Lemma 10 and Corollary 1, we get that Algorithm 2 is a model-producing decision procedure for MKT .

**Lemma 15.** *Algorithm 2 always terminates, and returns "YES" iff* Γ V*KT* D ϕ*. Further, if* Γ V*KT* D ϕ*, then it returns ("NO",* v*) for some* v *for which there exists* v ∈ V*KT such that* v = v |*sub*(Γ∪{ϕ})*,* v |=D Γ*, and* v |=D ϕ*.*

## **7 Future Work**

We have introduced a new semantics for the modal logic K, based on levels of valuations in many-valued non-deterministic matrices. Our semantics is effective, and was shown to tightly correspond to derivations in a sequent calculus for K. We also adapted these results for the modal logic KT.

There are two main directions for future work. The first is to establish similar semantics for other normal modal logics, such as KD, K4, S4 and S5, and to investigate ♦ as an independent modality. The second is to analyze the complexity, implement and experiment with decision procedures for K and KT based on the proposed semantics. In particular, we plan to consider SAT-based decision procedures that would encode this semantics in SAT, directly or iteratively.

## **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# **Local Reductions for the Modal Cube**

Cl´audia Nalon1 , Ullrich Hustadt2(B) , Fabio Papacchini3 , and Clare Dixon4

1 Department of Computer Science, University of Bras´ılia, Bras´ılia, Brazil<EMAIL_ADDRESS>
2 Department of Computer Science, University of Liverpool, Liverpool, UK<EMAIL_ADDRESS>
3 School of Computing and Communications, Lancaster University in Leipzig, Leipzig, Germany

<EMAIL_ADDRESS>
4 Department of Computer Science, University of Manchester, Manchester, UK<EMAIL_ADDRESS>
**Abstract.** The modal logic K is commonly used to represent and reason about necessity and possibility and its extensions with combinations of additional axioms are used to represent knowledge, belief, desires and intentions. Here we present local reductions of all propositional modal logics in the so-called modal cube, that is, extensions of K with arbitrary combinations of the axioms B, D, T, 4 and 5 to a normal form comprising a formula and the set of modal levels it occurs at. Using these reductions we can carry out reasoning for all these logics with the theorem prover KSP. We define benchmarks for these logics and experiment with the reduction approach as compared to an existing resolution calculus with specialised inference rules for the various logics.

### **1 Introduction**

Modal logics have been used to represent and reason about mental attitudes such as knowledge, belief, desire and intention, see for example [17,20,31]. These can be represented using extensions of the basic modal logic K with one or more of the axioms B (symmetry), D (seriality), T (reflexivity), 4 (transitivity) and 5 (Euclideaness). The logic K and these extensions form the so-called *modal cube*, see Fig. 1. In the diagram, a line from a logic L1 to a logic L2 to its right and/or above means that all theorems of L1 are also theorems of L2, but not vice versa. As indicated in Fig. 1, some of the logics have the same theorems, e.g., KB5 and KB4. Also, all logics not explicitly listed have the same theorems as KT5 aka S5. In total there are 15 distinct logics.

While these modal logics are well-studied and a multitude of calculi and translations to other logics exist, see, e.g., [1,3–6,9,13,14,16,18,22,41], fully

C. Dixon was partially supported by the EPSRC funded RAI Hubs FAIR-SPACE (EP/R026092/1) and RAIN (EP/R026084/1), and the EPSRC funded programme Grant S4 (EP/N007565/1).

**Fig. 1.** Modal Cube: Relationships between modal logics

automatic support by provers is still lacking. Early implementations covering the full modal cube, such as Catach's TABLEAUX system [7], are no longer available. LoTREC 2.0 [10] supports a wide range of logics but is not intended as an automatic theorem prover. MOIN [11] supports all the logics but the focus is on producing human-readable proofs and countermodels for small formulae. Other provers that go beyond just K, like MleanCoP [28] and CEGARBox [15] only support a small subset of the 15 logics. There are also a range of translations from modal logics to first-order and higher-order logics [13,18,19,27,33]. Regarding implementations of those, SPASS [33,43] is limited to a subset of the 15 logics, while LEO-III [13,36] supports all the logics in the modal cube, but can only solve very few of the available benchmark formulae.

KSP [23] is a modal logic theorem prover that implements both the modallayered resolution (MLR) calculus [25] for the modal logic K and the global resolution (GMR) calculus [24] for all the 15 logics considered here. It also supports several refinements of resolution and a range of simplification rules. In this paper, we give reductions of all logics of the modal cube into a normal form for the basic modal logic K. We then compare the performance of the combination of these reductions with the modal-layered resolution calculus to that of the global resolution calculus on a new benchmark collection for the modal cube.

In [29] we have presented new reductions1 of the propositional modal logics KB, KD, KT, K4, and K5 to Separated Normal Form with Sets of Modal Levels SNFsml. SNFsml is a generalisation of the Separated Normal Form with Modal Level, SNFml. In the latter, labelled modal clauses are used where a natural number label refers to a particular level within a tree Kripke structure at which a modal clause holds. In the former, a finite or infinite set of natural numbers labels each modal clause with the intended meaning that such a modal clause is true at every level of a tree Kripke structure contained in that set. As our prover KSP and the modal-layered resolution calculus it implements currently only support sets of modal clauses in SNFml, we then use a further reduction from SNFsml

1 A *reduction* here is a satisfiability preserving mapping between logics.

to SNFml to obtain an automatic theorem prover for these modal logics. Where all modal clauses are labelled with finite sets, this reduction is straightforward. This is the case for KB, KD and KT. For K4 and K5, characterised by the axioms ✷ϕ → ✷✷ϕ and ✸ϕ → ✷✸ϕ, modal clauses are in general labelled with infinite sets. However, using a result by Massacci [21] for K4 and an analogous result for K5 by ourselves, we are able to bound the maximal level occurring in those labelling sets which in turn makes a reduction to SNFml possible.

Also in [29], we have shown experimentally that these reductions allow us to reason effectively in these logics, compared to the global modal resolution calculus [24] and to the relational and semi-functional translation built into the first-order theorem prover SPASS 3.9 [33,38,42]. The reason that the comparison only included a rather limited selection of provers is that these are the only ones with built-in support for all six logics our reductions covered.

Unfortunately, we cannot simply combine our reductions for single axioms to obtain satisfiability preserving reductions for their combinations. There are two main reasons for this. First, our calculus does not use an explicit representation of the accessibility relationship within a Kripke structure, which would make it possible to reflect modal axioms via corresponding properties of that accessibility relationship. Instead, we add labelled modal clauses based on instances of the modal axioms for ✷-formulae occurring in the modal formula we want to check for satisfiability. However, if we deal with multiple modal axioms, then these axioms might interact making it necessary to add instances that are not necessary for each individual axiom. For instance, consider, the converse of axiom B, ✸✷ϕ → ϕ, and axiom 4, ✷ϕ → ✷✷ϕ. Together they imply ✸✷ϕ → ✷ϕ. Instances of this derived axiom are necessary for completeness of a reduction from KB4 to K, but are unsound for KB and K4 separately.

Second, our reductions attempt to keep the labelling sets minimal in size in order to decrease the number of inferences that can be performed. Again, taking axioms B and 4 as examples, in KB, a ✷-formula ✷ψ true at level ml in a treelike Kripke structure M forces ψ to be true at level ml − 1, while in K4, ✷ψ true at level ml in M forces ψ to be true all levels ml with ml > ml. This is reflected in the labelling sets we use for these two logics. However, for KB4, ✷ψ true at level ml forces ψ to be true at every level in a tree-like Kripke structure M (unless M consists only of a single world).

Since we intend to maintain these two properties of our reductions, we have to consider each modal logic individually. As we will see, for some logics a reduction can be obtained as the union of the existing reductions while for others we need a logic-specific reduction to accommodate the interaction of axioms.

The structure of the paper is as follows. In Sect. 2 we recall common concepts of propositional modal logic and the definition of our normal form SNFml. Section 3 introduces our reduction for extensions of the basic modal logic K with combinations of the axioms B, D, T, 4, and 5. Section 4 presents a transformation from SNFsml to SNFml which allows us to use the modal resolution prover KSP to reason in all the modal logics. In Sect. 5 we compare the performance of a combination of our reductions and the modal-layered resolution calculus implemented in the prover KSP with resolution calculi specifically designed for the logics under consideration as well as the prover LEO-III.

#### **2 Preliminaries**

The language of modal logic is an extension of the language of propositional logic with a unary modal operator ✷ and its dual ✸. More precisely, given a denumerable set of *propositional symbols*, P = {p, p0, q, q0, t, t0,...} as well as propositional *constants* **true** and **false**, *modal formulae* are inductively defined as follows: constants and propositional symbols are modal formulae. If ϕ and ψ are modal formulae, then so are ¬ϕ, (ϕ ∧ ψ), (ϕ ∨ ψ), (ϕ → ψ), ✷ϕ, and ✸ϕ. We also assume that ∧ and ∨ are associative and commutative operators and consider, e.g., (p∨(q∨r)) and (r∨(q∨p)) to be identical formulae. We often omit parentheses if this does not cause confusion. By var(ϕ) we denote the set of all propositional symbols occurring in ϕ. This function straightforwardly extends to finite sets of modal formulae. A *modal axiom (schema)* is a modal formula ψ representing the set of all instances of ψ.

A *literal* is either a propositional symbol or its negation; the set of literals is denoted by LP . By ¬l we denote the *complement* of the literal l ∈ LP , that is, if l is the propositional symbol p then ¬l denotes ¬p, and if l is the literal ¬p then ¬l denotes p. By |l| for l ∈ LP we denote p if l = p or l = ¬p. A *modal literal* is either ✷l or ✸l, where l ∈ LP .

A *(normal) modal logic* is a set of modal formulae which includes all propositional tautologies, the axiom schema ✷(ϕ → ψ) → (✷ϕ → ✷ψ), called the *axiom* K, it is closed under modus ponens (if ϕ and ϕ → ψ then ψ) and the rule of necessitation (if ϕ then ✷ϕ).

K is the weakest modal logic, that is, the logic given by the smallest set of modal formulae constituting a normal modal logic. By KΣ we denote an *extension* of K by a set Σ of axioms.

The standard semantics of modal logics is the *Kripke semantics* or *possible world semantics*. A *Kripke frame* F is an ordered pair W, R where W is a nonempty set of *worlds* and R is a binary (accessibility) relation over W. A *Kripke structure* M over P is an ordered pair F, V where F is a Kripke frame and the *valuation* V is a function mapping each propositional symbol in P to a subset V (p) of W. A *rooted Kripke structure* is an ordered pair M,w0 with w0 ∈ W. To simplify notation, in the following we write W, R, V and W, R, V, w0 instead of W, R, V and W, R, V , w0, respectively.

Satisfaction (or truth) of a formula at a world w of a Kripke structure M = W, R, V is inductively defined by:

**Table 1.** Modal axioms and relational frame properties

**Table 2.** Rewriting Rules for Simplification

```
ϕ ∧ ϕ ⇒ ϕ
   ϕ ∨ ϕ ⇒ ϕ
ϕ ∧ true ⇒ ϕ
                ϕ ∧ ¬ϕ ⇒ false
                ϕ ∨ ¬ϕ ⇒ true
              ϕ ∧ false ⇒ false
                                  ✷true ⇒ true
                                  ✸false ⇒ false
                                ϕ ∨ false ⇒ ϕ
                                                    ¬true ⇒ false
                                                    ¬false ⇒ true
                                                  ϕ ∨ true ⇒ true
                                                                   ¬¬ϕ ⇒ ϕ
```
If M,w |= ϕ holds then M is a *model* of ϕ, ϕ is *true at* w *in* M and M *satisfies* ϕ. A modal formula ϕ is *satisfiable* iff there exists a Kripke structure M and a world w in M such that M,w |= ϕ.

We are interested in extensions of K with the modal axioms shown in Table 1 and their combinations. Each of these axioms defines a class of Kripke frames where the accessibility relation R satisfies the first-order property stated in the table. Combinations of axioms then define a class of Kripke frames where the accessibility relation satisfies the combination of their corresponding properties.

Given a normal modal logic L with corresponding class of frames F, we say a modal formula ϕ is L*-satisfiable* iff there exists a frame F ∈ F, a valuation V and a world w ∈ F such that F, V, w |= ϕ. It is L*-valid* or *valid in* L iff for every frame F ∈ F, every valuation V and every world w ∈ F, F, V, w |= ϕ. A normal modal logic L2 is *an extension* of a normal modal logic L1 iff all L1-valid formulae are also L2-valid.

A rooted Kripke structure M = W, R, V, w0 is a *rooted tree Kripke structure* iff R is a tree, that is, a directed acyclic connected graph where each node has at most one predecessor, with *root* w0. It is a *rooted tree Kripke model* of a modal formula ϕ iff W, R, V, w0 |= ϕ. In a rooted tree Kripke structure with root w0 for every world wk ∈ W there is exactly one path connecting w0 and wk, the length of that path is the *modal level of* wk *(in* M*), denoted by* mlM(wk).

It is well-known [17] that a modal formula ϕ is K-satisfiable iff there is a finite rooted tree Kripke structure M = F, V, w0 such that M,w0 |= ϕ.

For the reductions presented in the next section we assume that any modal formula ϕ has been simplified by exhaustively applying the rewrite rules in Table 2, and it is in Negation Normal Form (NNF). That is, a formula where only propositional symbols are allowed in the scope of negations. We say that such a formula is in *simplified NNF*.

The reductions produce formulae in a clausal normal form, called *Separated Normal Form with Sets of Modal Levels* SNFsml, introduced in [29]. The language of SNFsml extends that of the basic modal logic K with sets of modal levels as labels. Clauses in SNFsml have one of the following forms:

S : n i=1 li (literal clause) S : l → ✷l (positive modal clause) S : l → ✸l (negative modal clause)

where S ⊆ N and l, l , li are propositional literals with 1 ≤ i ≤ n, n ∈ N. We write : ϕ instead of N : ϕ and such clauses are called *global clauses*. Positive and negative modal clauses are together known as *modal clauses*.

Given a rooted tree Kripke structure M and a set S of natural numbers, by M[S] we denote the set of worlds that are at a modal level in S, that is, M[S] = {w ∈ W | mlM(w) ∈ S}. Then

$$M \vdash S : \varphi \text{ iff } \langle M, w \rangle \vdash \varphi \text{ for every world } w \in M[S].$$

The motivation for using a set S to label clauses is that in our reductions the formula ϕ may hold at several levels, possibly an infinite number of levels. It therefore makes sense to label such formulae not with just a single level, but a set of levels. The Separated Normal Form with Modal Level, SNFml, can be seen as the special case of SNFsml where all labelling sets are singletons.

Note that if S = ∅, then M |= S : ϕ trivially holds. Also, a Kripke structure M can satisfy S : **false** if there is no world w with mlM(w) ∈ S. On the other hand, S : **false** with 0 ∈ S is unsatisfiable as a rooted tree Kripke structure always has a world with modal level 0.

If M |= S : ϕ, then we say that S : ϕ *holds in* M or *is true in* M. For a set Φ of labelled formulae, M |= Φ iff M |= S : ϕ for every S : ϕ in Φ, and we say Φ is K*-satisfiable*.

We introduce some notation that will be used in the following. Let S+ = {l+ 1 ∈ N | l ∈ S}, S− = {l−1 ∈ N | l ∈ S}, and S≥ = {n | n ≥ min(S)}, where min(S) is the least element in S. Note that the restriction of the elements being in N implies that S− cannot contain negative numbers.

# **3 Extensions of K**

In this section we define reductions from all the logics in the modal cube to SNFsml. We assume that the set P of propositional symbols is partitioned into two infinite sets Q and T such that Q contains the propositional symbols of the modal formula ϕ under consideration, and T surrogate symbols tψ for every subformula ψ of ϕ and supplementary propositional symbols. In particular, for every modal formula ψ we have var(ψ) ⊂ Q and there exists a propositional symbol tψ ∈ T uniquely associated with ψ. These surrogate symbols serve the same purpose as Tseitin variables [40] and Skolem predicates [30,39] in the transformation of propositional and first-order formulae, respectively, to clausal form via structural transformation.

It turns out that given a reduction ρKΣ for KΣ with {D,T} ∩ Σ = ∅, there is a uniform and straightforward way we can obtain a reduction for KDΣ and KTΣ from ρKΣ. Also, the valid formulae of KDTΣ are the same as those of

**Table 3.** Categorisation of modal logics in the modal cube

KTΣ, so we do not need to consider the case of adding both axioms to KΣ. Similarly, the logics KT45, KDB4, KTB4 and KT5 all have the same set of valid formulae. Therefore, as shown in Table 3, we can divide the 15 modal logics into three categories: Six 'base logics', five modal logics obtained by extending a 'base logic' with D, and a further four modal logics obtained by extending a 'base logic' with T. For four of the six 'base logics' (namely, K, KB, K4, and K5) we have already devised reductions in [29], so only two (i.e., KB4 and K45) remain.

Given a modal formula ϕ in simplified NNF and L = KΣ with Σ ⊆ {B, D,T, 4, 5}, we can obtain a set ΦL of clauses in SNFsml such that ϕ is L-satisfiable iff ΦL is K-satisfiable with ΦL = ρsml L (ϕ) = {{0} : tϕ} ∪ ρL({0} : tϕ → ϕ), where ρL is defined as follows:

$$\begin{aligned} \rho\_L(S:t \to \mathbf{true}) &= \emptyset \\ \rho\_L(S:t \to \mathbf{false}) &= \{S:\neg t\} \\ \rho\_L(S:t \to (\psi\_1 \land \psi\_2)) &= \{S:\neg t \lor \eta(\psi\_1), S:\neg t \lor \eta(\psi\_2)\} \cup \delta\_L(S, \psi\_1) \cup \delta\_L(S, \psi\_2) \\ \rho\_L(S:t \to \psi) &= \{S:\neg t \lor \psi\} \\ \text{if } \psi &\text{ is a disjoint of literals} \\ \rho\_L(S:t \to (\psi\_1 \lor \psi\_2)) &= \{S:\neg t \lor \eta(\psi\_1) \lor \eta(\psi\_2)\} \cup \delta\_L(S, \psi\_1) \cup \delta\_L(S, \psi\_2) \\ \text{if } \psi\_1 \lor \psi\_2 \text{ is not a disjoint of literals} \\ \rho\_L(S:t \to \lozenge \psi) &= \{S:t \to \lozenge \eta(\psi)\} \cup \delta\_L(S^+, \psi) \end{aligned}$$

ρL(S : t → ✷ψ) = PL(S : t → ✷ψ) ∪ ΔL(S : t → ✷ψ)

η and δL are defined as follows:

$$\eta(\psi) = \begin{cases} \psi, & \text{if } \psi \text{ is a literal} \\ t\_{\psi}, & \text{otherwise} \end{cases} \quad \delta\_L(S, \psi) = \begin{cases} \emptyset, & \text{if } \psi \text{ is a literal} \\ \rho\_L(S: t\_{\psi} \to \psi), & \text{otherwise} \end{cases}$$

and functions PL and ΔL, are defined as shown in Table 4.

We can see in Table 4 that the reduction for KB4 has an additional SNFsml clause : t✷ψ ∨t✷¬t✷ψ that occurs neither in the reduction for KB nor in that for K4. It can be seen as an encoding of the derived axiom ✸✷ψ → ✷ψ that follows from the contrapositive ✸✷ψ → ψ of B and 4 ✷ψ → ✷✷ψ .

For K45 we see that all the SNFsml clauses in the reduction for K5 carry over. These clauses are already sufficient to ensure that, semantically, if t✷ψ is true at any world at a level other than 0, then t✷ψ is true at every world. Consequently, to accommodate axiom 4, it suffices to add the SNFsml clause {0} : t✷ψ → ✷t✷ψ to ensure that this also holds for the root world at level 0.

where lbP *K*Σ and lbδ *K*Σ are defined as follows

**Table 4.** Reduction of ✷-formulae, Σ ⊆ {B, 4, 5}.

For reductions of KDΣ and KTΣ we have favoured the reuse of reductions for KΣ, KD and KT over optimisation for specific logics. For example, take KBD. Given that in a symmetric model, every world w except the root world w0 has an R-successor, the axiom D only 'enforces' that w0 also has an R-successor. So, instead of adding a clause S : t✷ψ → ✸ψ for every clause S : t✷ψ → ✷η(ψ) we could just add {0} : t✷ψ → ✸ψ iff 0 ∈ S. Similarly, in KT5, because of 5, for all worlds w except w0 we already have wRw. So, we could again {0} : ¬t✷ψ ∨η(ψ) for every clause S : t✷ψ → ✷η(ψ) iff 0 ∈ S.

For the KB4-unsatisfiable formula ψ1 = (¬p ∧ ✸✸✷p), if we were to independently apply the reductions for KB and K4, that is, we compute {{0} : tψ1 } ∪ρKB({0} : tψ1 → ψ1)∪ρK4({0} : tψ1 → ψ1), then the result is the following set of clauses Φ1:

(1) {0} : tψ1 (2) {0} : ¬tψ1 ∨ ¬p (3) {0} : ¬tψ1 ∨ t✸✸✷p (4) {0} : t✸✸✷p → ✸t✸✷p (5) {1} : t✸✷p → ✸t✷p (6) {2}≥ : t✷p → ✷p (7) {2}≥ : t✷p → ✷t✷p (8) {1} : p ∨ t✷¬t✷p (9) {1} : t✷¬t✷p → ✷¬t✷p

Clauses (1) to (5) stem from the transformation of ψ1 to SNFsml for K, Clauses (6) and (7) stem from the reduction for 4 and Clauses (8) and (9) stem from the reduction for B. This set of SNFsml clauses is K-satisfiable. The clauses imply {1} : p, but neither {1} : ✷p nor {0} : p which we need to obtain a contradiction. Part of the reason is that we would need to apply the reduction for 4 and B recursively to newly introduced surrogates for ✷-formulae which in turn leads to the introduction of further surrogates and problems with the termination of the reduction.

In contrast, the clause set Φ2 obtained by our reduction for KB4 is:

$$\begin{array}{llll} \text{(10)} \ \{0\}: t\_{\psi\_{1}} & \text{(15)} \star: t\_{\Box p} \to \Box p & \text{(17)} \star: p \lor t\_{\Box \neg t\_{\Box p}}\\ \text{(11)} \ \{0\}: \neg t\_{\psi\_{1}} \vee \neg p & \text{(16)} \star: t\_{\Box p} \to \Box t\_{\Box p} & \text{(18)} \star: t\_{\Box \neg t\_{\Box p}} \to \Box \neg t\_{\Box p} \\ \text{(12)} \ \{0\}: \neg t\_{\psi\_{1}} \vee t\_{\Diamond \Diamond \Box p} & \text{(19)} \star: t\_{\Box p} \lor t\_{\Box \neg t\_{\Box \neg t\_{\Box p}}}\\ \text{(13)} \ \{0\}: t\_{\Diamond \Diamond \Box p} \to \Diamond t\_{\Diamond \Diamond p} & \text{(20)} \star: t\_{\Box \neg t\_{\Box \neg t\_{\Box p}}} \to \Box t\_{\Box \neg t\_{\Box p}}\\ \text{(14)} \ \{1\}: t\_{\Diamond \Diamond p} \to \Diamond t\_{\Box p} & \end{array}$$

Note Clauses (19) and (20) in Φ2 for which there are no corresponding clauses in Φ1. Also, the set of labels of Clauses (15) to (18) are strict supersets of those of the corresponding Clauses (6) to (9). Φ2 implies both {1} : ✷p and {0} : p. The latter, together with Clauses (10) and (11), means Φ2 is K-unsatisfiable.

**Theorem 1.** *Let* ϕ *be a modal formula in simplified NNF,* Σ ⊆ {B, D,T, 4, 5}*, and* ΦKΣ = ρsml KΣ (ϕ)*. Then* ϕ *is* KΣ*-satisfiable iff* ΦKΣ *is* K*-satisfiable.*

*Proof (Sketch).* For |Σ| ≤ 1 this follows from Theorem 5 in [29].

For K45, KB4, KDΣ , and KTΣ with Σ ⊆ {B, 4, 5} we proceed in analogy to the proofs of Theorems 3 and 4 in [29]. Let L be one of these logics.

To show that if ϕ is L-satisfiable then ΦL is K-satisfiable, we show that given a rooted L-model M of ϕ a small variation of the unravelling of M is a rooted tree K-model M L of ΦL. The main step is to define the valuation of the additional propositional symbols tψ so that we can prove that all clauses in ΦL hold in M L. To show that if ΦL is K-satisfiable then ϕ is L-satisfiable, we take a rooted tree K-model M = W, R, V, w0 of ΦL and construct a Kripke structure ML = W, RL,V,w0. The relation RL is the closure of R under the relational properties associated with the axioms of L. The proof that ML is a model of ϕ relies on the fact that the clauses in ΦL ensure that for subformulae ✷ψ of ϕ, ψ will be true at all worlds reachable via RL from a world where ✷ψ is true.

# **4 From SNF***sml* **to SNF***ml*

As KSP does not support SNFsml, in our evaluation of the effectiveness of the reductions defined in Sect. 3, we have used a transformation from SNFsml to SNFml. An alternative approach would be to reflect the use of SNFsml in the calculus and re-implement the prover. Whilst we believe that redesigning the calculus presents few problems, re-implementing KSP needs more thought in particular how to represent infinite sets. The route we adopt here allows us to experiment with the approach in general without having to change the prover. For extensions of K with one or more of the axioms B, D, T such a transformation

**Table 5.** Bounds on the length of prefixes in SST tableaux

is straightforward as the sets of modal levels occurring in the normal form of modal formulae are all finite. Thus, instead of a single SNFsml clause S : ¬tψ ∨ ηf (ψ) we can use the finite set of SNFml clauses {ml : ¬tψ ∨ ηf (ψ) | ml ∈ S}.

For extensions of K with at least one of the axioms 4 and 5, potentially together with other axioms, the sets of modal levels labelling clauses are in general infinite. For each logic L it is, however, possible to define a computable function that maps the modal formula ϕ under consideration onto a bound dbϕ L such that, restricting the modal levels in the normal form of ϕ by dbϕ L, preserves satisfiability equivalence.

To establish the bound and prove satisfiability equivalence, we need to introduce the basic notions of Single Step Tableaux (SST) calculi for a modal logic L [14,21], which uses sequences of natural numbers to prefix modal formulae in a tableau. The SST calculus consists of a set of rules, with the (π) rule being the only rule increasing prefixes' lengths (i.e., σ : ✸ϕ/σ.n : ϕ with σ.n new on the branch). For a logic L, an L*-tableau* T in the SST calculus for a modal formula ϕ is a (binary) tree where the root of T . is labelled with 1 : ϕ, and every other node is labelled with a prefixed formula σ : ψ obtained by application of a rule of the calculus. A *branch* B is a path from the root to a leaf. A *branch* B is *closed* if it contains either **false** or a propositional contradiction at the same prefix. A *tableau* "T is *closed* if all its branches are closed. A prefixed formula σ : ψ is *reduced for rule* (r) *in* B if the branch B already contains the conclusion of such rule application. By a *systematic tableau construction* we mean an application of the procedure in [14, p. 374] adapted to SST rules.

For each logic L, we establish its bound by considering an L-SST calculus, where a modal level in an SNFsml clause corresponds to the length of a prefix in an SST tableau. The bound then either follows from an already known bound on the length of prefixes in an SST tableau preserving correctness of the SST calculus, or we establish such a bound ourselves. To prove satisfiability equivalence, we show that, for a closed SST tableau with such a bound on the length of prefixes in place, we can construct a resolution refutation of a set of SNFsml or SNFml clauses with a corresponding bound on modal levels in those clauses.

For a modal formula ϕ in simplified NNF let dϕ m be the modal depth of ϕ, dϕ ✸ be the maximal nesting of ✸-operators not under the scope of any ✷ operators in ϕ, nϕ ✷ be the number of ✷-subformulae in ϕ, and nϕ ✸ be the number of ✸-subformulae below ✷-operators in ϕ. Our results for the bounds on the length of prefixes in SST tableaux can then be summarised by the following theorem.

**Theorem 2.** *Let* L = KΣ *with* Σ ⊆ {B, D,T, 4, 5}*. A systematic tableau construction of an* L*-tableau for a modal formula* ϕ *in simplified NNF under the following Constraints (TC1) and (TC2)*

*terminates in one of following states:*

The proof is analogous to Massacci's [21, Section B.2]. Note that for logics KD4 and KD5, we use max(1, nϕ ✸) in the calculation of the bound. That is, if nϕ ✸ ≥ 1 then max(1, nϕ ✸) = nϕ ✸ and the bound is the same as for K4 and K5. Otherwise max(1, nϕ ✸) = 1, that is, the bound is the same as for a formula with a single ✸-subformula below ✷-operators in ϕ.

For K, KD, KT, KB and KDB these bounds were already stated in [21, Tables III and IV]. The bound for KTB follows straightforwardly from that for KB and KDB. For KD4, Massacci [21, Tables III and IV] states the bound to be the same as for K4. However, this is not correct for the case that the formula ϕ contains no ✸-formulae, where its bound would simply be 2, independent of ϕ. For example, the formula ✷✷✷**false** which is KD4-unsatisfiable, does not have a closed KD4-tableau with this bound. For the other logics the bounds are new. As argued in [21], the bounds allow tableau decision procedures for extensions of K with axioms 4 and 5 that do not require a loop check and are therefore of wider interest.

Note that in KT4, ✷✷ψ and ✷ψ are equivalent and so are ✷(ψ∧✷ϑ) and ✷(ψ∧ ϑ). So, it makes sense to further simplify KT4 formulae using such equivalences before computing the normal form and the bound with the benefit that it may not only reduce the bound but also the size of the normal form. Similar equivalences that can be used to reduce the number of modal operators in a formula also exist for other logics, see, e.g., [8, Chapter 4].

To establish a relationship between closed tableaux and resolution refutations of a set of SNFml clauses, we formally define the modal layered resolution calculus. Table 6 shows the inference rules of the calculus restricted to labels occurring in our normal form. For GEN1 and GEN3, if the modal clauses in the premises occur at the modal level ml, then the literal clause in the premises occurs at modal level ml + 1.

Let Φ be a set of SNFml clauses. A *(resolution) derivation from* Φ is a sequence of sets Φ0, Φ1,... where Φ0 = Φ and, for each i > 0, Φi+1 = Φi ∪ {D}, where D ∈ Φi is the resolvent obtained from Φi by an application of one of the inference rules to premises in Φi. A *(resolution) refutation of* Φ is a derivation Φ0,...,Φk, k ∈ N, where 0 : **false** ∈ Φk.

To map a set of SNFsml clauses to a set of SNFml clauses, using a bound n ∈ N on the modal levels, we define a function dbn on clauses and sets of clauses in SNFsml as follows:

$$\begin{aligned} \mathrm{db}\_n(S:\varphi) &= \{ ml: \varphi \mid ml \in S \text{ and } ml \le n \} \\ \mathrm{db}\_n(\Phi) &= \bigcup\_{S: \varphi \in \Phi} \mathrm{db}\_n(S:\varphi) \end{aligned}$$

Note that prefixes in SST-tableaux have a minimal length of 1 while the minimal modal level in SNFml clauses is 0. So, a prefix of length n in a prefixed formula corresponds to a modal level n − 1 in an SNFml clause.

The proof of the following theorem then takes advantage of the fact that we have surrogates and associated clauses for each subformula of ϕ and proceeds by induction over applications of rule (π).

**Theorem 3.** *Let* L = KΣ *with* Σ ⊆ {B, D,T, 4, 5}*,* ϕ *be a* KΣ*-unsatisfiable formula in simplified NNF,* dbϕ L *be as defined in Table 5, and* ΦL = ρml L (ϕ) = dbdbϕ L−1(ρsml L (ϕ))*. Then there is a resolution refutation of* ΦL*.*

Regarding the size of the encoding, we note that, ignoring the labelling sets, the reduction ρsml L into SNFsml is linear with respect to the size of the original formula. The size including the labelling sets would depend on the exact representation of those sets, in particular, of infinite sets. As those are not arbitrary, there is still an overall polynomial bound on the size of the sets of SNFsml clauses produced by ρsml L . When transforming clauses from SNFsml into SNFml, we may need to add every clause to all levels within the bounds provided by Theorem 3. The parameters for calculating those bounds, dϕ m, dϕ ✸, nϕ ✸, and nϕ ✷, are all themselves linearly bound by the size of the formula. Thus, in the worst case, which is S4, the size of the clause set produced by ρml L is bounded by a polynomial of degree 3 with respect to the size of the original formula.

It is worth pointing out that both the reduction ρsml L of a modal formula to SNFsml and the reduction ρml L to SNFml are also reversible, that is, we can reconstruct the original formula from the SNFsml and from the SNFml clause set obtained by ρsml L or ρml L , respectively. This reconstruction can also be performed in polynomial time. Thus the reduction itself does not affect the complexity of the satisfiability problem. For instance, the satisfiability problem for S5 is NP-complete and so is the satisfiability problem of the subclass CS5 of SNFml clause sets that can be obtained as the result of an application of ρml S5 to a modal formula. However, a generic decision procedure for K will not be a complexityoptimal decision procedure for CS5.

#### **Table 6.** Inference rules of the MLR calculus

LRES : ml : D ∨ l ml : D ∨ ¬l ml : D ∨ D MRES : ml : l1 → ✷l ml : l2 → ✸¬l ml : ¬l1 ∨ ¬l2 GEN2 : ml : l 1 → ✷l1 ml : l 2 → ✷¬l1 ml : l 3 → ✸l2 ml : ¬l 1 ∨ ¬l 2 ∨ ¬l 3 GEN1 : ml : l 1 → ✷¬l1 . . . ml : l m → ✷¬lm ml : l → ✸¬l ml +1: l1 ∨ ... ∨ lm ∨ l ml : ¬l 1 ∨ ... ∨ ¬l m ∨ ¬l GEN3 : ml : l 1 → ✷¬l1 . . . ml : l m → ✷¬lm ml : l → ✸l ml +1: l1 ∨ ... ∨ lm ml : ¬l 1 ∨ ... ∨ ¬l m ∨ ¬l

#### **5 Evaluation**

An empirical evaluation of the practical usefulness of the reductions we presented in Sects. 3 and 4 faces the challenge that there is no substantive collection of benchmark formulae for the 15 logics of the modal cube except for basic modal logic. Catach [7] evaluates his prover on 31 modal formulae with a maximal length of 22 and maximal modal depth of 4. They are not sufficiently challenging. The QMLTP Problem Library for First-Order Modal Logics [32] focuses on quantified formulae and contains only a few formulae taken from the research literature that are purely propositional and were not written for the basic modal logic K. The Logics Workbench (LWB) benchmark collection [2] contains formulae for K, KT and S4 but not for any of the other logics we consider. For each of these three logics, the collection consists of 18 parameterised classes with 21 formulae each, plus scripts with which further formulae could be generated if needed. All formulae in 9 classes are satisfiable and all formulae in the other 9 classes are unsatisfiable in the respective logic.

In [29] we have used the 18 classes of the LWB benchmark collection for K to evaluate our approach for the six logics consisting of K and its extensions with a single axiom. One drawback of using these 18 classes for other modal logics is that formulae that are K-satisfiable are not necessarily KΣ-satisfiable for non-empty sets Σ of additional axioms. For example, for K5, only 60 out of 180 K-satisfiable formulae were K5-satisfiable. Another drawback is that while K-unsatisfiable formulae are also KΣ-unsatisfiable, a resolution refutation would not necessarily involve any of the additional clauses introduced by our reduction for KΣ. It may be that the additional clauses allow us to find a shorter refutation, but it may just be a case of finding the same refutation in a larger search space. It is also worth recalling that simplification alone is sufficient to determine that all formulae in the class k lin p are K-unsatisfiable while pure literal elimination can be used to reduce all formulae in k grz p to the same simple formula [26].

**Table 7.** Logic-specific modification of unsatisfiable benchmark formulae

Thus, some of the classes evaluate the preprocessing capabilities of a prover but not the actual calculus and its implementation.

We therefore propose a different approach here. The principles underlying our approach are that (i) there should be the same number of formulae for each logic though not necessarily the same formulae across all logics; (ii) there should be an equal number of satisfiable and unsatisfiable formulae for each logic; (iii) a formula that is L-unsatisfiable should only be L -unsatisfiable for every extension L of L; (iv) a formula that is L -satisfiable should be L-satisfiable for every extension L of L; (v) the formulae should belong to parameterised classes of formulae of increasing difficulty. Note that Principles (iii) and (iv) are intentionally not symmetric. For L-unsatisfiable formulae it should be necessary for a prover to use the rules or clauses specific to L instead of being able to find a refutation without those. For L-satisfiable formulae we want to maximise the search space for a model.

For unsatisfiable formulae, we take the five LWB classes k branch p, k path p, k ph p, k poly p, k t4p p and for each logic L in the modal cube transform each formula in a class so that is L-unsatisfiable, but L -satisfiable for any logic L that is not an extension of L. The transformation proceeds by first converting a formula ϕ to simplified NNF. Then for each propositional literal l it replaces all its occurrences by (l∨ψp L) where |l| = p and ψp L is a modal formula uniquely associated with p and L, resulting in a formula ϕ . Finally, for logics KD4 and KDB we need to add a disjunct (✷q ∧ ✷¬q) to ϕ , while for logics S4 and KTB we need to add a disjunct (q ∧✷¬q), where q is a propositional symbol not occurring in ϕ . These disjuncts are unsatisfiable in the respective logics but satisfiable in logics where D, or T, do not hold. Table 7 shows the formulae ψp L that we use in our evaluation. In the table, qp and q p are propositional variables uniquely associated with p that do not occur in ϕ. The overall effect of this transformation is that the resulting classes of formulae satisfy Principles (iii) and (v).

For satisfiable formulae, we use the five classes k poly n, s4 md n, s4 ph n, s4 path n, s4 s5 n without modification. Although the first of these classes was designed to be K-satisfiable and the other four to be S4-satisfiable, the formulae in those classes are satisfiable in all the logics we consider. s4 ipc n also consists

**Table 8.** Benchmarking results

only of S5-satisfiable formulae but these appear to be insufficiently challenging and have not been included in our benchmark set. All other classes of the LWB benchmark classes for K and S4 are satisfiable in some of the logics, but not in all. The five classes satisfy Principles (iv) and (v). The benchmark collection consisting of all ten classes together then also satisfies Principles (i) and (ii).

Another challenge for an empirical evaluation is the lack of available fully automatic theorem provers for all 15 logics that we have already discussed in Sect. 1. This leaves us with just three different approaches we can compare (i) the higher-order logic prover LEO-III [12,37], with **E** 2.6 as external reasoner, *LEO-III+E for short*, that supports a wide range of logics via semantic embedding into higher-order logic (ii) the combination of our reductions with the modallayered resolution (MLR) calculus for SNFml clauses [25], *R+MLR calculus for short*, implemented in the modal theorem prover KSP (iii) the global modal resolution (GMR) calculus, implemented in KSP, which has resolution rules for all 15 logics [24]. For R+MLR and GMR calculi, resolution inferences between literal clauses can either be unrestricted (cplain option), restricted by negative resolution (cneg option), or restricted by an ordering (cord option). It is worth pointing out that negative and ordered resolution require slightly different transformations to the normal form that introduce additional clauses (snf+ and snf++ options, respectively). Also, the ordering cannot be arbitrary [25]. For the experiments, we have used the following options: (i) input processing: prenexing, together with simplification and pure literal elimination (bnfsimp, prenex, early ple); (ii) preprocessing of clauses: renaming reuses symbols (limited reuse renaming), forward and backward subsumption (fsub, bsub) are enabled; the usable is populated with clauses whose maximal literal is positive (populate usable, max lit positive); pure literal elimination is set for GMR (ple) and modal level ple is set for MLR (mlple); (iii) processing: inference rules not required for completeness are also used (unit, lhs unit,mres), the options for preprocessing of clauses are kept and clause selection takes the shortest clause by level (shortest).

For LEO-III we provide the prover with a modal formula in the syntax it expects plus a logic specification that tells the prover in which modal logic the formula is meant to be solved, for example, \$modal system S4. LEO-III can collaborate with external reasoners during proof search and we have used **E** 2.6 [34,35] as external reasoner and restricted LEO-III to one instance of **E** running in parallel. LEO-III is implemented in Java and we have set the maximum heap size to 1 GB and the thread stack size to 64 MB for the JVM.

Table 8 shows our benchmarking results. The first three columns of the table show the logic in which we determine the satisfiability status of each formula, the satisfiability status of the formulae, and their number. The next six columns then show how many of those formulae were solved by KSP with a particular calculus and refinement. The last column shows the result for LEO-III. The highest number or numbers are highlighted in bold. A time limit of 100 CPU seconds was set for each formula. Benchmarking was performed on a PC with an AMD Ryzen 5 5600X CPU @ 4.60 GHz max and 64 GB main memory using Fedora release 34 as operating system.

While the R+MLR calculus is competitive with GMR on extensions of K with axioms D, T and, possibly, B, the GMR calculus has better performance on extensions with axioms 4 and 5.

On satisfiable formulae, where for all logics we use exactly the same formulae and both resolution calculi have to saturate the set of clauses up to redundancy, the number of formulae solved is directly linked to the number of inferences necessary to do so. The fact that we reduce SNFsml clauses to SNFml clauses via the introduction of multiple copies of the same clausal formulae with different labels clearly leads to a corresponding multiplication of the inferences that need to be performed. LEO-III+E does not solve any of the satisfiable formulae. This can be seen as an illustration of how important the use of additional techniques is that can turn resolution into a decision procedure on embeddings of modal logics into first-order logic [18,33].

On unsatisfiable formulae, where we use different formulae for each logic, the number of formulae solved is linked to the number of inferences it takes to find a refutation. For instance, on K it takes the GMR calculus on average 6.2 times the number of inferences to find a refutation than the R+MLR calculus. However, for all other logics the opposite is true. On the remaining 14 logics, the R+MLR calculus on average requires 6.5 times the number of inferences to find a refutation than the GMR calculus. Given that the R+MLR calculus currently uses a reduction from a modal logic to SNFsml followed by a transformation from SNFsml to SNFml, it is difficult to discern which of the two is the major problem. It is clear that multiple copies of the same clausal formulae are also detrimental to proof search. LEO-III+E does reasonably well on unsatisfiable formulae and the results clearly show the impact that additional axioms have on its performance. It performs best for KT and K but for logics involving axioms 4 and 5 very few formulae can be solved. The external prover **E** finds the proof for 121 out of the 122 modal formulae LEO-III+E can solve.

## **6 Conclusions**

We have presented novel reductions of extensions of the modal logic K with arbitrary combinations of the axioms B, D, T, 4, 5 to clausal normal forms SNFsml and SNFml for K. The implementation of those reductions combined with KSP [26], allows us to reason in all 15 logics of the modal cube in a fully automatic way. Such support was so far extremely limited.