Local is Best: Efficient Reductions to Modal Logic K

The main motivation for reducing problems in one logic (the source logic) to ‘equivalent’ problems in another formalism is to exploit results and tools for that formalism to solve theoretical or practical problems in the source logic. For propositional modal logics, this approach has been researched extensively for reductions of the satisfiability problem in these logics to the satisfiability problem in ‘stronger’ logics such as first-order logic [14, 26], second-order theory of n successors [7], simple type theory [4], and regular grammar logics [25].

An alternative approach is to reduce propositional modal logics to a ‘weaker’ logic, in particular, the basic modal logic \({\textsf {K} }\). For extensions of \({\textsf {K} }\) with one of the axioms \(\textsf {B} \), \(\textsf {D} \), \(\textsf {a}lt _\textsf {1} \), \(\textsf {T} \), and \(\textsf {4} \), Kracht [17] defines reduction functions of their global and local satisfiability problem to the corresponding problem in \({\textsf {K} }\) and proves their correctness. He also defines a reduction function for \({\textsf {K5} }\), the extension of \({\textsf {K} }\) with \(\textsf {5} \), to \({\textsf {K4} }\), but this reduction is incorrect as not all theorems of \({\textsf {K4} }\) are theorems of \({\textsf {K5} }\). Several features of Kracht’s approach are relevant to our work. First, as is not uncommon in modal logic, he uses \(\Box \) as the only modal operator occurring in modal formulae and the modal operator \(\Diamond \) is expressed as \(\lnot \Box \lnot \). This negatively impacts the size of the resulting formulae as the reduction functions cannot treat the modal operators \(\Box \) and \(\Diamond \) differently (as we do here). Second, the basic idea underlying his reduction functions is the following: given a modal formula \(\varphi \), generate sufficiently many instances \(\Delta \) of a modal axiom \(\Lambda \) so that \(\varphi \) is \({\textsf {K} }\Lambda \)-satisfiable iff \(\varphi \wedge \Delta \) is \({\textsf {K} }\)-satisfiable. Third, Kracht is concerned with preservation of the computational complexity of the satisfiability problem under consideration, as well as the preservation of other theoretical properties. For instance, the local satisfiability problem in the modal logics covered by Kracht is PSPACE-complete. So, it is sufficient to ensure that \(\Delta \) is polynomial in size with respect to \(\varphi \). As Kracht himself concludes, his method offers a uniform way of transferring results about one modal logic to another, but may not be as useful for practical applications.

In [21, 23], we have introduced a new normal form for basic multi-modal logic, called Separated Normal Form with Modal Levels, \(\textsf {SNF}_{ml}\), which uses labeled modal clauses. These labels refer to the level within a tree Kripke structure at which a modal clause holds. This can be seen as a compromise between approaches that label formulae with worlds at unspecified level [1, 3] and approaches that label formulae with paths [6, 30]. A combination of a normal form transformation for modal formulae and a resolution-based calculus for labeled modal clauses can then be used to decide local and global satisfiability in basic modal logic. In [22, 24], we have presented \({\text {K}_{\text {S}}}{\text {P}}\), an implementation of that calculus, together with an experimental evaluation that indicates that \({\text {K}_{\text {S}}}{\text {P}}\) performs well if propositional variables are evenly spread across a wide range of modal levels within the formulae one wants to decide.

A feature of \(\textsf {SNF}_{ml}\) is its use of additional propositional symbols as ‘surrogates’ for subformulae of a modal formula \(\varphi \). In the following, we take advantage of the availability of those surrogates to provide a novel transformation from extensions of \({\textsf {K} }\) with a single one of the axioms \(\textsf {B} \), \(\textsf {D} \), \(\textsf {T} \), \(\textsf {4} \) and \(\textsf {5} \) to \(\textsf {SNF}_{ml}\). Another novel aspect is that we modify the normal form so that it uses sets of modal levels as labels instead of a single modal level. In \({\textsf {K} }\), we only need a definition of a surrogate at the modal level at which the corresponding subformula occurs in \(\varphi \). But in \({\textsf {KB} }\), \({\textsf {KT} }\), \({\textsf {K4} }\) and \({\textsf {K5} }\), we need a definition at every reachable modal level, of which there can be many. We call the resulting normal form, Separated Normal Form with Sets of Modal Levels, \(\textsf {SNF}_{sml}\).

The structure of the paper is as follows. In Sect. 2, we recap common concepts of propositional modal logic including its syntax and semantics. Section 3 defines \(\textsf {SNF}_{sml}\). Section 4 defines the reductions of \({\textsf {K} }\), \({\textsf {KB} }\), \({{\textsf {KD} }}\), \({\textsf {KT} }\), \({\textsf {K4} }\) and \({\textsf {K5} }\) to \(\textsf {SNF}_{sml}\); correctness results are given in Sect. 5. Sect. 6 shows a reduction from \(\textsf {SNF}_{sml}\) to \(\textsf {SNF}_{ml}\) and its correctness; the reduction is needed to evaluate our result via \({\text {K}_{\text {S}}}{\text {P}}\). Related work is discussed in Sect. 7. In Sect. 8, we compare the performance of a combination of our reductions and the modal-layered resolution calculus implemented in \({\text {K}_{\text {S}}}{\text {P}}\) with resolution calculi specifically designed for the logics under consideration and with translation-based approaches built into the first-order theorem prover SPASS and the higher-order logic prover LEO-III. Section 9 provides concluding remarks and future work.

This paper is an extended and revised version of [29]. We provide correctness proofs for our reductions for \({\textsf {K4} }\) and \({\textsf {K5} }\) that were not included in [29]. Section 6 is new and not only defines a satisfiability preserving transformation from \(\textsf {SNF}_{sml}\) (with infinite sets of labels) to \(\textsf {SNF}_{ml}\), but also proves its correctness via a simulation of Massacci’s Single Step Tableaux (SST) calculus [18] for \({\textsf {K4} }\) and \({\textsf {K5} }\) using the modal-layered resolution calculus for \(\textsf {SNF}_{ml}\) clauses [21]. For \({\textsf {K5} }\), we also establish a bound on the length of prefixes in the SST calculus that preserves refutation completeness of the calculus without need for a loop check.

The language of modal logic is an extension of the language of propositional logic with unary modal operators \(\Box \) and \(\Diamond \). More precisely, given a denumerable set of propositional symbols, \(P= \{p, p_0, q, q_0, t, t_0,\ldots \}\) as well as propositional constants \(\mathbf{true}\) and \(\mathbf{false}\), modal formulae are inductively defined as follows: constants and propositional symbols are modal formulae. If \(\varphi \) and \(\psi \) are modal formulae, then so are \(\lnot \varphi \), \((\varphi \wedge \psi )\), \((\varphi \vee \psi )\), \((\varphi \rightarrow \psi )\), \(\Box \varphi \), and \(\Diamond \varphi \). We also assume that \(\wedge \) and \(\vee \) are associative and commutative operators and consider, e.g., \((p\vee (q\vee r))\) and \((r\vee (q\vee p))\) to be identical formulae. We often omit parentheses if this does not cause confusion. By \(\mathsf {var} (\varphi )\), we denote the set of all propositional symbols occurring in \(\varphi \). This function straightforwardly extends to finite sets of modal formulae. A modal axiom (schema) is a modal formula \(\psi \) representing the set of all instances of \(\psi \).

A literal is either a propositional symbol or its negation; the set of literals is denoted by \(L_{P}\). We denote by \(\lnot l\) the complement of the literal \(l\in L_{P}\), that is, \(\lnot l\) denotes \(\lnot p\) if l is \(p \in P\), and \(\lnot l\) denotes p if l is the literal \(\lnot p\). A modal literal is either \(\Box l\) or \(\Diamond l\), where \(l \in L_{P}\).

A (normal) modal logic is a set of modal formulae which includes all propositional tautologies, the axiom schema \(\Box {(\varphi \rightarrow \psi )} \rightarrow (\Box {\varphi } \rightarrow \Box {\psi })\), called the axiom \(\textsf {K} \), is closed under modus ponens (if \(\vdash {} \varphi \) and \(\vdash {} \varphi \rightarrow \psi \) then \(\vdash {}\psi \)) and the rule of necessitation (if \(\vdash {}\varphi \) then \(\vdash {} \Box {\varphi }\)). \({\textsf {K} }\) is the weakest modal logic, that is, the logic given by the smallest set of modal formulae constituting a normal modal logic. By \({\textsf {K} }\varSigma \), we denote an extensions of \({\textsf {K} }\) by a set \(\varSigma \) of axioms.

The standard semantics of modal logics is the Kripke semantics or possible world semantics. A Kripke frame \(F\) is an ordered pair \(\langle W, R \rangle \) where \(W\) is a non-empty set of worlds and \(R\) is a binary (accessibility) relation over \(W\). A Kripke structure \(M\) over \(P\) is an ordered pair \(\langle F,V \rangle \) 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\). We say \(M= \langle F,V \rangle \) is based on the frame \(F\). A rooted Kripke structure is an ordered pair \(\langle M,w_0 \rangle \) with \(w_0\in W\). In the following, we write \(\langle W, R, V \rangle \) and \(\langle W, R, V,w_0 \rangle \) instead of \(\langle \langle W, R \rangle , V \rangle \) and \(\langle \langle \langle W, R \rangle , V \rangle ,w_0 \rangle \), respectively.

Satisfaction (or truth) of a formula at a world \(w\) of a Kripke structure \(M= \langle W, R, V \rangle \) is inductively defined by:If \(\langle M, w \rangle \models \varphi \) holds then \(M\) is a model of \(\varphi \), \(\varphi \) is true at w in \(M\) and \(M\) satisfies \(\varphi \). A modal formula \(\varphi \) is satisfiable iff there exists a Kripke structure \(M\) and a world w in \(M\) such that \(\langle M, w \rangle \models \varphi \).

In the following, we are interested in extensions of \({\textsf {K} }\) with one of the axiom schemata shown in Table 1. Each of these axiom schemata defines a class of Kripke frames where the accessibility relation \(R\) satisfies the first-order property stated in the table.

Given a normal modal logic L with corresponding class of frames \(\mathfrak {F}\), we say a modal formula \(\varphi \) is L-satisfiable iff there exists a frame \(F\in \mathfrak {F}\), a valuation V and a world \(w_0\in F\) such that \(\langle F,V,w_0 \rangle \models \varphi \).

A path rooted at \(w\) of length k, \(k\ge 0\), in a frame \(F = \langle W,R \rangle \) is a sequence \(\vec {w} = (w_0,w_1,\ldots ,w_k)\) where for every i, \(1\le i\le k\), \(w_{i-1}\mathbin {\!R\!}w_i\). We say that the path \((w_0,w_1,\ldots ,w_k)\) connects \(w_0\) and \(w_k\). For a path \(\vec {w} = (w_0,\ldots ,w_k)\) and world \(w_{k+1}\) with \(w_k\mathbin {R}w_{k+1}\), \(\vec {w}\circ w_{k+1}\) denotes the path \((w_0,\ldots ,w_k,w_{k+1})\). A path \((w_0)\) of length 0 is identified with its root \(w_0\). We denote the set of all paths rooted at a world \(w_0\) in \(F\) by \(\vec {F}[w_0]\) and the set of all paths by \(\vec {F}\). The function \(\mathsf {trm}: \vec {F}\rightarrow W\) maps every path \(\vec {w} = (w_0,\ldots ,w_k)\) to its terminal world \(w_k\) while the function \(\mathsf {len}:\vec {F}\rightarrow {\mathbb N}\) maps every path \(\vec {w} = (w_0,w_1,\ldots ,w_k)\) to its length k.

A rooted Kripke structure \(M = \langle W,R,V,w_0 \rangle \) 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 \(w_0\). It is a rooted tree Kripke model of a modal formula \(\varphi \) iff \(\langle W,R,V,w_0 \rangle \models \varphi \). In a rooted tree Kripke structure with root \(w_0\) for every world \(w_k\in W\) there is exactly one path \(\vec {w}\) connecting \(w_0\) and \(w_k\); the modal level of \(w_k\) (in M), denoted by \(\mathsf {ml}_{M}(w_k)\), is given by \(\mathsf {len}(\vec {w})\).

Let \(F = \langle W, R \rangle \) be a Kripke frame with \(w\in W\). The unraveling \(F^u[w]\) of \(F\) at \(w\) is the frame \(\langle \vec {W}, \vec {R} \rangle \) where:Let \(F=\langle W, R \rangle \) and \(F'=\langle W', R' \rangle \) be two Kripke frames. A function \(f :W\mapsto W'\) is a p-morphism (or a bounded morphism) from \(F\) to \(F'\) if the following holds:Analogously for Kripke models. For \(F = \langle W,R \rangle \), \(M = \langle F,V,w_0 \rangle \), and the function \(\mathsf {trm}\) is a p-morphism from \(M'\) to \(M\).

When considering satisfiability, the following holds (see, [12]):

For the normal form transformation presented in the next section we assume that any modal formula \(\varphi \) has been simplified by exhaustively applying the rewrite rules in Table 2 and 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.

In [21], we have introduced a novel clausal normal form, called Separated Normal Form with Modal Levels, \(\textsf {SNF}_{ml}\), whose language extends that of the basic modal logic \({\textsf {K} }\) with labels for modal levels. Clauses in \(\textsf {SNF}_{ml}\) have one of the following forms:where \(ml\in {\mathbb N}\cup \{{\star }\}\) and l, \(l'\), \(l_b\) are propositional literals with \(1 \le b \le r\), \(r \in {\mathbb N}\). Clauses \({\star }:\psi \) are global clauses.

Given a rooted tree Kripke structure M, the satisfiability of an \(\textsf {SNF}_{ml}\) clause is defined as follows:The label \({\star }\) only occurs in the clausal normal form of a modal formula \(\varphi \) if we consider the problem whether there exists a Kripke structure \(M\) such that \(\varphi \) is true at all worlds of \(M\). For satisfiability of \(\varphi \) all labels will be from a finite subset of \({\mathbb N}\). In this case the labels can be seen as a compromise between a normal form where even for local satisfiability all clauses are global and a normal form that uses paths to constrain a clause to just a subset of all worlds at a particular modal level.

A feature of our reductions is that the same formula \(\bigvee _{b=1}^{r} l_b\), \(l' \rightarrow \Box l\), or \(l' \rightarrow \Diamond l\) may have to hold at several levels, possibly even an infinite number of levels. It therefore makes sense to label such formulae not with just a single level but a set of levels. We call this normal form Separated Normal Form with Sets of Modal Levels, \(\textsf {SNF}_{sml}\). Informally, the labels in \({\textsf {SNF}}_{sml}\) state that a formula is satisfied at all worlds in a given set of modal levels, instead of a single modal level as in \({\textsf {SNF}}_{ml}\). We write \(S: \varphi \), where S is a set of natural numbers, to denote that a formula \(\varphi \) is true at all modal levels \(ml\in S\). We write \({\star }: \varphi \) instead of \({\mathbb N}:\varphi \).

Formally, given a rooted tree Kripke structures \(M = \langle W,R,V,w_0 \rangle \) and a set of modal levels S, by M[S], we denote the set of worlds that are at a modal level in S, that is, \(M[S] = \{w\in W\mid \mathsf {ml}_{M}(w)\in S\}\). The satisfaction of labeled formulae in M is then defined as follows:If \(M\models S: \varphi \), then we say that \(S: \varphi \) holds in \(M\) or is true in \(M\). For a set \(\varPhi \) of labeled formulae, \(M\models \varPhi \) iff \(M\models S:\varphi \) for every \(S:\varphi \) in \(\varPhi \), and we say \(\varPhi \) is \({\textsf {K} }\)-satisfiable.

Note that if \(S=\emptyset \), then \(M\models S: \varphi \) trivially holds. Also, \(S:\mathbf{false}\) with \(0\not \in S\), is not in itself unsatisfiable, a Kripke structure \(M\) can satisfy \(S:\mathbf{false}\) if it has no worlds w with \(\mathsf {ml}_{M}(w)\in S\). On the other hand, \(S:\mathbf{false}\) with \(0\in S\) is unsatisfiable as a rooted tree Kripke structure always has a world with modal level 0.

A labeled modal formula is then an \(\textsf {SNF}_{sml}\) clause iff it is of one of the following forms:where \(S \subseteq {\mathbb N}\) and l, \(l'\), \(l_b\) are propositional literals with \(1 \le b \le r\), \(r \in {\mathbb N}\). Positive and negative modal clauses are together known as modal clauses. We regard a literal clause as a set of literals, that is, two clauses are the same if they contain the same set of literals.

In the following, we assume that the set \(P\) of propositional symbols is partitioned into two infinite sets Q and T such that Q contains the original propositional symbols and T surrogate symbols \(t_\psi \) and supplementary propositional symbols. In particular, for every modal formula \(\psi \), we have \(\mathsf {var}(\psi )\subset Q\) and there exists a propositional symbol \(t_\psi \in T\) uniquely associated with \(\psi \).

We introduce some notation that will be used in the following. Let \(S^+= \{l + 1\in {\mathbb N}\mid l \in S\}\), \(S^- = \{ l - 1 \in {\mathbb N}\mid l \in S\}\), and \(S^\ge = \{n \mid n \ge {\textsf {min}}(S)\}\), where \(\textsf {min}(S)\) is the least element in S. Note that the restriction of the elements being in \({\mathbb N}\) implies that \(S^-\) cannot contain negative numbers.

Given a modal formula \(\varphi \) in simplified NNF and \(L\in \{{\textsf {K} }, {\textsf {KB} }, {\textsf {KD} }, {\textsf {KT} }, {\textsf {K4} }, {\textsf {K5} }\}\), then we can obtain a set \(\varPhi _L\) of clauses in \(\textsf {SNF}_{sml}\) such that \(\varphi \) is L-satisfiable iff \(\varPhi _L\) is \({\textsf {K} }\)-satisfiable as \(\varPhi _L =\{\{ 0 \}: t_\varphi \}\cup \rho _{L}(\{0\}:t_\varphi \rightarrow \varphi )\), where \(\rho _{L}\) is defined as follows:where \(\eta \) and \(\delta _{L}\) are defined as follows:and functions \(P_{L}\), \(\Delta _{L}\) are defined as shown in Table 3.

The function \(\eta \) maps a propositional literal \(\psi \) to itself while it maps every other modal formula \(\psi \) to a new propositional symbol \(t_\psi \in T\) uniquely associated with \(\psi \). We call \(t_\psi \) the surrogate of \(\psi \) or simply a surrogate. The functions \({P_{{\textsf {\textit{KB}}}}}\) and \({P_{{\textsf {\textit{K5}}}}}\) introduce additional propositional symbols, called supplementary propositional symbols, \(t_{\Box \lnot t_{\Box \psi }}\in T\) and \(t_{\Diamond t_{\Box \psi }}\in T\), respectively, that do not correspond to subformulae of the formula we are transforming.

For \({P_{{\textsf {\textit{KT}}}}}\), \({P_{{\textsf {\textit{KD}}}}}\) and \({P_{{\textsf {\textit{K4}}}}}\) the additional clauses \(S : \lnot t_{\Box \psi }\vee \eta (\psi )\), \(S : t_{\Box \psi }\rightarrow \Diamond \eta (\psi )\) and \(S : t_{\Box \psi }\rightarrow \Box t_{\Box \psi }\), respectively, are directly based on the axiom schemata. Intuitively, \({P_{{\textsf {\textit{KB}}}}}\) is based on the following consideration: take a world w in a Kripke structure \(M\) with a symmetric accessibility relation \(R\). If there exists a world v with \(w\!\mathbin {R}\!v\) such that \(\langle M, v \rangle \models \Box \psi \), then \(\langle M, w \rangle \models \psi \). Now, take the contrapositive of that statement: If \(\langle M, w \rangle \not \models \psi \), then for every world v with \(w\mathbin {\!R\!}v\), \(\langle M, v \rangle \not \models \Box \psi \). Equivalently, \(\langle M, w \rangle \models \psi \) or \(\langle M, w \rangle \models \Box \lnot \!\Box \!\psi \). This is expressed by the formula \(\eta (\psi )\vee t_{\Box \lnot t_{\Box \psi }}\). For \({P_{{\textsf {\textit{K5}}}}}\), the formula \(t_{\Diamond t_{\Box \psi }}\rightarrow \Box t_{\Diamond t_{\Box \psi }}\) expresses an instance of axiom schema \({{{\textsf {\textit{5}}}}}\), \(\Diamond \varphi \!\rightarrow \Box \!\Diamond \!\varphi \), with \(\varphi = \Box {\psi }\), i.e., \(\Diamond \!\Box \!\psi \rightarrow \Box \!\Diamond \!\Box \psi \). The contrapositive of axiom schema \(\textsf {5} \) is \(\Diamond \Box \varphi \rightarrow \Box \varphi \), equivalent to \(\lnot \Diamond \!\Box \varphi \vee \Box \varphi \). For \(\varphi =\psi \) this is expressed by the formula \(\lnot t_{\Diamond t_{\Box \psi }}\vee t_{\Box \psi }\). For the formula \(\lnot t_{\Diamond t_{\Box \psi }}\rightarrow \Box \lnot t_{\Box \psi }\), consider \(\lnot \!\Diamond \!\Box \!\psi \). By duality of \(\Box \) and \(\Diamond \), this is equivalent to \(\lnot \lnot \!\Box \!\lnot \!\Box \!\psi \) and \(\Box \lnot \!\Box \!\psi \). So, \(\lnot \!\Diamond \!\Box \psi \rightarrow \Box \lnot \!\Box \!\psi \) in every normal modal logic, not only \({\textsf {K5} }\). The remaining labeled formulae introduced by \({P_{{\textsf {\textit{KB}}}}}\) and \({P_{{\textsf {\textit{K5}}}}}\) ensure that supplementary propositional symbols are defined.

To simplify presentation in the following, we define a function \(\eta _f\) as follows:and we treat the two clauses \(S: \lnot t_{\psi _1\wedge \psi _2} \vee \eta (\psi _1)\) and \(S: \lnot t_{\psi _1\wedge \psi _2} \vee \eta (\psi _2)\) resulting from the normal form transformation of \(\psi _1\wedge \psi _2\) as a single ‘clause’ \(S: \lnot t_{\psi _1\wedge \psi _2} \vee \eta _f(\psi _1\wedge \psi _2)\). We also interchangeably write \(S:\lnot t_{\Box \psi }\vee \eta _f(\Box \psi )\) for \(S:t_{\Box \psi }\rightarrow \eta _f(\Box \psi )\) and, analogously, \(S:\lnot t_{\Diamond \psi }\vee \eta _f(\Diamond \psi )\) for \(S:t_{\Diamond \psi }\rightarrow \eta _f(\Diamond \psi )\). We then call any clause of the form \(S:\lnot t_\psi \vee \eta _f(\psi )\) a definitional clause.

As \({\text {K}_{\text {S}}}{\text {P}}\) does not support \(\textsf {SNF}_{sml}\), in our evaluation of the effectiveness of the reductions defined in Sect. 4, we have used a transformation from \(\textsf {SNF}_{sml}\) to \(\textsf {SNF}_{ml}\). For \({\textsf {KD} }\), \({\textsf {KT} }\), \({\textsf {KB} }\) such a transformation is straightforward as the sets of modal levels occurring in the normal form of modal formulae are all finite. Thus, instead of a single \(\textsf {SNF}_{sml}\) clause \(S:\lnot t_\psi \vee \eta _f(\psi )\), we can use the finite set of \(\textsf {SNF}_{ml}\) clauses \(\{ml:\lnot t_\psi \vee \eta _f(\psi )\;|\;ml\in S\}\).

However, for \({\textsf {K4} }\) and \({\textsf {K5} }\) the sets of modal levels labeling clauses are in general not finite. But just as in first-order clausal logic where for every unsatisfiable clause set, there exists a finite subset of its Herbrand expansion that is unsatisfiable, for every unsatisfiable set of \(\textsf {SNF}_{sml}\) clauses \(\varPhi \), there exists an unsatisfiable set of \(\textsf {SNF}_{sml}\) clauses \(\varPhi ' = \{S':C\;|\;S:C\in \varPhi \}\) such that all sets of modal levels \(S'\) are finite. The question is whether there is a computable function that can generate \(\varPhi '\) from \(\varPhi \).

This is indeed the case. For \({\textsf {K4} }\), we can take advantage of a bound established by Massacci [18] on the length of prefixes in SST depending on the modal formula \(\varphi \) under consideration. We can use that bound to limit the maximal modal level occurring in a set of modal levels S labeling \(\textsf {SNF}_{sml}\) clauses. As all such sets are finite we can straightforwardly use a finite set of \(\textsf {SNF}_{ml}\) clauses instead. In order to establish that this approach preserves completeness, we show that for every closed tableaux for a modal formula \(\varphi \) in simplified NNF in the SST (SST) calculus with prefixes limited by Massacci’s bound, we can construct a resolution refutation from a set of \(\textsf {SNF}_{ml}\) clauses for \(\varphi \) where modal levels are subject to a corresponding bound. Completeness then follows from Massacci’s result that the SST calculus with that bound is still refutationally complete.

Formally, the SST calculus uses prefixed formulae, that is, pairs \(\sigma : \varphi \), where the prefix \(\sigma \) is a non-empty sequence of natural numbers and \(\varphi \) is a modal formula. Intuitively, \(\sigma \) “names” a world that satisfies \(\varphi \). In the following, \(\sigma \) is a prefix, \(\sigma _0 . \sigma _1\) the concatenation of the sequence \(\sigma _0\) with the sequence \(\sigma _1\) and \(\sigma .n\) the concatenation of \(\sigma \) with n. If \(\sigma = n_1 . n_2 . \ldots . n_{k-1} . n_k\) is a prefix, the length of the prefix \(\sigma \) is k and is denoted by \(|\sigma |\). For a logic L, an L-tableau \(\mathscr {T}\) in the SST calculus is a (binary) tree where each node is labeled with a prefixed formula. Nodes other than the root node are labeled with a second prefixed formula, its premise, and with the name of the SST rule that was applied to the premise to obtain the formula labeling the node. An L-tableau \(\mathscr {T}\) is an L-tableau for the modal formula \(\varphi \) if the root of \(\mathscr {T}\) is labeled with \(1:\varphi \). An L-branch \(\mathscr {B}\) is a path from the root to a leaf while a partial L-branch \(\mathscr {B}\) is path from the root to some node in the tree. Given a partial L-branch \(\mathscr {B} = (m_0,\ldots ,m_k)\) and a path \(\mathcal {P} = (n_1,\ldots ,n_l)\) in \(\mathscr {T}\) such that \(n_1\) is a child of \(m_k\), then \(\mathscr {B}\circ \mathcal {P}\) denotes the partial L-branch \(\mathscr {B}' = (m_0,\ldots ,m_k,n_1,\ldots ,n_l)\). The SST rules for \({\textsf {K4} }\) consist of (\(\alpha \)), (\(\beta \)), (\(\pi \)), (K) and (4) in Table 4 while the SST rules for \({\textsf {K5} }\) consist of (\(\alpha \)), (\(\beta \)), (\(\pi \)), (K), (\(4^{R}\)), (\(4^{D}\)) and (\(Cxt^{1}\)). Nodes are added to a tableau \(\mathscr {T}\) and labeled as follows: if the antecedent \(\sigma :\psi \) of a SST rule (r) labels a node on a branch \(\mathscr {B}\), then we extend the branch with nodes labeled with the consequents of the rule and each of those nodes is labeled with \(\sigma :\psi \) as premise and (r) as the rule that was applied to create the nodes. Note that rules (K) and (4) can only be applied to a formula \(\sigma :\Box \varphi \) if a prefix \(\sigma .n\), introduced by an application of rule \((\pi )\), is already present in a branch. Analogously, for rule \(4^{D}\). By a systematic tableau construction, we mean an application of the procedure in [11, p. 374] adapted to SST rules.

A prefixed formula \(\sigma :\varphi \) is in a branch \(\mathscr {B}\), denoted by \(\sigma :\varphi \in \mathscr {B}\), if there is a node in \(\mathscr {B}\) labeled with \(\sigma :\varphi \). A prefix is present in a branch \(\mathscr {B}\) if there is a prefixed formula in \(\mathscr {B}\) with that prefix, and it is new if it is not present. A branch \(\mathscr {B}\) is closed if there is a prefix \(\sigma \) such that either (i) \(\sigma :\mathbf{false}\) is present in \(\mathscr {B}\) or (ii) for some propositional symbol p, both \(\sigma : p\) and \(\sigma : \lnot p\) are present in \(\mathscr {B}\). A tableau is closed if every branch is closed. A prefixed formula \(\sigma : \varphi \) is reduced for rule (r) in \(\mathscr {B}\), if (r) has the form \(\sigma : \varphi / \sigma ' : \varphi '\) and \(\sigma ' : \varphi '\) is in \(\mathscr {B}\); if (r) has the form \(\sigma : \varphi / \sigma _1 : \varphi _1 | \sigma _2 : \varphi _2\) and at least one of \(\sigma _1 : \varphi _1\) and \(\sigma _2 : \varphi _2\) is in \(\mathscr {B}\).

By \({\mathscr {B}|^\mathsf{p}_{\sigma }}\), \({\mathscr {B}|^\mathsf{m}_{\sigma }}\), and \({\mathscr {B}|^\mathsf{a}_{\sigma }}\), we denote the sets \(\{l|l\in L_{P},\sigma :l\in \mathscr {B}\}\), \(\{\Diamond l|l\in L_{P},\sigma :\Diamond l\in \mathscr {B}\}\cup \{\Box l|l\in L_{P},\sigma :\Box l\in \mathscr {B}\}\), and \({\mathscr {B}|^\mathsf{p}_{\sigma }}\cup {\mathscr {B}|^\mathsf{m}_{\sigma }}\), respectively.

For a modal formula \(\varphi \) in simplified NNF let \(d^\varphi _\Diamond \) be the maximal nesting of \(\Diamond \)-operators not under the scope of any \(\Box \) operators in \(\varphi \), \(n^\varphi _\Box \) be the number of \(\Box \)-subformulae in \(\varphi \), and \(n^\varphi _\Diamond \) be the number of \(\Diamond \)-subformulae below \(\Box \)-operators in \(\varphi \).

Theorem 11 allows rule (\(\pi \)) to be applied to a prefix \(\sigma \) of length \(1 + d^\varphi _\Diamond + n^\varphi _\Diamond \times n^\varphi _\Box \), creating a prefix of length \(2 + d^\varphi _\Diamond + n^\varphi _\Diamond \times n^\varphi _\Box \). No prefix of greater length can occur in a tableau.

For \({\textsf {K5} }\), Massacci did not provide a bound on the length of prefixes in his SST calculus that preserves refutational completeness. However, using the techniques that he applied to prove such a bound for \({\textsf {K4} }\), Theorem 12 establishes a bound for \({\textsf {K5} }\).

In order to establish a relationship between closed tableaux and resolution refutations of a set of \(\textsf {SNF}_{ml}\) clauses, we formally define the modal-layered resolution calculus. Table 5 shows the inference rules of the calculus restricted to labels occurring in the clauses produced by our reductions. 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 the modal level, \(ml+1\).

Let \(\varPhi \) be a set of \(\textsf {SNF}_{ml}\) clauses. A (resolution) derivation from \(\varPhi \) is a sequence of sets \(\varPhi _0,\varPhi _1,\ldots \) where \(\varPhi _0 = \varPhi \) and, for each \(i>0\), \(\varPhi _{i+1} = \varPhi _i \cup \{D\}\), where \(D \not \in \varPhi _i\) is the resolvent obtained from \(\varPhi _i\) by an application of one the inference rules to premises in \(\varPhi _i\). A (resolution) refutation of \(\varPhi \) is a derivation \(\varPhi _0,\ldots ,\varPhi _k\), \(k \in {\mathbb N}\), where \(0:\mathbf{false}\in \varPhi _k\).

To map a set of \(\textsf {SNF}_{sml}\) clauses to a set of \(\textsf {SNF}_{ml}\) clauses, using a bound \(n\in {\mathbb N}\) on the modal levels, we define a function \(\mathrm {db}_{n}\) on clauses and sets of clauses in \(\textsf {SNF}_{sml}\) as follows:Note that prefixes in SST-tableaux have a minimal length of 1 while the minimal modal level in \(\textsf {SNF}_{ml}\) clauses is 0. So, a prefix of length n in a prefixed formula corresponds to a modal level \(n-1\) in an \(\textsf {SNF}_{ml}\) clause.

In analogy, we can also prove a corresponding result for \({\textsf {K5} }\) with the bound established in Theorem 12.

The approaches most closely related to ours are Kracht’s reductions of normal modal logics to basic modal logic [16, 17], the global modal resolution calculus [20], and Schmidt and Hustadt’s axiomatic translation principle for translations of normal modal logics to first-order logic [31].

The first significant difference to our approach is that Kracht’s reductions and the axiomatic translation exclude the modal operator \(\Diamond \) from the language and only consider the modal operator \(\Box \). In order to present Kracht’s approach, we need some additional notions. Let \(\mathsf {sf}(\varphi ), \mathsf {dg}(\varphi )\), and |S| denote the set of all subformulae of \(\varphi \), the maximum nesting of modal operators in \(\varphi \), and the cardinality of the set S, respectively. Let \(\Diamond ^0\psi =\Box ^0\psi =\Box ^{<1}\psi = \psi \), \(\Box ^{<n+1}\psi = (\psi \wedge \Box \!\Box ^{<n}\!\psi )\), \(\Box ^{n+1}\psi =\Box \!\Box ^n\!\psi \), and \(\Diamond ^{n+1}\psi =\Diamond \!\!\Diamond ^n\!\psi \). We can then define a reduction function \(\rho ^\textsf {K} _L\) for a normal modal logic L in \(\{{\textsf {KB} },{\textsf {KD} },{\textsf {KT} },{\textsf {K4} }\}\) as follows:\({\begin{array}{llll} \mathrm{where} \,P^\textsf {K} _{{\textsf {\textit{KB}}}}(\varphi ) &{}= \{\lnot \psi \rightarrow \Box \lnot \!\Box \!\psi \mid \Box \!\psi \in \mathsf {sf}(\varphi )\} &{} P^\textsf {K} _{{\textsf {\textit{KD}}}}(\varphi ) &{}= \{\lnot \Box \mathbf{false}\}\\ \qquad \quad \,\,P^\textsf {K} _{{\textsf {\textit{K4}}}}(\varphi ) &{}= \{\Box \psi \rightarrow \Box \!\Box \!\psi \mid \Box \psi \in \mathsf {sf}(\varphi )\} &{} P^\textsf {K} _{{\textsf {\textit{KT}}}}(\varphi ) &{}= \{\Box \psi \rightarrow \psi \mid \Box \psi \in \mathsf {sf}(\varphi )\} \end{array}}\)

Kracht shows that \(\varphi \) is L-satisfiable iff \(\rho ^\textsf {K} _L(\varphi )\) is \(\textsf {K} {}{}\)-satisfiable. There are three differences to our approach. First, \(P^\textsf {K} _L(\varphi )\) will include an axiom instance for every occurrence of a subformula \(\lnot \Box \psi \), equivalent to \(\Diamond \lnot \psi \), in \(\varphi \). In contrast, our approach requires no logic specific treatment of such subformulae. Second, the use of \(\Box ^{<n} P^\textsf {K} _L(\varphi )\) in \(\rho ^\textsf {K} _L\) means that the axiom instance is available at every modal level. This means, for example, that for \(\vartheta _1 = \Diamond ^{100}(\lnot p\wedge \Box p)\), the formula \({\rho ^\textsf {K} _{{\textsf {\textit{KT}}}}(\vartheta _1)}\) contains the axiom instance \(\Box p\rightarrow p\) over 100 times, although it is only required at the level at which \(\Box p\) occurs. Third, this is further compounded if the formula \(\psi \) in \(\Box \psi \) is itself a complex formula. We try to avoid that by using a surrogate propositional symbol \(t_\psi \) instead, but this will only have a positive effect if the definitional clauses for \(t_\psi \) do not have to be repeated.

The global modal resolution (GMR) calculus operates on \(\mathsf {SNF}_K\) clauses, that is, clauses of the formwhere l, \(l'\), \(l_b\) are propositional literals with \(1 \le b \le r\), \(r \in {\mathbb N}\), and \(\Box ^*\) is the universal operator. The calculus has specific inference rules for normal modal logics such as \({\textsf {KB} }\), \({\textsf {KD} }\), \({\textsf {KT} }\), \({\textsf {K4} }\), \({\textsf {K5} }\). Table 6 shows the two additional rules for \({\textsf {K5} }\), the only logic for which there are rules for both \(\Box \) and \(\lnot \!\Box \!\lnot \), i.e., \(\Diamond \). These inference rules can be seen to perform an ‘on-the-fly’ computation of a reduction. Note that the clauses produced by \({P_{{\textsf {\textit{K5}}}}}\) differ from those produced by GMR for \({\textsf {K5} }\). Implicitly, our results here also show that it should be possible to eliminate EUC1 from the GMR calculus.

For the axiomatic translation, we only present the function \(P^\textsf {R}S _L\) that computes the logic dependent first-order clausal formulae that are part of the overall translation.Here the variables x and y range over worlds. The predicate symbols \(Q_\psi \) correspond to our surrogate symbols \(t_\psi \). The clausal formulae used in the treatment of \({\textsf {KT} }\) and \({\textsf {K4} }\) are translations of the \(\textsf {SNF}_{ml}\) clauses we use (or vice versa). \({\textsf {KB} }\) and \({\textsf {K5} }\) are handled in a different way as the first-order clausal formulae refer directly the accessibility relation and can therefore more easily express the transfer of information to a predecessor world. The universal quantification over worlds also means that the constraints expressed by the formulae hold at all modal levels without the need of any repetition.

In Sect. 8, we will also use the relational and semi-functional translation of modal logics to first-order logic combined with structural transformation to clause normal form. In both approaches \(\Box \psi \) is translated as \(\forall x y (\lnot Q_{\Box \psi }(x)\vee \lnot R(x,y)\vee Q_\psi (y))\), while \(\Diamond \psi \) becomes \(\forall x\exists y (\lnot Q_{\Diamond \psi }(x)\vee (R(x,y) \wedge Q_\psi (y)))\) and \(\forall x\exists \alpha (\lnot Q_{\Diamond \psi }(x)\vee (\mathrm {def}(x)\wedge Q_\psi ([x\alpha ])))\) in the relational and semi-functional translation, respectively. Here, the variables x and y also range over worlds while \(\alpha \) and \(\beta \) range over partial accessibility functions.

Then, depending on the modal logics, further formulae representing the semantic properties of the accessibility R are added. For the relational translation these will simply be the formulae in the fourth column of Table 1. The semi-functional translation uses collections of partial accessibility function in addition to the accessibility relation. A predicate \(\mathrm {def}\) is used to represent on which worlds a partial accessibility function is defined. For each modal logic there is then again a background theory consisting of formulae over \(\mathrm {def}\) and R that represents the properties of the underlying accessibility relation which is added to the translation of a formula. For example, for \({\textsf {K5} }\) the background theory is: \( \forall x y\forall \alpha \beta ((\lnot \mathrm {def}(x)\vee \mathrm {def}(y))\wedge (\lnot \mathrm {def}(\mathrm {w_0})\vee R(\mathrm {w_0},[\mathrm {w_0}\alpha ]))\wedge (\lnot \mathrm {def}(x)\vee \lnot \mathrm {def}(y)\vee R([x\alpha ],[y\beta ]))), \) where \(\mathrm {w_0}\) is a constant representing the root world in a rooted Kripke structure.

In [35], Sebastiani and Venscovi present an encoding of \({\textsf {K} }\) into propositional logic. In this encoding, each propositional symbol produced by their reduction corresponds to labeled formulae in each possible world following closely the application of the tableau rules for \({\textsf {K} }\) given in [18]. As noted by the authors, such encoding leads to an exponential blow-up in the size of a formula in the worst case (if P \(\ne \) NP). In practice, however, their implemented tool \(K_m2SAT\), combined with state of the art SAT solvers, performed well in most of the usual benchmarks. The InkreSAT prover [15] provides decision procedures for \({\textsf {K} }\), \({\textsf {KT} }\), \({\textsf {K4} }\) and \({\textsf {S4} }\), that is, a subset of the logics considered here. Their approach also reduces the satisfiability problem for a particular logic into the satisfiability problem for propositional logic. Differently from [35], the translation is interleaved with calls to the underlying SAT prover; the result from the SAT prover is then incrementally used to guide the translation. This helps with earlier simplification and better performance when compared with \(K_m2SAT\). In the worst case, however, as with [35], the translation is exponential in the size of the input formula. In [24], we have compared InKreSAT and \({\text {K}_{\text {S}}}{\text {P}}\), \(K_m2SAT\) does not appear to be publicly available anymore. The evaluation indicates InKreSAT has the second best performance when all the benchmarks were considered, but less impressive results on the LWB benchmark with the fifth best performance among the six competing tools.

For our evaluation, we have restricted ourselves to fully automatic provers with built-in support for all the six logics we have considered. By ‘built-in support,’ we mean the possibility to specify the logic either via command-line option or via a configuration option within an input file together with modal formula.

We have compared the performance of the following approaches: (i) the combination of our reductions with the modal-layered resolution (MLR) calculus for \(\textsf {SNF}_{ml}\) clauses [21], R+MLR calculus for short, implemented in the modal theorem prover \({\text {K}_{\text {S}}}{\text {P}}\), with three different refinements for resolution inferences on labeled propositional clauses; (ii) the global modal resolution (GMR) calculus, also implemented in \({\text {K}_{\text {S}}}{\text {P}}\), with three different refinements for resolution inferences on propositional clauses; (iii) the combinations of the relational and semi-functional translation of modal logics to first-order logic with ordered first-order resolution implemented in the first-order theorem prover SPASS; (iv) the higher-order logic prover LEO-III with \({\textbf {E}} \) 2.6 as external reasoner.

In total this gives us nine different approaches to compare. The axiomatic translation is currently not implemented in SPASS. Other provers, such as LWB [13] and MleanCoP [27], do not have built-in support for the full range of logics considered here. LoTREC 2.0 [8] supports all the logics, but is not intended as automatic theorem prover.

\({\text {K}_{\text {S}}}{\text {P}}\) [19] implements the reductions presented in Sect. 3, the transformation from \(\textsf {SNF}_{sml}\) to \(\textsf {SNF}_{ml}\) presented in Sect. 6, as well as a normal form transformation of modal formulae to sets of \(\mathsf {SNF}_K\) clauses, required for the GMR calculus. It implements both the R+MLR and the GMR calculus. Resolution inferences between (labeled) propositional clauses can either be unrestricted (cplain option), restricted by an ordering (cord option), that is, clauses can only be resolved on their maximal literals with respect to an ordering chosen by the prover in such a way to preserve completeness, restricted to negative resolution (cneg option), that is, one of the premises in an inference has to be a negative clause, or restricted to positive resolution. We do not include the last option in our evaluation as it typically performs worse. \({\text {K}_{\text {S}}}{\text {P}}\) also implements a range of simplification rules that are applied to modal formulae before their transformation to normal form. Of those, we have enabled pure literal elimination (early_ple option), simplification using the Box Normal Form [28] and Prenex Normal Form (bnfsimp and prenex options) [22]. For clause processing, unit resolution and pure elimination are enabled (unit, lhs_unit, and ple options).

SPASS 3.9 [38, 39] supports automated reasoning in extended modal logics, including all logics considered here, PDL-like modal logics as well as description logics. It includes eight different translations of modal logics to first-order logic. In our evaluation, we have used the relational translation and the semi-functional translation. For the local satisfiability problem in \({\textsf {KB} }\) to \({\textsf {K5} }\), for the relational translation, SPASS adds the first-order frame properties given in Table 1 while for the semi-functional translation, it adds the background theories devised by Nonnengart [26]. For the transformation to first-order clausal form, we have enabled renaming of quantified subformulae. The only inference rules used are ordered resolution and ordered factoring, the reduction rules used are condensing, backward subsumption, and forward subsumption. For the relational and semi-functional translation for \({\textsf {K} }\), \({\textsf {KB} }\), \({\textsf {KD} }\), and \({\textsf {KT} }\) we thereby obtain a decision procedure, while for the other logics we do not. For \({\textsf {K4} }\) and \({\textsf {K5} }\), the fragment of first-order clausal logic corresponding to the semi-functional translation of modal formula and their background theories is decidable by ordered resolution with selection [32]. However, the non-trivial ordering and selection function required is not currently implemented in SPASS.

LEO-III [9, 36] makes use of a semantic embedding approach [10] to automatically transform modal formulae into corresponding HOL formulae. This embedding is most closely related to the relational translation in that it employs a representation of the worlds and accessibility relationship in Kripke frames and deals with modal logics other than the basic modal logic \({\textsf {K} }\) by adding the corresponding frame properties. LEO-III implements extensional paramodulation for higher-order logic [37] but can also collaborate with external reasoners during proof search. In our evaluation, we have exclusively used \({\textbf {E}} \) 2.6 [33, 34] as external reasoner.

For our evaluation, we have chosen the LWB basic modal logic benchmark collection [2], with 20 formulae in each of 18 parameterized classes. For \({\textsf {K} }\), all formulae in 9 classes are satisfiable while all formulae in the other 9 classes are unsatisfiable. In simplified NNF, 63% of modal operators are \(\Box \) and 37% are \(\Diamond \) operators. We have used the collection for each of the six logics. If a formula is unsatisfiable in \({\textsf {K} }\) then it remains unsatisfiable in the other five logics, while the opposite is not true. As we move to logics other than \({\textsf {K} }\), it is also no longer the case that all formulae in a class have the same satisfiability status.

Table 7 shows the results of our evaluation. The first column lists the six logics. We then separate the 360 LWB benchmark formulae into satisfiable (S) and unsatisfiable (U) formulae with respect to each logic. This gives us 12 categories. The third column then indicates the number of formulae in each. The last nine columns in the table show how many formulae within a category each of the approaches was able to solve with a time limit of 100 CPU seconds for each formula. In the last two lines of the table, we sum up the results for all logics. Benchmarking was performed on a PC with an AMD Ryzen 5 5600X CPU @ 4.60GHz max and 32GB main memory using Fedora release 34 as operating system. As we can see, the two best performing approaches are the GMR calculus with the ordered resolution refinement (cord) and the R+MLR calculus with the ordered resolution refinement, with the former performing slightly better. Each approach achieves the highest number of solved formulae in 3 categories and they are joint best on a further two categories. The GMR calculus is better on satisfiable formulae in almost all logics as it avoids the duplication of clauses introduced by the transformation from \(\textsf {SNF}_{sml}\) to \(\textsf {SNF}_{ml}\) required for the R+MLR calculus. On the other hand, the R+MLR calculus is better on most categories of unsatisfiable formulae. For SPASS, overall, we see a clear advantage of the semi-functional translation over the relational one, on both satisfiable and unsatisfiable formulae. LEO-III performs reasonably well on unsatisfiable formulae but cannot solve any of the satisfiable formulae. It is interesting to see that it performs better than SPASS with the relational translation on unsatisfiable \({\textsf {K4} }\) and \({\textsf {K5} }\) formulae. We put this down to the use of \({\textbf {E}} \) as external prover. Out of 717 formulae solved by LEO-III, \({\textbf {E}} \) provides the proof for 573 of those, including 267 out of 318 unsatisfiable \({\textsf {K4} }\) and \({\textsf {K5} }\) formulae solved. This shows that \({\textbf {E}} \) solves considerably more of those formulae than SPASS with 159 formulae.

It is worth pointing out that the results for \({\text {K}_{\text {S}}}{\text {P}}\) in Table 7 differ from those in [29]. First, improvements have been made to the implementation of the GMR calculus meaning it solves more formulae now. Second, in [29], we have used bounds for the reduction from \(\textsf {SNF}_{sml}\) to \(\textsf {SNF}_{ml}\) for \({\textsf {K4} }\) and \({\textsf {K5} }\) that were sufficient for the LWB benchmark formulae, but lower than the worst case bounds we established in Sect. 6. Here, we use the latter which results in fewer formulae being solved by the R+MLR calculus.

We have presented new reductions of propositional modal logics \({\textsf {KB} }\), \({\textsf {KD} }\), \({\textsf {KT} }\), \({\textsf {K4} }\), \({\textsf {K5} }\) to Separated Normal Form with Sets of Modal Levels. We have shown experimentally that these reductions allow us to reason effectively in these logics.

The obvious next step is to consider extensions of the basic modal logic \({\textsf {K} }\) with combinations of the axioms \(\textsf {B} \), \(\textsf {D} \), \(\textsf {T} \), \(\textsf {4} \), and \(\textsf {5} \). Unfortunately, a simple combination of the reductions for each of the axioms is not sufficient to obtain a satisfiability-preserving reduction for the such modal logics. An example is the simple formula \(\lnot p\wedge \Diamond \!\Diamond \!\Box p\) which is \({\textsf {KB4} }\)-unsatisfiable. If we definethat is, \({P_{{\textsf {\textit{KB4}}}}}\) is the union of \({P_{{\textsf {\textit{KB}}}}}\) and \({P_{{\textsf {\textit{K4}}}}}\), then the clause set obtained from \(\{\{0\}: t_0\}\cup \rho _{{\textsf {\textit{KB4}}}}(\{0\}: t_0\rightarrow \lnot p\wedge \Diamond \!\Diamond \Box p)\) is \({\textsf {K} }\)-satisfiable. The same issue also occurs in the axiomatic translation of modal logics to first-order logic where the translation for \({\textsf {KB4} }\) is not simply the combination of the translations for \({\textsf {KB} }\) and \({\textsf {K4} }\) [31, Theorem 5.6]. We are currently exploring solutions to this problem.

Regarding practical applications, it would be advantageous to have an implementation of a calculus that operates directly \(\textsf {SNF}_{sml}\) clauses. This would greatly reduce the number of inference steps performed on satisfiable formulae and simplify proof search in general. Again, such an implementation is future work.