# Resolution Calculi for Non-normal Modal Logics

Dirk Pattinson, Cláudia Nalon, Nicola Olivetti

► To cite this version:

Dirk Pattinson, Cláudia Nalon, Nicola Olivetti. Resolution Calculi for Non-normal Modal Logics: A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus. Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Sep 2023, Prague (Czech Republic), Czech Republic. pp.322-341, 10.1007/978-3-031-43513-3_18 . hal-04457384

HAL Id: hal-04457384

https://amu.hal.science/hal-04457384

Submitted on 15 Apr 2024

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Resolution Calculi for Non-normal Modal Logics

Dirk Pattinson, Cláudia Nalon, Nicola Olivetti

► To cite this version:

Dirk Pattinson, Cláudia Nalon, Nicola Olivetti. Resolution Calculi for Non-normal Modal Logics. Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Sep 2023, Prague (Czech Republic), Czech Republic. pp.322-341, 10.1007/978-3-031-43513-3_18. hal-04457384

HAL Id: hal-04457384

https://amu.hal.science/hal-04457384v1

Submitted on 15 Apr 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Resolution Calculi for Non-normal Modal Logics

Dirk Pattinson¹(✉)[0000-0002-5832-6666], Nicola Olivetti²[0000-0001-6254-3754], and Cláudia Nalon³[0000-0002-9792-5346]★

1 School of Computing, The Australian National University, Canberra, Australia,
dirk.pattinson@anu.edu.au

2 Aix Marseille University, CNRS, LIS, Marseille, France,
nicola.olivetti@lis-lab.fr

3 Department of Computer Science, University of Brasília, Brasília, Brazil,
nalon@unb.br

**Abstract.** We present resolution calculi for the cube of classical non-normal modal logics. The calculi are based on a simple clausal form that comprises both local and global clauses. Any formula can be efficiently transformed into a small set of clauses. The calculi contain uniform rules and provide a decision procedure for all logics. Their completeness is based on a new and crucial notion of inconsistency predicate, needed to ensure the usual closure properties of maximal consistent sets. As far as we know the calculi presented here are the first resolution calculi for this class of logics.

**Keywords:** Modal Logic · Automated Reasoning · Resolution.

## 1 Introduction

Non-normal modal logics (NNMLs) have been studied since the seminal work by Kripke in the 1960s, and then developed prominently by Montague, Segeberg, Scott, and Chellas in the 1970s. They are called *non-normal* as they do not satisfy all axioms of minimal normal modal logic **K**. NNMLs are used in a variety of contexts. In epistemic reasoning they offer a simple (preliminary) solution to the problem of logical omniscience. In deontic logic, they allow to avoid some well-known paradoxes of classical deontic logic, and enable us to represent conflicting obligations. Multi-agent non-normal modalities have been used to capture notions of agency and ability, where □*φ* is read as “the agent can bring about *φ*”, for a formula *φ* [12]. Moreover, the non-normal monotonic logic **EM** coincides with the 2-agent case of Pauly’s coalition logic with determinacy. Finally NNMLs are the formalism of choice to express normality and typicality, or truth in most of the cases, as a modality [43].

In this paper we consider the classical cube of NNMLs. It comprises the minimal modal logic **E**, the smallest modal logic closed under congruence (only), and extensions of **E** with one or more of the axioms C, M and N. This results in a cube of 8 systems, where the stronger one (defined by all three axioms M, N, and

<footnote>★ C. Nalon was partially supported by FAPDF 11/2021, DPG/UnB 004/2022.</footnote>
# Resolution Calculi for Non-normal Modal Logics

Dirk Pattinson¹(✉)[0000-0002-5832-6666], Nicola Olivetti²[0000-0001-6254-3754], and Cláudia Nalon³[0000-0002-9792-5346]★

¹ School of Computing, The Australian National University, Canberra, Australia,
dirk.pattinson@anu.edu.au

² Aix Marseille University, CNRS, LIS, Marseille, France,
nicola.olivetti@lis-lab.fr

³ Department of Computer Science, University of Brasília, Brasília, Brazil,
nalon@unb.br

**Abstract.** We present resolution calculi for the cube of classical non-normal modal logics. The calculi are based on a simple clausal form that comprises both local and global clauses. Any formula can be efficiently transformed into a small set of clauses. The calculi contain uniform rules and provide a decision procedure for all logics. Their completeness is based on a new and crucial notion of inconsistency predicate, needed to ensure the usual closure properties of maximal consistent sets. As far as we know the calculi presented here are the first resolution calculi for this class of logics.

**Keywords:** Modal Logic · Automated Reasoning · Resolution.

## 1 Introduction

Non-normal modal logics (NNMLs) have been studied since the seminal work by Kripke in the 1960s, and then developed prominently by Montague, Segeberg, Scott, and Chellas in the 1970s. They are called *non-normal* as they do not satisfy all axioms of minimal normal modal logic **K**. NNMLs are used in a variety of contexts. In epistemic reasoning they offer a simple (preliminary) solution to the problem of logical omniscience. In deontic logic, they allow to avoid some well-known paradoxes of classical deontic logic, and enable us to represent conflicting obligations. Multi-agent non-normal modalities have been used to capture notions of agency and ability, where □*φ* is read as “the agent can bring about *φ*”, for a formula *φ* [12]. Moreover, the non-normal monotonic logic **EM** coincides with the 2-agent case of Pauly’s coalition logic with determinacy. Finally NNMLs are the formalism of choice to express normality and typicality, or truth in most of the cases, as a modality [43].

In this paper we consider the classical cube of NNMLs. It comprises the minimal modal logic **E**, the smallest modal logic closed under congruence (only), and extensions of **E** with one or more of the axioms C, M and N. This results in a cube of 8 systems, where the stronger one (defined by all three axioms M, N, and

<footnote>★ C. Nalon was partially supported by FAPDF 11/2021, DPG/UnB 004/2022.</footnote>
C) is just the normal modal logic K. NNMLs have a well-understood semantics defined in terms of neighbourhood models [7]. In these models, each world w is associated with a set of neighbourhoods N(w), where each neighbourhood is a set of worlds itself. If we accept the traditional interpretation of a proposition as the set of worlds in which it holds (its truth set), we can think of N(w) as a set of propositions associated with w, i.e. precisely those propositions that are necessary, known, obligatory, ... at the world w. The classical cube arises by imposing closure properties on the set of neighbourhoods (or propositions) associated with a world, and captured syntactically by the axioms.

From an automated reasoning and proof theoretic view, NNMLs are not as well studied as normal modal logics. Cut-free Gentzen calculi for NNML have been studied in [25,22,23,41,42]. Labelled calculi of different kinds have been proposed in [15,37,10], where the neighbourhood semantics is represented syntactically through two different labels, for worlds and neighbourhoods. Situated between these two approaches, there are calculi that augment sequents with additional structure, but without fully representing the neighbourhood semantics: linear nested sequents with an additional nesting operator [26] and structured hypersequents [9]. All these calculi have different purposes and properties. Cut-free Gentzen calculi typically provide a straightforward decision procedure, in some cases of optimal complexity, and help to prove interpolation [42]. Labelled calculi, and also the approach taken in [9], allow us to extract countermodels of unprovable sequents. The structured calculi of [26] provide a uniform and modular formulation of NNML when extended with axioms of the standard modal cube. An algorithmic alternative to deduction has been proposed in [16], where the satisfiability problem in NNML is reduced to a set of SAT problems. This essentially implements the proof of the complexity bound for these logics given by Vardi [52].

This paper presents a different approach to reasoning in NNMLs and introduces resolution calculi for all logics in the NNML cube. Resolution methods usually rely on normal forms, which not only helps in the design of the inference rules, but also allow for simple implementations. Moreover, although the complexity of the method is high – proofs might be exponential in the size of the input for some problems [21] – resolution for classical logics is widely implemented [27,28,49,11,17,47,50] with excellent performance in practice [48]. Resolution calculi have been designed for several modal logics, including the normal modal logic K and its extensions in the modal cube, either as direct method or using translations into more expressive logics, e.g. as in [5,4,1,6,3,13,14,29,8,2,30,36,31] and [39,40,38]. Recent evaluations [32,33,31,34,18,44,35] show that resolution-based provers for K also perform well when compared with tableaux, SAT, and translation based procedures for modal logics [51,20,24,19,18,49,11,17,47,50].

To the best of our knowledge, ours are the first resolution calculi for NNMLs. We use a very simple, congruential translation of formulae into sets of local and global clauses, where the latter are required to hold at any point in the model. Completeness is established via canonical models, and the main conceptual novelty is the analysis of maximally consistent sets using *inconsistency predicates*.
C) is just the normal modal logic K. NNMLs have a well-understood semantics defined in terms of neighbourhood models [7]. In these models, each world w is associated with a set of neighbourhoods N(w), where each neighbourhood is a set of worlds itself. If we accept the traditional interpretation of a proposition as the set of worlds in which it holds (its truth set), we can think of N(w) as a set of propositions associated with w, i.e. precisely those propositions that are necessary, known, obligatory, ... at the world w. The classical cube arises by imposing closure properties on the set of neighbourhoods (or propositions) associated with a world, and captured syntactically by the axioms.

From an automated reasoning and proof theoretic view, NNMLs are not as well studied as normal modal logics. Cut-free Gentzen calculi for NNML have been studied in [25,22,23,41,42]. Labelled calculi of different kinds have been proposed in [15,37,10], where the neighbourhood semantics is represented syntactically through two different labels, for worlds and neighbourhoods. Situated between these two approaches, there are calculi that augment sequents with additional structure, but without fully representing the neighbourhood semantics: linear nested sequents with an additional nesting operator [26] and structured hypersequents [9]. All these calculi have different purposes and properties. Cut-free Gentzen calculi typically provide a straightforward decision procedure, in some cases of optimal complexity, and help to prove interpolation [42]. Labelled calculi, and also the approach taken in [9], allow us to extract countermodels of unprovable sequents. The structured calculi of [26] provide a uniform and modular formulation of NNML when extended with axioms of the standard modal cube. An algorithmic alternative to deduction has been proposed in [16], where the satisfiability problem in NNML is reduced to a set of SAT problems. This essentially implements the proof of the complexity bound for these logics given by Vardi [52].

This paper presents a different approach to reasoning in NNMLs and introduces resolution calculi for all logics in the NNML cube. Resolution methods usually rely on normal forms, which not only helps in the design of the inference rules, but also allow for simple implementations. Moreover, although the complexity of the method is high – proofs might be exponential in the size of the input for some problems [21] – resolution for classical logics is widely implemented [27,28,49,11,17,47,50] with excellent performance in practice [48]. Resolution calculi have been designed for several modal logics, including the normal modal logic K and its extensions in the modal cube, either as direct method or using translations into more expressive logics, e.g. as in [5,4,1,6,3,13,14,29,8,2,30,36,31] and [39,40,38]. Recent evaluations [32,33,31,34,18,44,35] show that resolution-based provers for K also perform well when compared with tableaux, SAT, and translation based procedures for modal logics [51,20,24,19,18,49,11,17,47,50].

To the best of our knowledge, ours are the first resolution calculi for NNMLs. We use a very simple, congruential translation of formulae into sets of local and global clauses, where the latter are required to hold at any point in the model. Completeness is established via canonical models, and the main conceptual novelty is the analysis of maximally consistent sets using *inconsistency predicates*.
As we demonstrate by example, our modal resolution calculus does not derive the modal literal $\neg l$ from a set $\mathcal{C}$ of clauses if $\mathcal{C} \cup \{l\}$ is inconsistent. Rather, it derives a (set of) literals $e$ such that $\{e, l\}$ are inconsistent over $\mathcal{C}$. This allows us to show that maximally consistent sets are negation complete and disjunction complete. Also, inconsistency predicates allow us to lift statements of global satisfiability of clauses to resolution derivability, which in turn establishes premisses of resolution rules that we need to establish completeness.

The paper is structured as follows. In the next section we present the language of NNMLs and their axiomatisations. We then present the calculi for each modal logic in the NNML cube in Section 3, together with results for termination and soundness. Completeness is shown in Section 4. The completeness results show that proof systems for stronger logics are obtained modularly by adding rules to the weaker systems. We conclude in Section 5.

## 2 Syntax, Semantics, and Axiomatisation

**Definition 1.** We fix a countable set $\mathcal{V}$ of propositional variables. The language $\mathcal{L}$ of the basic unimodal logic is given by the grammar $\mathcal{L} \ni \phi, \psi := p \mid \neg\phi \mid \Box\phi \mid \phi \lor \psi$ where $p \in \mathcal{V}$.

Other connectives $\top, \bot, \wedge, \rightarrow$ and $\diamond$ are defined in the standard way, and we use the usual operator precedence $\wedge, \vee, \rightarrow, \leftrightarrow$ from strongest to weakest. We denote the set of subformulae of $\phi \in \mathcal{L}$ and their negations by $\mathbf{subf}(\phi)$, where leading double negations are eliminated.

**Terminology 2.** Variables and their negations are called propositional literals, and modal literals are of the form $\Box p$ or $\neg\Box p$ where $p \in \mathcal{V}$ is a propositional variable. A literal is either a propositional or a modal literal. We write $\text{Lit}(\mathcal{V})$ for the set of literals with variables in $\mathcal{V}$.

Formulae are interpreted with respect to *neighbourhood models*.

**Definition 3.** A neighbourhood frame is a pair $(W, N)$ where $W$ is a set (of worlds) and $N: W \to \mathcal{P}(\mathcal{P}(W))$ is a (neighbourhood) function, where $\mathcal{P}(S)$ denotes the powerset of $S$. A neighbourhood model is a neighbourhood frame endowed with a valuation, that is, a triple $(W, N, \theta)$ where $(W, N)$ is a neighbourhood frame and $\theta: \mathcal{V} \to \mathcal{P}(W)$ is a (valuation) function.

**Definition 4.** Truth of a formula $\phi \in \mathcal{L}$ at a world $w \in W$ of a neighbourhood model $M = (W, N, \theta)$ is given inductively by:

$$ 
\begin{align*}
M, w \models p &\iff w \in \theta(p) \\
M, w \models \phi \lor \psi &\iff M, w \models \phi \text{ or } M, w \models \psi \\
M, w \models \neg\phi &\iff M, w \models \phi \\
M, w \models \Box\phi &\iff [\phi]_M \in N(w)
\end{align*}
$$

where $[\phi]_M = \{w \in W \mid M, w \models \phi\}$ is the truth set of $\phi$.
As we demonstrate by example, our modal resolution calculus does not derive the modal literal $\neg l$ from a set $\mathcal{C}$ of clauses if $\mathcal{C} \cup \{l\}$ is inconsistent. Rather, it derives a (set of) literals $e$ such that $\{e, l\}$ are inconsistent over $\mathcal{C}$. This allows us to show that maximally consistent sets are negation complete and disjunction complete. Also, inconsistency predicates allow us to lift statements of global satisfiability of clauses to resolution derivability, which in turn establishes premisses of resolution rules that we need to establish completeness.

The paper is structured as follows. In the next section we present the language of NNMLs and their axiomatisations. We then present the calculi for each modal logic in the NNML cube in Section 3, together with results for termination and soundness. Completeness is shown in Section 4. The completeness results show that proof systems for stronger logics are obtained modularly by adding rules to the weaker systems. We conclude in Section 5.

## 2 Syntax, Semantics, and Axiomatisation

**Definition 1.** We fix a countable set $\mathcal{V}$ of propositional variables. The language $\mathcal{L}$ of the basic unimodal logic is given by the grammar $\mathcal{L} \ni \phi, \psi := p \mid \neg\phi \mid \Box\phi \mid \phi \lor \psi$ where $p \in \mathcal{V}$.

Other connectives $\top, \bot, \wedge, \rightarrow$ and $\diamond$ are defined in the standard way, and we use the usual operator precedence $\wedge, \vee, \rightarrow, \leftrightarrow$ from strongest to weakest. We denote the set of subformulae of $\phi \in \mathcal{L}$ and their negations by $\mathbf{subf}(\phi)$, where leading double negations are eliminated.

**Terminology 2.** Variables and their negations are called propositional literals, and modal literals are of the form $\Box p$ or $\neg\Box p$ where $p \in \mathcal{V}$ is a propositional variable. A literal is either a propositional or a modal literal. We write $\text{Lit}(\mathcal{V})$ for the set of literals with variables in $\mathcal{V}$.

Formulae are interpreted with respect to *neighbourhood models*.

**Definition 3.** A neighbourhood frame is a pair $(W, N)$ where $W$ is a set (of worlds) and $N: W \to \mathcal{P}(\mathcal{P}(W))$ is a (neighbourhood) function, where $\mathcal{P}(S)$ denotes the powerset of $S$. A neighbourhood model is a neighbourhood frame endowed with a valuation, that is, a triple $(W, N, \theta)$ where $(W, N)$ is a neighbourhood frame and $\theta: \mathcal{V} \to \mathcal{P}(W)$ is a (valuation) function.

**Definition 4.** Truth of a formula $\phi \in \mathcal{L}$ at a world $w \in W$ of a neighbourhood model $M = (W, N, \theta)$ is given inductively by:

$$ 
\begin{align*}
M, w \models p &\iff w \in \theta(p) \\
M, w \models \phi \lor \psi &\iff M, w \models \phi \text{ or } M, w \models \psi \\
M, w \models \neg\phi &\iff M, w \models \phi \\
M, w \models \Box\phi &\iff [\phi]_M \in N(w)
\end{align*}
$$

where $[\phi]_M = \{w \in W \mid M, w \models \phi\}$ is the truth set of $\phi$.
<table><caption>**Table 1.** Axioms and frame properties, where $(W, N)$ is a frame, $\alpha, \beta \subseteq W$, $w \in W$.</caption><thead><tr><th>Axiom</th><th>Frame Property</th></tr></thead><tbody><tr><td>C: (□φ ∧ □ψ) → □(φ ∧ ψ)</td><td>Closed under intersection:<br>α ∈ N(w) ∧ β ∈ N(w) → α ∩ β ∈ N(w)</td></tr><tr><td>M: □(φ ∧ ψ) → □φ</td><td>Supplemented : α ∈ N(w) ∧ α ⊆ β → β ∈ N(w)</td></tr><tr><td>N: □⊤</td><td>Contains the unit: W ∈ N(w)</td></tr></tbody></table>

<figure><img src="image_2.png" /><figcaption>**Fig. 1.** The classical modal cube. Arrows indicate proper inclusion.</figcaption></figure>

A formula $\phi \in \mathcal{L}$ is satisfiable in a neighbourhood model $M = (W, N, \theta)$ if there is $w \in W$ such that $M, w \models \phi$. A set $\Gamma = \{\gamma_1, \dots, \gamma_n\}, n \in \mathbb{N}$, is satisfiable if and only if there is a neighbourhood model $(W, N, \theta)$ and a world $w \in W$ such that $M, w \models \gamma_i$, for all $1 \le i \le n$. A formula $\phi$ is satisfiable in a class $C$ of neighbourhood models if there exists $M \in C$ such that $\phi$ is satisfiable in $M$. We denote by $\mathcal{E}$ the class of all neighbourhood models.

The axiomatisation for the minimal logic $\mathbf{E}$ comprises the axiomatisation of classical propositional logic and the rule RE: from $\phi \leftrightarrow \psi$ derive $\Box\phi \leftrightarrow \Box\psi$. We also consider the extensions of $\mathbf{E}$ with the axioms given in Table 1. Neighbourhood models modularly characterise the classical cube of NNMLs given in Figure 1 in the sense that a formula $\phi$ is a theorem of $\mathbf{E}$ if and only if it is valid in the class $\mathcal{E}$ of all neighbourhood models [7]. Furthermore, $\phi$ is a theorem of $\mathbf{E}\Sigma$ with $\Sigma \subseteq \{C, M, N\}$ if and only if it is valid in the class of neighbourhood models that satisfy each of the additional axioms, whose corresponding frame conditions are given in Table 1. That is, the following holds [7, Theorem 7.5].

**Theorem 5.** The logic $\mathbf{E}$ (resp. $\mathbf{EC}, \mathbf{EM}, \mathbf{EN}, \mathbf{EMC}, \mathbf{ECN}, \mathbf{EMN}, \mathbf{EMCN}$) is characterised by the class $\mathcal{E}$ (resp. $\mathcal{EC}, \mathcal{EM}, \mathcal{EN}, \mathcal{EMC}, \mathcal{ECN}, \mathcal{EMN}, \mathcal{EMCN}$) of neighbourhood models.

We also note that axioms M and N are, respectively, equivalent to the rules RM ($\phi \rightarrow \psi$ / $\Box\phi \rightarrow \Box\psi$) and RN ($\phi / \Box\phi$), and that the axiom K ($\Box(\phi \rightarrow \psi) \rightarrow \Box\phi \rightarrow \Box\psi$) is derivable from M and C. As a consequence, the top system $\mathbf{EMCN}$ is equivalent to $\mathbf{K}$, the weakest normal modal logic [7, Theorem 8.9]. Monotonicity and aggregation correspond to *regularity*, that is, the system with both M and C is equivalent to the regular system $\mathbf{R}$ [7, Theorem 8.11].

We conclude this section by providing the well-known results about the complexity of the satisfiability problem for the logics here considered [52].
<table><caption>**Table 1.** Axioms and frame properties, where $(W, N)$ is a frame, $\alpha, \beta \subseteq W$, $w \in W$.</caption><thead><tr><th>Axiom</th><th>Frame Property</th></tr></thead><tbody><tr><td>C: (□φ ∧ □ψ) → □(φ ∧ ψ)</td><td>Closed under intersection:<br>α ∈ N(w) ∧ β ∈ N(w) → α ∩ β ∈ N(w)</td></tr><tr><td>M: □(φ ∧ ψ) → □φ</td><td>Supplemented : α ∈ N(w) ∧ α ⊆ β → β ∈ N(w)</td></tr><tr><td>N: □⊤</td><td>Contains the unit: W ∈ N(w)</td></tr></tbody></table>

<figure><img src="image_2.png" /><figcaption>**Fig. 1.** The classical modal cube. Arrows indicate proper inclusion.</figcaption></figure>

A formula $\phi \in \mathcal{L}$ is satisfiable in a neighbourhood model $M = (W, N, \theta)$ if there is $w \in W$ such that $M, w \models \phi$. A set $\Gamma = \{\gamma_1, \dots, \gamma_n\}, n \in \mathbb{N}$, is satisfiable if and only if there is a neighbourhood model $(W, N, \theta)$ and a world $w \in W$ such that $M, w \models \gamma_i$, for all $1 \le i \le n$. A formula $\phi$ is satisfiable in a class $C$ of neighbourhood models if there exists $M \in C$ such that $\phi$ is satisfiable in $M$. We denote by $\mathcal{E}$ the class of all neighbourhood models.

The axiomatisation for the minimal logic $\mathbf{E}$ comprises the axiomatisation of classical propositional logic and the rule RE: from $\phi \leftrightarrow \psi$ derive $\Box\phi \leftrightarrow \Box\psi$. We also consider the extensions of $\mathbf{E}$ with the axioms given in Table 1. Neighbourhood models modularly characterise the classical cube of NNMLs given in Figure 1 in the sense that a formula $\phi$ is a theorem of $\mathbf{E}$ if and only if it is valid in the class $\mathcal{E}$ of all neighbourhood models [7]. Furthermore, $\phi$ is a theorem of $\mathbf{E}\Sigma$ with $\Sigma \subseteq \{C, M, N\}$ if and only if it is valid in the class of neighbourhood models that satisfy each of the additional axioms, whose corresponding frame conditions are given in Table 1. That is, the following holds [7, Theorem 7.5].

**Theorem 5.** *The logic $\mathbf{E}$ (resp. $\mathbf{EC}, \mathbf{EM}, \mathbf{EN}, \mathbf{EMC}, \mathbf{ECN}, \mathbf{EMN}, \mathbf{EMCN}$) is characterised by the class $\mathcal{E}$ (resp. $\mathcal{EC}, \mathcal{EM}, \mathcal{EN}, \mathcal{EMC}, \mathcal{ECN}, \mathcal{EMN}, \mathcal{EMCN}$) of neighbourhood models.*

We also note that axioms M and N are, respectively, equivalent to the rules RM ($\phi \rightarrow \psi$ / $\Box\phi \rightarrow \Box\psi$) and RN ($\phi / \Box\phi$), and that the axiom K ($\Box(\phi \rightarrow \psi)$ / $\Box\phi \rightarrow \Box\psi$) is derivable from M and C. As a consequence, the top system $\mathbf{EMCN}$ is equivalent to $\mathbf{K}$, the weakest normal modal logic [7, Theorem 8.9]. Monotonicity and aggregation correspond to *regularity*, that is, the system with both M and C is equivalent to the regular system $\mathbf{R}$ [7, Theorem 8.11].

We conclude this section by providing the well-known results about the complexity of the satisfiability problem for the logics here considered [52].
**Theorem 6.** Let $\mathbf{E}\Sigma$ with $\Sigma \subseteq \{M, N\}$. The satisfiability problem for $\mathbf{E}\Sigma$ is in NP and the satisfiability problem for $\mathbf{EC}\Sigma$ is in PSPACE.

### 3 Resolution Calculi

Our resolution calculi operates over sets of formulae in a specific normal form: disjunctions of (propositional or modal) literals. Formulae can be transformed into this form by means of renaming [45] which creates new propositions together with their definitions in the resulting formula. The idea here is simple. To translate the formula $\Box\phi$, say, to clausal form, we stipulate $\Box\phi$ to be equivalent to $\Box p$, and additionally $p$ to be equivalent to $\phi$ – but the latter has to be true in every world of a neighbourhood model. Hence $\Box\phi$ is satisfiable if and only if the formulae $\Box p$ and $G(p \leftrightarrow \phi)$ are satisfiable. Here $G(\cdot)$ is a global modality that stipulates that a formula is true at every world in a model. For a neighbourhood model $(W, N, \theta)$, $w \in W$, and a formula $\phi \in \mathcal{L}$, we have that $M, w \models G(\phi) \iff M, w' \models \phi$, for all $w' \in W$, where $M, w \models \phi$ is as in Definition 4. Alternatively (and equivalently), $M, w \models G(\phi) \iff [\phi] = W$.

A clause is a formula in one of the following forms:

- local clauses: $\bigvee_i l_i$, where the $l_i$ are propositional or modal literals; or

- global clauses: $G(\bigvee_i l_i)$, where the $l_i$ are propositional or modal literals.

We often think of a clause as a set of literals and sometimes use set notation, that is, we identify $l_1 \lor \dots \lor l_n$ with the set $\{l_1, \dots, l_n\}$, for $n \in \mathbb{N}$. This allows us to also use set theoretic notation on clauses. For instance, for a literal $l$ and clause $\gamma$, we may write $l \in \gamma$ and say that $l$ is an element of $\gamma$. Similarly, $\gamma_1 \subseteq \gamma_2$ means that all literals of $\gamma_1$ are literals of $\gamma_2$.

It is easy to see that every formula can be represented as a set of clauses. As most logics in the cube are non-monotonic, we only replace the argument of $\Box$ with an equivalent formula. As a consequence, the rewriting steps and introduction of new variables by renaming consistently use bi-implications ($\leftrightarrow$). For a fixed formula $\phi \in \mathcal{L}$, we let $\eta = \eta_\phi : \text{subf}(\phi) \to \mathcal{V} \setminus \mathcal{V}(\phi)$ be an injective renaming function that associates a fresh propositional variable to every (possibly negated) subformula of $\phi$.

**Proposition 7.** A formula $\phi$ is satisfiable if, and only if, $\{\eta(\phi)\} \cup \mathbf{R}(G(\eta(\phi) \leftrightarrow \phi))$ is satisfiable, where $\mathbf{R}$ is defined as follows and $t, p \in \mathcal{V}$:

$$
\begin{align*}
\mathbf{R}(G(t \leftrightarrow p)) &= \{G(\neg t \lor p), G(t \lor \neg p)\} \\
\mathbf{R}(G(t \leftrightarrow \neg \psi)) &= \{G(\neg t \lor \neg \eta(\psi)), G(t \lor \eta(\psi))\} \cup \mathbf{R}(G(\eta(\psi) \leftrightarrow \psi)) \\
\mathbf{R}(G(t \leftrightarrow \psi \lor \psi')) &= \{G(\neg t \lor \eta(\psi) \lor \neg \eta(\psi')), G(t \lor \neg \eta(\psi)), G(t \lor \neg \eta(\psi'))\} \\
&\quad \cup \mathbf{R}(G(\eta(\psi) \leftrightarrow \psi)) \cup \mathbf{R}(G(\eta(\psi') \leftrightarrow \psi')) \\
\mathbf{R}(G(t \leftrightarrow \Box \psi)) &= \{G(\neg t \lor \Box \eta(\psi)), G(t \lor \neg \Box \eta(\psi))\} \cup \mathbf{R}(G(\eta(\psi) \leftrightarrow \psi))
\end{align*}
$$

Moreover, the size of $\{\eta(\phi)\} \cup \{\mathbf{R}(G(\eta(\phi) \leftrightarrow \phi))\}$ is linear on the size of $\phi$.
**Theorem 6.** Let $\mathbf{E}\Sigma$ with $\Sigma \subseteq \{M, N\}$. The satisfiability problem for $\mathbf{E}\Sigma$ is in NP and the satisfiability problem for $\mathbf{EC}\Sigma$ is in PSPACE.

## 3 Resolution Calculi

Our resolution calculi operates over sets of formulae in a specific normal form: disjunctions of (propositional or modal) literals. Formulae can be transformed into this form by means of renaming [45] which creates new propositions together with their definitions in the resulting formula. The idea here is simple. To translate the formula $\Box\phi$, say, to clausal form, we stipulate $\Box\phi$ to be equivalent to $\Box p$, and additionally $p$ to be equivalent to $\phi$ – but the latter has to be true in every world of a neighbourhood model. Hence $\Box\phi$ is satisfiable if and only if the formulae $\Box p$ and $G(p \leftrightarrow \phi)$ are satisfiable. Here $G(\cdot)$ is a global modality that stipulates that a formula is true at every world in a model. For a neighbourhood model $(W, N, \theta)$, $w \in W$, and a formula $\phi \in \mathcal{L}$, we have that $M, w \models G(\phi) \iff M, w' \models \phi$, for all $w' \in W$, where $M, w \models \phi$ is as in Definition 4. Alternatively (and equivalently), $M, w \models G(\phi) \iff [\phi] = W$.

A clause is a formula in one of the following forms:

- local clauses: $\bigvee_i l_i$, where the $l_i$ are propositional or modal literals; or

- global clauses: $G(\bigvee_i l_i)$, where the $l_i$ are propositional or modal literals.

We often think of a clause as a set of literals and sometimes use set notation, that is, we identify $l_1 \lor \dots \lor l_n$ with the set $\{l_1, \dots, l_n\}$, for $n \in \mathbb{N}$. This allows us to also use set theoretic notation on clauses. For instance, for a literal $l$ and clause $\gamma$, we may write $l \in \gamma$ and say that $l$ is an element of $\gamma$. Similarly, $\gamma_1 \subseteq \gamma_2$ means that all literals of $\gamma_1$ are literals of $\gamma_2$.

It is easy to see that every formula can be represented as a set of clauses. As most logics in the cube are non-monotonic, we only replace the argument of $\Box$ with an equivalent formula. As a consequence, the rewriting steps and introduction of new variables by renaming consistently use bi-implications ($\leftrightarrow$). For a fixed formula $\phi \in \mathcal{L}$, we let $\eta = \eta_\phi : \text{subf}(\phi) \to \mathcal{V} \setminus \mathcal{V}(\phi)$ be an injective renaming function that associates a fresh propositional variable to every (possibly negated) subformula of $\phi$.

**Proposition 7.** A formula $\phi$ is satisfiable if, and only if, $\{\eta(\phi)\} \cup \mathbf{R}(G(\eta(\phi) \leftrightarrow \phi))$ is satisfiable, where $\mathbf{R}$ is defined as follows and $t, p \in \mathcal{V}$:

$$
\begin{align*}
\mathbf{R}(G(t \leftrightarrow p)) &= \{G(\neg t \lor p), G(t \lor \neg p)\} \\
\mathbf{R}(G(t \leftrightarrow \neg \psi)) &= \{G(\neg t \lor \neg \eta(\psi)), G(t \lor \eta(\psi))\} \cup \mathbf{R}(G(\eta(\psi) \leftrightarrow \psi)) \\
\mathbf{R}(G(t \leftrightarrow \psi \lor \psi')) &= \{G(\neg t \lor \eta(\psi) \lor \neg \eta(\psi')), G(t \lor \neg \eta(\psi)), G(t \lor \neg \eta(\psi'))\} \\
&\quad \cup \mathbf{R}(G(\eta(\psi) \leftrightarrow \psi)) \cup \mathbf{R}(G(\eta(\psi') \leftrightarrow \psi')) \\
\mathbf{R}(G(t \leftrightarrow \Box \psi)) &= \{G(\neg t \lor \Box \eta(\psi)), G(t \lor \neg \Box \eta(\psi))\} \cup \mathbf{R}(G(\eta(\psi) \leftrightarrow \psi))
\end{align*}
$$

Moreover, the size of $\{\eta(\phi)\} \cup \{\mathbf{R}(G(\eta(\phi) \leftrightarrow \phi))\}$ is linear on the size of $\phi$.
The proof is standard. We can transform a model that satisfies $\phi$ into a model where $\eta(\phi)$ has exactly the same truth set as $\phi$ by just changing the valuation of the renaming symbol. Conversely, models that satisfy the transformation are automatically models of $\phi$. The number of recursive calls is proportional to the number of subformulae of $\phi$, hence the linear complexity bound.

The inference rules for the modal logic E and its extensions are given in Table 2. In the table, C and D are clauses, l are literals and p are propositional variables, possibly subscripted or primed. Inference rules are presented using standard notation with premisses and conclusion, called the resolvent separated by a horizontal line. Every inference rule except G2L has a local and a global variant, expressed by a leading L (resp. G) in its name. The second letter of the rule name indicates the logic axiomatised by the rule, so that e.g. GMRES is sound for the monotone modal logic EM. In the following, we give the intuition for the global inference rules that can be readily translated to their local variants. We consider the following four groups of inference rules.

- **Inference rules for all classical modal logics:** The rule GRES is a syntactical variation of the propositional resolution rule [46], the only differences being that reasoning is carried out within the global modality and that l occurring in the premisses may be a modal literal. The rule G2L asserts that local satisfiability is a consequence of its global counterpart. The rule GERES expresses that $\Box p$ and $\neg\Box p'$ are inconsistent whenever p and p' are globally equivalent, i.e. have the same truth set. By virtue of the side condition, we have three non-redundant instances: (1) $G(C) = G(\neg p \lor p')$ and $G(C') = G(p \lor \neg p')$, which means that p and p' are semantically equivalent; (2) $G(C) = G(\neg p)$ and $G(C') = G(\neg p')$, in which case p and p' are globally false and so semantically equivalent; or (3) $G(C) = G(p')$ and $G(C') = G(p)$, where p and p' are semantically equivalent as they are both globally true. All other instances are already contradictory or can be reduced to the above by means of GRES.

- **Inference rules for classical modal logics with aggregation** that validate the axiom C. The rules GCRES1 and GCRES2 are sound in classical modal logics containing the axiom C. They are similar to the rule GERES, but the side conditions for clauses $C_i$ ensure that $(p_1 \wedge \dots \wedge p_n \leftrightarrow p)$ is globally true.

- **Inference rules for monotone classical modal logics** that validate the axiom M: The rule GMRES is sound in logics that are monotone. This rule is a weaker version of GERES where congruence is required. For monotone logics, the rule RM (from $\phi \to \psi$ derive $\Box\phi \to \Box\psi$) holds. The side condition gives three concrete instances: (1) $C = G(\neg p \lor p')$, thus, from $\Box p$ in the first premiss we have that $\Box p'$ holds, which contradicts with $\neg\Box p'$ in the second premiss; (2) $C = G(\neg p)$, that is, p is globally false and, ex falso sequitur quodlibet, we again have that $\Box p'$ holds, which contradicts the modal literal in the second premiss; or (3) $C = G(p')$, from which we can derive $\neg\Box p'$, using the contrapositive of RM, which contradicts with the modal literal in the first premiss.

- **Inference rules for classical modal logics with the unit** that validate the axiom N: The rule GNRES is sound for these logics, as the premiss $G(p)$ says that $\neg\Box p$
The proof is standard. We can transform a model that satisfies $\phi$ into a model where $\eta(\phi)$ has exactly the same truth set as $\phi$ by just changing the valuation of the renaming symbol. Conversely, models that satisfy the transformation are automatically models of $\phi$. The number of recursive calls is proportional to the number of subformulae of $\phi$, hence the linear complexity bound.

The inference rules for the modal logic E and its extensions are given in Table 2. In the table, C and D are clauses, l are literals and p are propositional variables, possibly subscripted or primed. Inference rules are presented using standard notation with premisses and conclusion, called the resolvent separated by a horizontal line. Every inference rule except G2L has a local and a global variant, expressed by a leading L (resp. G) in its name. The second letter of the rule name indicates the logic axiomatised by the rule, so that e.g. GMRES is sound for the monotone modal logic EM. In the following, we give the intuition for the global inference rules that can be readily translated to their local variants. We consider the following four groups of inference rules.

- **Inference rules for all classical modal logics:** The rule GRES is a syntactical variation of the propositional resolution rule [46], the only differences being that reasoning is carried out within the global modality and that l occurring in the premisses may be a modal literal. The rule G2L asserts that local satisfiability is a consequence of its global counterpart. The rule GERES expresses that $\Box p$ and $\neg\Box p'$ are inconsistent whenever p and p' are globally equivalent, i.e. have the same truth set. By virtue of the side condition, we have three non-redundant instances: (1) $G(C) = G(\neg p \lor p')$ and $G(C') = G(p \lor \neg p')$, which means that p and p' are semantically equivalent; (2) $G(C) = G(\neg p)$ and $G(C') = G(\neg p')$, in which case p and p' are globally false and so semantically equivalent; or (3) $G(C) = G(p')$ and $G(C') = G(p)$, where p and p' are semantically equivalent as they are both globally true. All other instances are already contradictory or can be reduced to the above by means of GRES.

- **Inference rules for classical modal logics with aggregation** that validate the axiom C. The rules GCRES1 and GCRES2 are sound in classical modal logics containing the axiom C. They are similar to the rule GERES, but the side conditions for clauses $C_i$ ensure that $(p_1 \wedge \dots \wedge p_n \leftrightarrow p)$ is globally true.

- **Inference rules for monotone classical modal logics** that validate the axiom M: The rule GMRES is sound in logics that are monotone. This rule is a weaker version of GERES where congruence is required. For monotone logics, the rule RM (from $\phi \to \psi$ derive $\Box\phi \to \Box\psi$) holds. The side condition gives three concrete instances: (1) $C = G(\neg p \lor p')$, thus, from $\Box p$ in the first premiss we have that $\Box p'$ holds, which contradicts with $\neg\Box p'$ in the second premiss; (2) $C = G(\neg p)$, that is, p is globally false and, ex falso sequitur quodlibet, we again have that $\Box p'$ holds, which contradicts the modal literal in the second premiss; or (3) $C = G(p')$, from which we can derive $\neg\Box p'$, using the contrapositive of RM, which contradicts with the modal literal in the first premiss.

- **Inference rules for classical modal logics with the unit** that validate the axiom N: The rule GNRES is sound for these logics, as the premiss $G(p)$ says that $\neg\Box p$
<figure><img src="image_3.png" /><figcaption>**Table 2.** Inference Rules</figcaption></figure>

(or its global occurrence) cannot be satisfied, therefore it must be the case that the resolvent $G(D)$ is satisfied.

The basic resolution calculus, RES<sub>E</sub>, comprises the inference rules LRES, GRES, G2L, LERES and GERES. For the extensions of E, the calculi can be
<figure><img src="image_3.png" /><figcaption>**Table 2.** Inference Rules</figcaption></figure>

(or its global occurrence) cannot be satisfied, therefore it must be the case that the resolvent $G(D)$ is satisfied.

The basic resolution calculus, RES<sub>E</sub>, comprises the inference rules LRES, GRES, G2L, LERES and GERES. For the extensions of E, the calculi can be
<table><caption>**Table 3.** Inference rules corresponding to each logic</caption><thead><tr><th>Calculus</th><th>Inference Rules</th></tr></thead><tbody><tr><td>RES<sub>E</sub></td><td>LRES, GRES, G2L, LERES, GERES</td></tr><tr><td>RES<sub>EC</sub></td><td>LRES, GRES, G2L, LCRES1, GCRES1, LCRES2, GCRES2</td></tr><tr><td>RES<sub>EM</sub></td><td>LRES, GRES, G2L, LMRES, GMRES</td></tr><tr><td>RES<sub>EN</sub></td><td>LRES, GRES, G2L, LERES, GERES, LNRES, GNRES</td></tr><tr><td>RES<sub>EMC</sub></td><td>LRES, GRES, G2L, LCRES1, GCRES1, LCRES2, GCRES2, LMRES, GMRES</td></tr><tr><td>RES<sub>ECN</sub></td><td>LRES, GRES, G2L, LCRES1, GCRES1, LCRES2, GCRES2, LNRES, GNRES</td></tr><tr><td>RES<sub>EMN</sub></td><td>LRES, GRES, G2L, LMRES, GMRES, LNRES, GNRES</td></tr><tr><td>RES<sub>EMCN</sub></td><td>LRES, GRES, G2L, LCRES1, GCRES1, LCRES2, GCRES2, LMRES, GMRES, LNRES, GNRES</td></tr></tbody></table>

obtained in a modular way, that is, by just adding the rules that are sound with respect to the axioms for the logic. However, it is easy to see that, for instance, when considering monotone logics, whenever **LERES** or **GERES** can be applied, the rules **LMRES** or **GMRES** can also be applied, generating exactly the same resolvent. Thus, **LERES** and **GERES** are both redundant in the calculi for monotone logics. In Table 3 we give the rules for the calculus for each considered logic, but where redundant inference rules are suppressed. We denote by **RES<sub>L</sub>** the resolution calculus for a particular logic **L**.

The following definitions are needed before we establish our main results.

**Definition 8.** Let $\mathcal{C}$ be a finite set of clauses and $\mathbf{L} = \mathbf{E}\Sigma$ with $\Sigma \subseteq \{C, M, N\}$. A derivation from $\mathcal{C}$ in $\mathbf{RES_L}$ is a sequence of sets of clauses $C_0, C_1, \dots$ where $C_0 = \mathcal{C}$ and for every $i \in \mathbb{N}$, $C_{i+1} = C_i \cup \{D\}$ where the resolvent $D$ was obtained from $C_i$ by applying the rules of $\mathbf{RES_L}$ given in Table 3. We require that $D \notin C_i$ and that $D$ is not a tautology (that is, a clause containing $l$ and $\neg l$).

**Definition 9.** Let $\mathcal{C}$ be a finite set of clauses and $C_0, C_1, \dots$ a derivation from $\mathcal{C}$ in $\mathbf{RES_L}$ where $\mathbf{L} = \mathbf{E}\Sigma$ with $\Sigma \subseteq \{C, M, N\}$. If there is $k \in \mathbb{N}$ such that $\epsilon \in C_k$, then $C_0, C_1, \dots, C_k$ is a *refutation* of $\mathcal{C}$. If there is $k \in \mathbb{N}$ such that any resolvent $D$ obtained from $C_k$ by applying the rules of $\mathbf{RES_L}$ given in Table 3 to $C_k$ is such that $D \in C_k$, then $C_k$ is *saturated*, and $C_k$ is the *saturation* of $\mathcal{C}$.

The following two theorems establish termination and soundness of the calculi.

**Theorem 10.** Let $\mathbf{L} = \mathbf{E}\Sigma$ with $\Sigma \subseteq \{C, M, N\}$, $\mathcal{C}$ be a finite set of clauses and $C_0, C_1, \dots$ be a derivation from $\mathcal{C}$ in $\mathbf{RES_L}$. Then there is $k \in \mathbb{N}$ such that $C_k$ is saturated, or $C_0, C_1, \dots, C_k$ is a refutation.

As there is a finite number of literals in $\mathcal{C}$ and no inference rule introduces new literals, there is also an upper bound on the number of clauses that can be generated by $\mathbf{RES_L}$. Hence either the empty clause is generated at some $C_k$ or no new clauses can be generated. Thus, any derivation in $\mathbf{RES_L}$ terminates.

**Theorem 11.** Let $\mathbf{L} = \mathbf{E}\Sigma$ with $\Sigma \subseteq \{C, M, N\}$. Then $\mathbf{RES_L}$ is sound.
<table><caption>**Table 3.** Inference rules corresponding to each logic</caption><thead><tr><th>Calculus</th><th>Inference Rules</th></tr></thead><tbody><tr><td>RES<sub>E</sub></td><td>LRES, GRES, G2L, LERES, GERES</td></tr><tr><td>RES<sub>EC</sub></td><td>LRES, GRES, G2L, LCRES1, GCRES1, LCRES2, GCRES2</td></tr><tr><td>RES<sub>EM</sub></td><td>LRES, GRES, G2L, LMRES, GMRES</td></tr><tr><td>RES<sub>EN</sub></td><td>LRES, GRES, G2L, LERES, GERES, LNRES, GNRES</td></tr><tr><td>RES<sub>EMC</sub></td><td>LRES, GRES, G2L, LCRES1, GCRES1, LCRES2, GCRES2, LMRES, GMRES</td></tr><tr><td>RES<sub>ECN</sub></td><td>LRES, GRES, G2L, LCRES1, GCRES1, LCRES2, GCRES2, LNRES, GNRES</td></tr><tr><td>RES<sub>EMN</sub></td><td>LRES, GRES, G2L, LMRES, GMRES, LNRES, GNRES</td></tr><tr><td>RES<sub>EMCN</sub></td><td>LRES, GRES, G2L, LCRES1, GCRES1, LCRES2, GCRES2, LMRES, GMRES, LNRES, GNRES</td></tr></tbody></table>

obtained in a modular way, that is, by just adding the rules that are sound with respect to the axioms for the logic. However, it is easy to see that, for instance, when considering monotone logics, whenever **LERES** or **GERES** can be applied, the rules **LMRES** or **GMRES** can also be applied, generating exactly the same resolvent. Thus, **LERES** and **GERES** are both redundant in the calculi for monotone logics. In Table 3 we give the rules for the calculus for each considered logic, but where redundant inference rules are suppressed. We denote by **RES<sub>L</sub>** the resolution calculus for a particular logic **L**.

The following definitions are needed before we establish our main results.

**Definition 8.** Let $\mathcal{C}$ be a finite set of clauses and $\mathbf{L} = \mathbf{E}\Sigma$ with $\Sigma \subseteq \{\text{C},\text{M},\text{N}\}$. A derivation from $\mathcal{C}$ in $\mathbf{RES_L}$ is a sequence of sets of clauses $C_0, C_1, \dots$ where $C_0 = \mathcal{C}$ and for every $i \in \mathbb{N}$, $C_{i+1} = C_i \cup \{D\}$ where the resolvent $D$ was obtained from $C_i$ by applying the rules of $\mathbf{RES_L}$ given in Table 3. We require that $D \notin C_i$ and that $D$ is not a tautology (that is, a clause containing $l$ and $\neg l$).

**Definition 9.** Let $\mathcal{C}$ be a finite set of clauses and $C_0, C_1, \dots$ a derivation from $\mathcal{C}$ in $\mathbf{RES_L}$ where $\mathbf{L} = \mathbf{E}\Sigma$ with $\Sigma \subseteq \{\text{C},\text{M},\text{N}\}$. If there is $k \in \mathbb{N}$ such that $\epsilon \in C_k$, then $C_0, C_1, \dots, C_k$ is a *refutation* of $\mathcal{C}$. If there is $k \in \mathbb{N}$ such that any resolvent $D$ obtained from $C_k$ by applying the rules of $\mathbf{RES_L}$ given in Table 3 to $C_k$ is such that $D \in C_k$, then $C_k$ is *saturated*, and $C_k$ is the *saturation* of $\mathcal{C}$.

The following two theorems establish termination and soundness of the calculi.

**Theorem 10.** Let $\mathbf{L} = \mathbf{E}\Sigma$ with $\Sigma \subseteq \{\text{C},\text{M},\text{N}\}$, $\mathcal{C}$ be a finite set of clauses and $C_0, C_1, \dots$ be a derivation from $\mathcal{C}$ in $\mathbf{RES_L}$. Then there is $k \in \mathbb{N}$ such that $C_k$ is saturated, or $C_0, C_1, \dots, C_k$ is a refutation.

As there is a finite number of literals in $\mathcal{C}$ and no inference rule introduces new literals, there is also an upper bound on the number of clauses that can be generated by $\mathbf{RES_L}$. Hence either the empty clause is generated at some $C_k$ or no new clauses can be generated. Thus, any derivation in $\mathbf{RES_L}$ terminates.

**Theorem 11.** Let $\mathbf{L} = \mathbf{E}\Sigma$ with $\Sigma \subseteq \{\text{C},\text{M},\text{N}\}$. Then $\mathbf{RES_L}$ is sound.
The proof is by induction on the number of steps of a derivation: as every step of a derivation is satisfiability preserving, as argued above, then all derivations from satisfiable sets of clauses only generate satisfiable sets of clauses.

We present two examples before establishing completeness in the next section.

**Example 12.** We show that $\square(p \lor q) \rightarrow \square(p \lor \neg\square(a \lor \neg a) \lor q)$ is valid in the logic EN by using the calculus RES<sub>EN</sub>. For the refutation, we negate the formula and obtain $\phi = \square(p \lor q) \land \neg\square(p \lor \neg\square(a \lor \neg a) \lor q)$. We show next the relevant clauses resulting from the transformation, where we have that $\phi_1 = \square(p \lor q)$, $\phi_2 = \neg\square(p \lor \neg\square(a \lor \neg a) \lor q)$, and $\phi_3 = (p \lor \neg\square(a \lor \neg a) \lor q)$:

1. $t_\phi$ 8. $G(\neg t_{\phi_2} \lor \neg\square t_{\phi_3})$

2. $G(\neg t_\phi \lor t_{\phi_1})$ 9. $G(\neg t_{\phi_3} \lor t_p \lor t_q \lor \neg\square t_{a\lor\neg a})$

3. $G(\neg t_\phi \lor t_{\phi_2})$ 10. $G(t_{\phi_3} \lor \neg t_p)$

4. $G(\neg t_{\phi_1} \lor \square t_{p\lor q})$ 11. $G(t_{\phi_3} \lor \neg t_q)$

5. $G(\neg t_{p\lor q} \lor t_p \lor t_q)$ 12. $G(t_{a\lor\neg a} \lor \neg t_a)$

6. $G(t_{p\lor q} \lor \neg t_p)$ 13. $G(t_{a\lor\neg a} \lor \neg t_{\neg a})$

7. $G(t_{p\lor q} \lor \neg t_q)$ 14. $G(t_{\neg a} \lor t_a)$

The steps of the refutation are as follows:

15. $G(t_{a\lor\neg a} \lor t_a)$ [GRES, 13, 14]

16. $G(t_{a\lor\neg a})$ [GRES, 15, 12]

17. $G(\neg t_{\phi_3} \lor t_p \lor t_q)$ [GNRES, 16, 9]

18. $G(\neg t_{\phi_3} \lor t_{p\lor q} \lor t_p)$ [GRES, 17, 7]

19. $G(\neg t_{\phi_3} \lor t_{p\lor q})$ [GRES, 18, 6]

20. $G(t_{\phi_3} \lor \neg t_{p\lor q} \lor t_p)$ [GRES, 11, 5]

21. $G(t_{\phi_3} \lor \neg t_{p\lor q})$ [GRES, 20, 10]

22. $G(\neg t_{\phi_1} \lor \neg t_{\phi_2})$ [GERES, 4, 8, 19, 21]

23. $G(\neg t_\phi \lor \neg t_{\phi_1})$ [GRES, 22, 3]

24. $G(\neg t_\phi)$ [GRES, 23, 2]

25. $\neg t_\phi$ [G2L, 24]

26. $\epsilon$ [LRES, 25, 1]

**Example 13.** We now show that $\phi = \square p \land \square q \rightarrow \square(p \land q)$ is valid in EC. The transformation of $\neg\phi$ produces, among others, Clauses (1)–(7). The refutation is refreshingly short: it is obtained in two steps after an application of GCRES1:

1. $t_\phi$ 6. $G(\neg t_{p\land q} \lor t_q)$

2. $G(\neg t_\phi \lor \square t_p)$ 7. $G(t_{p\land q} \lor \neg t_p \lor \neg t_q)$

3. $G(\neg t_\phi \lor \square t_q)$ 8. $G(\neg t_\phi)$ [GCRES1, 2, 3, 4, 5, 6, 7]

4. $G(\neg t_\phi \lor \neg\square t_{p\land q})$ 9. $\neg t_\phi$ [G2L, 8]

5. $G(\neg t_{p\land q} \lor t_p)$ 10. $\epsilon$ [LRES, 9, 1]

# 4 Completeness

We prove completeness by means of a canonical model construction. Our maximally consistent sets comprise both local and global clauses. The proof of the truth lemma hinges on the fact that maximally consistent sets are negation complete, that is, they contain either a literal or its negation. In completeness proofs of Hilbert systems, the argument is as follows. If M is a maximally consistent
The proof is by induction on the number of steps of a derivation: as every step of a derivation is satisfiability preserving, as argued above, then all derivations from satisfiable sets of clauses only generate satisfiable sets of clauses.

We present two examples before establishing completeness in the next section.

**Example 12.** We show that $\square(p \lor q) \rightarrow \square(p \lor \neg\square(a \lor \neg a) \lor q)$ is valid in the logic EN by using the calculus RES<sub>EN</sub>. For the refutation, we negate the formula and obtain $\phi = \square(p \lor q) \land \neg\square(p \lor \neg\square(a \lor \neg a) \lor q)$. We show next the relevant clauses resulting from the transformation, where we have that $\phi_1 = \square(p \lor q)$, $\phi_2 = \neg\square(p \lor \neg\square(a \lor \neg a) \lor q)$, and $\phi_3 = (p \lor \neg\square(a \lor \neg a) \lor q)$:

1. $t_\phi$ 8. $G(\neg t_{\phi_2} \lor \neg\square t_{\phi_3})$

2. $G(\neg t_\phi \lor t_{\phi_1})$ 9. $G(\neg t_{\phi_3} \lor t_p \lor t_q \lor \neg\square t_{a\lor\neg a})$

3. $G(\neg t_\phi \lor t_{\phi_2})$ 10. $G(t_{\phi_3} \lor \neg t_p)$

4. $G(\neg t_{\phi_1} \lor \square t_{p\lor q})$ 11. $G(t_{\phi_3} \lor \neg t_q)$

5. $G(\neg t_{p\lor q} \lor t_p \lor t_q)$ 12. $G(t_{a\lor\neg a} \lor \neg t_a)$

6. $G(t_{p\lor q} \lor \neg t_p)$ 13. $G(t_{a\lor\neg a} \lor \neg t_{\neg a})$

7. $G(t_{p\lor q} \lor \neg t_q)$ 14. $G(t_{\neg a} \lor t_a)$

The steps of the refutation are as follows:

15. $G(t_{a\lor\neg a} \lor t_a)$ [GRES, 13, 14]

16. $G(t_{a\lor\neg a})$ [GRES, 15, 12]

17. $G(\neg t_{\phi_3} \lor t_p \lor t_q)$ [GNRES, 16, 9]

18. $G(\neg t_{\phi_3} \lor t_{p\lor q} \lor t_p)$ [GRES, 17, 7]

19. $G(\neg t_{\phi_3} \lor t_{p\lor q})$ [GRES, 18, 6]

20. $G(t_{\phi_3} \lor \neg t_{p\lor q} \lor t_p)$ [GRES, 11, 5]

21. $G(t_{\phi_3} \lor \neg t_{p\lor q})$ [GRES, 20, 10]

22. $G(\neg t_{\phi_1} \lor \neg t_{\phi_2})$ [GERES, 4, 8, 19, 21]

23. $G(\neg t_\phi \lor \neg t_{\phi_1})$ [GRES, 22, 3]

24. $G(\neg t_\phi)$ [GRES, 23, 2]

25. $\neg t_\phi$ [G2L, 24]

26. $\epsilon$ [LRES, 25, 1]

**Example 13.** We now show that $\phi = \square p \land \square q \rightarrow \square(p \land q)$ is valid in EC. The transformation of $\neg\phi$ produces, among others, Clauses (1)–(7). The refutation is refreshingly short: it is obtained in two steps after an application of GCRES1:

1. $t_\phi$ 6. $G(\neg t_{p\land q} \lor t_q)$

2. $G(\neg t_\phi \lor \square t_p)$ 7. $G(t_{p\land q} \lor \neg t_p \lor \neg t_q)$

3. $G(\neg t_\phi \lor \square t_q)$ 8. $G(\neg t_\phi)$ [GCRES1, 2, 3, 4, 5, 6, 7]

4. $G(\neg t_\phi \lor \neg\square t_{p\land q})$ 9. $\neg t_\phi$ [G2L, 8]

5. $G(\neg t_{p\land q} \lor t_p)$ 10. $\epsilon$ [LRES, 9, 1]

# 4 Completeness

We prove completeness by means of a canonical model construction. Our maximally consistent sets comprise both local and global clauses. The proof of the truth lemma hinges on the fact that maximally consistent sets are negation complete, that is, they contain either a literal or its negation. In completeness proofs of Hilbert systems, the argument is as follows. If $M$ is a maximally consistent
set, and neither $\phi \in M$ nor $\neg\phi \in M$, then both $M \cup \{\phi\}$ and $M \cup \{\neg\phi\}$ are
inconsistent, that is, $M \cup \{\phi\} \vdash \bot$ and $M \cup \{\neg\phi\} \vdash \bot$. Hence $M \vdash \neg\phi$ and $M \vdash \phi$
which contradicts the consistency of $M$, so that our supposition that neither
$\phi \in M$ nor $\neg\phi \in M$ must have been false.

However, this argument is not available for resolution calculi, where we take
a set $\mathcal{C}$ of local or global clauses to be consistent if $\mathcal{C} \nvdash \emptyset$. In the simplest calculus,
RES<sub>E</sub>, consider the set $\mathcal{C} = \{G(\neg p \lor q), G(\neg q \lor p), \neg \Box q\}$. Then clearly $\mathcal{C} \cup \{\Box p\} \vdash \epsilon$,
but it is patently false that $\mathcal{C} \vdash \neg \Box p$.

However, something nearly as useful eventuates: We have that $\mathcal{C} \vdash \neg\Box q$, and $\Box p$ and $\neg\Box q$ together are inconsistent over $\mathcal{C}$ (using a single application of LERES). That is, while we cannot derive $\neg\Box p$, at least we can derive a literal, here $\neg\Box q$, that is inconsistent with $\Box p$ over $\mathcal{C}$. This is captured in the notion of inconsistency predicate, where, in full generality, we need to consider the inconsistency of $n$-element sets to accommodate instances of LNRES (where we are going to designate singleton sets as inconsistent) and the LCRES rules (where inconsistent sets can contain any finite number of elements). We formulate this for an arbitrary resolution calculus.

**Definition 14.** A modal resolution calculus is a relation $\vdash$ between clause sets and clauses that is closed under propositional resolution. That is, $\mathcal{C} \vdash D \lor l$ and $\mathcal{C} \vdash D' \lor \neg l$ then $\mathcal{C} \vdash D \lor D'$, for all local clauses $D$ and literals $l$. Let $\vdash$ be a modal resolution calculus and $\mathcal{C}$ be a set of global clauses. An inconsistency predicate for $\mathcal{C}$ and $\vdash$ is a subset $\mathcal{P} \subseteq \mathcal{P}(\mathrm{Lit}(\mathcal{V}))$ such that the following three conditions hold:

1. Every element $I = \{l_1, \dots, l_n\} \in \mathcal{P}$ is inconsistent over $\mathcal{C}$, that is, there are global clauses $\Gamma_1, \dots, \Gamma_n$ such that $\{\Gamma_1, \dots, \Gamma_k, l_1, \dots, l_n\} \vdash \epsilon$ and $\mathcal{C} \vdash \Gamma_i$ for all $1 \le i \le k$.

2. The set $\mathcal{P}$ is closed under cut, that is $A \cup B \in \mathcal{P}$ whenever $A \cup \{l\} \in \mathcal{P}$ and $B \cup \{\neg l\} \in \mathcal{P}$.

3. Propositional literals are only inconsistent with their negations, i.e. $A = \{p, \neg p\}$ whenever $p \in A \in \mathcal{P}$ for a propositional variable $p \in \mathcal{V}$.

The formulation of inconsistency predicate instantiates to all modal calculi in the paper, where for a calculus RES, we say that $\mathcal{C} \vdash D$ if $D$ is in the saturation of $\mathcal{C}$. We think of an element $\{l_1, \dots, l_n\}$ of an inconsistency predicate not as a clause, but rather as a conjunction of singleton clauses (that is inconsistent as per the first requirement). The second requirement formalises the semantically sound condition $\bigcap_i a_i \cap \bigcap_j b_j = \emptyset$ whenever $x \cap \bigcap_i a_i = \emptyset = (W \setminus x) \cap \bigcap_j b_j$ for subsets $x, a_i, b_j \subseteq W$ of a set $W$. We require that, in the formulation of the condition, that $A \cup B$ is inconsistent, i.e., $\mathcal{C}$ proves a sufficient number of global clauses $\Gamma$ that, together with $A \cup B$, allows us to derive the empty clause $\epsilon$.

As an example, and a stepping stone to prove the completeness of classical modal logic, we have the following:

**Lemma 15.** Let $\vdash$ be the calculus for classical modal logic and let $\mathcal{C}$ be a set of global clauses. Then the set $\mathcal{P}_E$ containing
set, and neither $\phi \in M$ nor $\neg\phi \in M$, then both $M \cup \{\phi\}$ and $M \cup \{\neg\phi\}$ are
inconsistent, that is, $M \cup \{\phi\} \vdash \bot$ and $M \cup \{\neg\phi\} \vdash \bot$. Hence $M \vdash \neg\phi$ and $M \vdash \phi$
which contradicts the consistency of $M$, so that our supposition that neither
$\phi \in M$ nor $\neg\phi \in M$ must have been false.

However, this argument is not available for resolution calculi, where we take
a set $\mathcal{C}$ of local or global clauses to be consistent if $\mathcal{C} \nvdash \emptyset$. In the simplest calculus,
RES<sub>E</sub>, consider the set $\mathcal{C} = \{G(\neg p \lor q), G(\neg q \lor p), \neg\Box q\}$. Then clearly $\mathcal{C} \cup \{\Box p\} \vdash \epsilon$,
but it is patently false that $\mathcal{C} \vdash \neg\Box p$.

However, something nearly as useful eventuates: We have that $\mathcal{C} \vdash \neg\Box q$, and $\Box p$ and $\neg\Box q$ together are inconsistent over $\mathcal{C}$ (using a single application of LERES). That is, while we cannot derive $\neg\Box p$, at least we can derive a literal, here $\neg\Box q$, that is inconsistent with $\Box p$ over $\mathcal{C}$. This is captured in the notion of inconsistency predicate, where, in full generality, we need to consider the inconsistency of $n$-element sets to accommodate instances of LNRES (where we are going to designate singleton sets as inconsistent) and the LCRES rules (where inconsistent sets can contain any finite number of elements). We formulate this for an arbitrary resolution calculus.

**Definition 14.** A modal resolution calculus is a relation $\vdash$ between clause sets and clauses that is closed under propositional resolution. That is, $\mathcal{C} \vdash D \lor l$ and $\mathcal{C} \vdash D' \lor \neg l$ then $\mathcal{C} \vdash D \lor D'$, for all local clauses $D$ and literals $l$. Let $\vdash$ be a modal resolution calculus and $\mathcal{C}$ be a set of global clauses. An inconsistency predicate for $\mathcal{C}$ and $\vdash$ is a subset $\mathcal{P} \subseteq \mathcal{P}(\mathrm{Lit}(\mathcal{V}))$ such that the following three conditions hold:

1. Every element $I = \{l_1, \dots, l_n\} \in \mathcal{P}$ is inconsistent over $\mathcal{C}$, that is, there are global clauses $\Gamma_1, \dots, \Gamma_n$ such that $\{\Gamma_1, \dots, \Gamma_k, l_1, \dots, l_n\} \vdash \epsilon$ and $\mathcal{C} \vdash \Gamma_i$ for all $1 \le i \le k$.

2. The set $\mathcal{P}$ is closed under cut, that is $A \cup B \in \mathcal{P}$ whenever $A \cup \{l\} \in \mathcal{P}$ and $B \cup \{\neg l\} \in \mathcal{P}$.

3. Propositional literals are only inconsistent with their negations, i.e. $A = \{p, \neg p\}$ whenever $p \in A \in \mathcal{P}$ for a propositional variable $p \in \mathcal{V}$.

The formulation of inconsistency predicate instantiates to all modal calculi in
the paper, where for a calculus RES, we say that $\mathcal{C} \vdash D$ if $D$ is in the saturation
of $\mathcal{C}$. We think of an element $\{l_1, \dots, l_n\}$ of an inconsistency predicate not as a
clause, but rather as a conjunction of singleton clauses (that is inconsistent as
per the first requirement). The second requirement formalises the semantically
sound condition $\bigcap_i a_i \cap \bigcap_j b_j = \emptyset$ whenever $x \cap \bigcap_i a_i = \emptyset = (W \setminus x) \cap \bigcap_j b_j$
for subsets $x, a_i, b_j \subseteq W$ of a set $W$. We require that, in the formulation of the
condition, that $A \cup B$ is inconsistent, i.e., $\mathcal{C}$ proves a sufficient number of global
clauses $\Gamma$ that, together with $A \cup B$, allows us to derive the empty clause $\epsilon$.

As an example, and a stepping stone to prove the completeness of classical
modal logic, we have the following:

**Lemma 15.** Let $\vdash$ be the calculus for classical modal logic and let $\mathcal{C}$ be a set of global clauses. Then the set $\mathcal{P}_E$ containing
- the set $\{l, \neg l\}$ for every (propositional or modal) literal $l \in \text{Lit}(\mathcal{V})$, and

- the set $\{\Box p, \neg \Box q\}$ for every pair $p, q \in \mathcal{V}$ of propositions such that $C \vdash G(C)$ and $C \vdash G(C')$ for sub-clauses $C \subseteq (\neg p \lor q)$ and $C' \subseteq (\neg q \lor p)$.

is an inconsistency predicate for $\vdash$ and $C$.

*Proof (Sketch).* The inconsistency requirement is clear, as every element of an inconsistency predicate is an instance of a resolution rule. For cut closure, apply GRES to premisses of a rule inducing a cut.

The following definition is an adaptation of the deduction theorem to modal resolution calculi. The reader is encouraged to instantiate this to the case of the modal logic $\mathbf{E}$ (and the inconsistency predicate of Lemma 15), as we do in the example following the definition.

**Definition 16.** An inconsistency predicate $\mathbf{P}$ is *compatible* with a modal resolution calculus $\vdash$ if for every local clause $D$ and every (propositional or modal) literal $l$ with $C \cup \{l\} \vdash D$, either $D = l$ or there is $n \ge 0$ and $D_1, \dots, D_n, E_1, \dots, E_n$ such that

- $D = D_1 \lor \dots \lor D_n$

- $C \vdash E_i \lor D_i$ for all $1 \le i \le n$

- $\{l, e_1, \dots, e_n\} \in \mathbf{P}$ for all $e_1, \dots, e_n$ with $e_i \in E_i$.

For the case of classical modal logic, the definition of compatibility takes the following form.

**Example 17.** If $\vdash$ is the resolution calculus for the classical modal logic $\mathbf{E}$, the inconsistency predicate $\mathbf{P}_E$ from Lemma 15 is binary. As a consequence, the above definition can only be instantiated with $n = 1$. Hence $\mathbf{P}_E$ is compatible, if for all literals $l$ and all local clauses $D$ with $C \cup \{l\} \vdash D$ either $D = l$ or there is a local clause $E$ such that $C \vdash E \lor D$ and $\{l, e\} \in \mathbf{P}_E$ for all $e \in E$.

As a second example, and to make further progress to completeness of the resolution calculus $\vdash$ for classical modal logic, we establish that the inconsistency predicate $\mathbf{P}_E$ from Lemma 15 is indeed compatible.

**Lemma 18.** *The inconsistency relation $\mathbf{P}_E$ from Lemma 15 is compatible with the resolution calculus $\vdash$ for classical modal logic.*

The proof proceeds by induction on the derivation of $C \cup \{l\}$ and is omitted.

Finally, we can reap some of the benefits of our work, and take the next step towards showing that maximally consistent sets are negation complete, i.e. for every literal $l$, they contain either $l$ or $\neg l$.

**Lemma 19.** Let $C$ be a set of local or global clauses, $l$ be a literal and $\mathbf{P}$ be a compatible inconsistency predicate. If $C \cup \{l\} \vdash \epsilon$ and $C \cup \{\neg l\} \vdash \epsilon$, then $C \vdash \epsilon$.
- the set $\{l, \neg l\}$ for every (propositional or modal) literal $l \in \text{Lit}(\mathcal{V})$, and

- the set $\{\Box p, \neg \Box q\}$ for every pair $p, q \in \mathcal{V}$ of propositions such that $C \vdash G(C)$ and $C \vdash G(C')$ for sub-clauses $C \subseteq (\neg p \lor q)$ and $C' \subseteq (\neg q \lor p)$.

is an inconsistency predicate for $\vdash$ and $C$.

*Proof (Sketch).* The inconsistency requirement is clear, as every element of an inconsistency predicate is an instance of a resolution rule. For cut closure, apply GRES to premisses of a rule inducing a cut.

The following definition is an adaptation of the deduction theorem to modal resolution calculi. The reader is encouraged to instantiate this to the case of the modal logic $\mathbf{E}$ (and the inconsistency predicate of Lemma 15), as we do in the example following the definition.

**Definition 16.** An inconsistency predicate $\mathbf{P}$ is *compatible* with a modal resolution calculus $\vdash$ if for every local clause $D$ and every (propositional or modal) literal $l$ with $C \cup \{l\} \vdash D$, either $D = l$ or there is $n \ge 0$ and $D_1, \dots, D_n, E_1, \dots, E_n$ such that

- $D = D_1 \lor \dots \lor D_n$

- $C \vdash E_i \lor D_i$ for all $1 \le i \le n$

- $\{l, e_1, \dots, e_n\} \in \mathbf{P}$ for all $e_1, \dots, e_n$ with $e_i \in E_i$.

For the case of classical modal logic, the definition of compatibility takes the following form.

**Example 17.** If $\vdash$ is the resolution calculus for the classical modal logic $\mathbf{E}$, the inconsistency predicate $\mathbf{P}_E$ from Lemma 15 is binary. As a consequence, the above definition can only be instantiated with $n = 1$. Hence $\mathbf{P}_E$ is compatible, if for all literals $l$ and all local clauses $D$ with $C \cup \{l\} \vdash D$ either $D = l$ or there is a local clause $E$ such that $C \vdash E \lor D$ and $\{l, e\} \in \mathbf{P}_E$ for all $e \in E$.

As a second example, and to make further progress to completeness of the resolution calculus $\vdash$ for classical modal logic, we establish that the inconsistency predicate $\mathbf{P}_E$ from Lemma 15 is indeed compatible.

**Lemma 18.** *The inconsistency relation $\mathbf{P}_E$ from Lemma 15 is compatible with the resolution calculus $\vdash$ for classical modal logic.*

The proof proceeds by induction on the derivation of $C \cup \{l\}$ and is omitted.

Finally, we can reap some of the benefits of our work, and take the next step towards showing that maximally consistent sets are negation complete, i.e. for every literal $l$, they contain either $l$ or $\neg l$.

**Lemma 19.** Let $C$ be a set of local or global clauses, $l$ be a literal and $\mathbf{P}$ be a compatible inconsistency predicate. If $C \cup \{l\} \vdash \epsilon$ and $C \cup \{\neg l\} \vdash \epsilon$, then $C \vdash \epsilon$.
*Proof.* We demonstrate the proof for the special case of a binary inconsistency relation $\mathbf{P}$, i.e. every set $A \in \mathbf{P}$ has two elements. As $\mathcal{C} \cup \{l\} \vdash \epsilon$, we have a local clause $E$ such that $\mathcal{C} \vdash E$, and $\{e, l\} \in \mathbf{P}$ for all $e \in E$ by compatibility. Similarly, as $\mathcal{C} \cup \{\neg l\} \vdash \epsilon$, we have a local clause $E'$ with $\{\neg l, e'\} \in \mathbf{P}$ for all $e' \in E'$. If either $E = \epsilon$ or $E' = \epsilon$ we are done. If not, we have $\{e, e'\} \in \mathbf{P}$ for all $e \in E$ and $e' \in E'$ as $\mathbf{P}$ is cut closed. This allows us to construct a resolution proof of $\epsilon$ from $\mathcal{C} \vdash E$ and $\mathcal{C} \vdash E'$ as $\mathbf{P}$ is an inconsistency predicate.

**Remark 20.** For classical modal logic, we have shown that $\mathcal{C} \cup \{l\} \vdash D$, then either $D = l$ or $\mathcal{C} \vdash E \lor D$ where $\{l, e\} \in \mathbf{P}$ for all $e \in E$, where $\mathbf{P}$ is the inconsistency predicate from Lemma 15.

One might hypothesise whether $E$ can always be chosen to be a singleton, or at least a sub-singleton. We show, by means of example, that neither is the case. First, we cannot always choose $E$ as singleton: For $\mathcal{C} = \{p\}$ and $l = q$, we have that $\mathcal{C} \cup \{l\} \vdash p$ but we do not have $\mathcal{C} \vdash E \lor p$ for any singleton clause $E$ (here, $E = \epsilon$ satisfies the condition).

We also cannot always choose $E$ to be a sub-singleton clause. For example, put $\mathcal{C} = \{\neg\Box q \lor \neg\Box p \lor D, G(\neg p \lor q), G(p \lor \neg q)\}$. Then $\mathcal{C} \cup \{\Box p\} \vdash D$, but there is no sub-singleton clause $E$ so that $\mathcal{C} \vdash E \lor D$.

We have now collected all the preliminaries to define and investigate maximally consistent sets, i.e. the worlds of the canonical model.

**Definition 21.** Let $\mathcal{C}$ be a set of global clauses. A *local extension* of $\mathcal{C}$ is a set $M$ of clauses that extends $\mathcal{C}$ by local clauses only. That is, a local extension of $\mathcal{C}$ is a set $M$ of clauses that satisfies $\{\Gamma \in M \mid \Gamma \text{ global}\} = \mathcal{C}$.

A local extension of $\mathcal{C}$ is *maximally consistent* if $M$ is consistent ($M \not\vdash \epsilon$) and every other consistent local extension of $M'$ of $\Gamma$ that encompasses $M$ ($M' \supseteq M$) satisfies $M = M'$.

Calculi with a compatible inconsistency relation are negation complete.

**Lemma 22.** Let $\vdash$ be a modal calculus with a compatible inconsistency relation, and let $M$ be a maximally consistent local extension of a set $\mathcal{C}$ of global clauses. Then, for every (propositional or modal) literal $l$, we have $l \in M$ or $\neg l \in M$.

*Proof.* If neither $l \in M$ nor $\neg l \in M$, then $M \cup \{l\} \vdash \epsilon$ and $M \cup \{\neg l\} \vdash \epsilon$. Applying Lemma 19 now contradicts the consistency of $M$.

As we have insisted that resolution calculi are closed under propositional resolution, they are also disjunction complete:

**Corollary 23.** Let $\vdash$ be a modal resolution calculus with a compatible inconsistency relation, and let $M$ be a maximally consistent local extension of a set $\mathcal{C}$ of global clauses. If $l_1 \lor \dots \lor l_n \in M$, then there exists $1 \le i \le n$ such that $l_i \in M$.

*Proof.* If neither $l_i \in M$, then all $\neg l_i \in M$ and we conclude inconsistency of $M$.
*Proof.* We demonstrate the proof for the special case of a binary inconsistency relation $\mathbf{P}$, i.e. every set $A \in \mathbf{P}$ has two elements. As $\mathcal{C} \cup \{l\} \vdash \epsilon$, we have a local clause $E$ such that $\mathcal{C} \vdash E$, and $\{e, l\} \in \mathbf{P}$ for all $e \in E$ by compatibility. Similarly, as $\mathcal{C} \cup \{\neg l\} \vdash \epsilon$, we have a local clause $E'$ with $\{\neg l, e'\} \in \mathbf{P}$ for all $e' \in E'$. If either $E = \epsilon$ or $E' = \epsilon$ we are done. If not, we have $\{e, e'\} \in \mathbf{P}$ for all $e \in E$ and $e' \in E'$ as $\mathbf{P}$ is cut closed. This allows us to construct a resolution proof of $\epsilon$ from $\mathcal{C} \vdash E$ and $\mathcal{C} \vdash E'$ as $\mathbf{P}$ is an inconsistency predicate.

**Remark 20.** For classical modal logic, we have shown that $\mathcal{C} \cup \{l\} \vdash D$, then either $D = l$ or $\mathcal{C} \vdash E \lor D$ where $\{l, e\} \in \mathbf{P}$ for all $e \in E$, where $\mathbf{P}$ is the inconsistency predicate from Lemma 15.

One might hypothesise whether $E$ can always be chosen to be a singleton, or at least a sub-singleton. We show, by means of example, that neither is the case. First, we cannot always choose $E$ as singleton: For $\mathcal{C} = \{p\}$ and $l = q$, we have that $\mathcal{C} \cup \{l\} \vdash p$ but we do not have $\mathcal{C} \vdash E \lor p$ for any singleton clause $E$ (here, $E = \epsilon$ satisfies the condition).

We also cannot always choose $E$ to be a sub-singleton clause. For example, put $\mathcal{C} = \{\neg\Box q \lor \neg\Box p \lor D, G(\neg p \lor q), G(p \lor \neg q)\}$. Then $\mathcal{C} \cup \{\Box p\} \vdash D$, but there is no sub-singleton clause $E$ so that $\mathcal{C} \vdash E \lor D$.

We have now collected all the preliminaries to define and investigate maximally consistent sets, i.e. the worlds of the canonical model.

**Definition 21.** Let $\mathcal{C}$ be a set of global clauses. A *local extension* of $\mathcal{C}$ is a set $M$ of clauses that extends $\mathcal{C}$ by local clauses only. That is, a local extension of $\mathcal{C}$ is a set $M$ of clauses that satisfies $\{\Gamma \in M \mid \Gamma \text{ global}\} = \mathcal{C}$.

A local extension of $\mathcal{C}$ is *maximally consistent* if $M$ is consistent ($M \not\vdash \epsilon$) and every other consistent local extension of $M'$ of $\Gamma$ that encompasses $M$ ($M' \supseteq M$) satisfies $M = M'$.

Calculi with a compatible inconsistency relation are negation complete.

**Lemma 22.** Let $\vdash$ be a modal calculus with a compatible inconsistency relation, and let $M$ be a maximally consistent local extension of a set $\mathcal{C}$ of global clauses. Then, for every (propositional or modal) literal $l$, we have $l \in M$ or $\neg l \in M$.

*Proof.* If neither $l \in M$ nor $\neg l \in M$, then $M \cup \{l\} \vdash \epsilon$ and $M \cup \{\neg l\} \vdash \epsilon$. Applying Lemma 19 now contradicts the consistency of $M$.

As we have insisted that resolution calculi are closed under propositional resolution, they are also disjunction complete:

**Corollary 23.** Let $\vdash$ be a modal resolution calculus with a compatible inconsistency relation, and let $M$ be a maximally consistent local extension of a set $\mathcal{C}$ of global clauses. If $l_1 \lor \dots \lor l_n \in M$, then there exists $1 \le i \le n$ such that $l_i \in M$.

*Proof.* If neither $l_i \in M$, then all $\neg l_i \in M$ and we conclude inconsistency of $M$.
Compatible inconsistency predicates allow us to assert properties relative to derivations of a clause with the help of an additional singleton clause. The following lemma generalises this to a finite number of singleton clauses, but requires that the singleton clauses be *propositional*. This allows us to harness the fact that propositional literals are only inconsistent with their negation, which is enough to establish the hypotheses of the form $G(C)$ where $C \subseteq D$ is a sub-clause of a propositional clause $D$.

**Lemma 24.** Let $\vdash$ be a modal resolution calculus with compatible inconsistency predicate. Moreover, suppose that $C$ is a set of global clauses, $l_1, \dots, l_n$ are propositional literals and $D$ is a (local) clause such that $l_i \notin D$ for all $i = 1, \dots, n$, and $C \cup \{l_1, \dots, l_n\} \vdash D$. Then there is a sub-clause $E_0 \subseteq \neg l_1 \vee \dots \vee \neg l_n$ such that $C \vdash E \vee D$.

*Proof.* By induction on the number $n$ of literals, where $n = 0$ is evident. If $C \cup \{l_1, \dots, l_{n+1}\} \vdash D$, we have that $C \cup \{l_1, \dots, l_n\} \vdash E_0 \vee D$ where $\{e, l_{n+1}\} \in \mathbf{P}$, for all $e \in E_0$. This implies that either $E_0 = \epsilon$ or $E_0 = \neg l_{n+1}$. The claim follows by applying the inductive hypothesis.

The above lemma *fails* without assuming that the $l_i$ are propositional literals, as illustrated by the example at the beginning of this section.

In the proof of the truth lemma, we need to show derivability of premisses (of modal rules) based on the truth set of formulae in maximally consistent sets. The following corollary establishes this for local clauses, which we will then lift to global derivability.

**Corollary 25.** Consider a modal resolution calculus with a compatible inconsistency predicate, and let $C$ be a set of global clauses, and let $D = l_1 \vee \dots \vee l_n$ be a propositional clause such that all maximally consistent local extensions $M$ of $C$ contain at least one $l_i$ ($i = 1, \dots, n$). Then there exists a sub-clause $D_0 \subseteq D$ such that $C \vdash D_0$.

The next property is obviously present in the calculus $RE$ and its extensions.

**Definition 26.** A modal resolution calculus has the *global lifting property* if, for any set $C$ of global clauses, and a *local* clause $D$, we have that $C \vdash G(D)$ whenever $C \vdash D$.

For our calculi, this essentially means that rules with a global clause as a conclusion only have global clauses as premisses.

**Lemma 27.** *The calculus $RES_E$, as well as all other calculi discussed in this paper, has the global lifting property.*

We finally turn to canonical models, where we isolate the construction that is identical for all of the logics that we treat here.

**Definition 28 (Canonical Model).** Let $C$ be a set of global clauses. The $C$-canonical model, or the canonical model based on $C$, is the triple $(W, N, \theta)$ where
Compatible inconsistency predicates allow us to assert properties relative to derivations of a clause with the help of an additional singleton clause. The following lemma generalises this to a finite number of singleton clauses, but requires that the singleton clauses be *propositional*. This allows us to harness the fact that propositional literals are only inconsistent with their negation, which is enough to establish the hypotheses of the form $G(C)$ where $C \subseteq D$ is a sub-clause of a propositional clause $D$.

**Lemma 24.** Let $\vdash$ be a modal resolution calculus with compatible inconsistency predicate. Moreover, suppose that $C$ is a set of global clauses, $l_1, \dots, l_n$ are propositional literals and $D$ is a (local) clause such that $l_i \notin D$ for all $i = 1, \dots, n$, and $C \cup \{l_1, \dots, l_n\} \vdash D$. Then there is a sub-clause $E_0 \subseteq \neg l_1 \vee \dots \vee \neg l_n$ such that $C \vdash E \vee D$.

*Proof.* By induction on the number $n$ of literals, where $n = 0$ is evident. If $C \cup \{l_1, \dots, l_{n+1}\} \vdash D$, we have that $C \cup \{l_1, \dots, l_n\} \vdash E_0 \vee D$ where $\{e, l_{n+1}\} \in P$, for all $e \in E_0$. This implies that either $E_0 = \epsilon$ or $E_0 = \neg l_{n+1}$. The claim follows by applying the inductive hypothesis.

The above lemma *fails* without assuming that the $l_i$ are propositional literals, as illustrated by the example at the beginning of this section.

In the proof of the truth lemma, we need to show derivability of premisses (of modal rules) based on the truth set of formulae in maximally consistent sets. The following corollary establishes this for local clauses, which we will then lift to global derivability.

**Corollary 25.** Consider a modal resolution calculus with a compatible inconsistency predicate, and let $C$ be a set of global clauses, and let $D = l_1 \vee \dots \vee l_n$ be a propositional clause such that all maximally consistent local extensions $M$ of $C$ contain at least one $l_i$ ($i = 1, \dots, n$). Then there exists a sub-clause $D_0 \subseteq D$ such that $C \vdash D_0$.

The next property is obviously present in the calculus $RE$ and its extensions.

**Definition 26.** A modal resolution calculus has the *global lifting property* if, for any set $C$ of global clauses, and a local clause $D$, we have that $C \vdash G(D)$ whenever $C \vdash D$.

For our calculi, this essentially means that rules with a global clause as a conclusion only have global clauses as premisses.

**Lemma 27.** *The calculus $RES_E$, as well as all other calculi discussed in this paper, has the global lifting property.*

We finally turn to canonical models, where we isolate the construction that is identical for all of the logics that we treat here.

**Definition 28 (Canonical Model).** Let $C$ be a set of global clauses. The $C$-canonical model, or the canonical model based on $C$, is the triple $(W, N, \theta)$ where
- $W$ is the set of all maximally consistent local extensions of $C$

- $\theta(p) = \{M \in W \mid p \in M\}$

- $N(M) = \{\theta(p) \mid \Box p \in M\}$.

Here, consistent and maximally consistent refers to consistency in the modal resolution calculus $\mathbf{RES}_E$ for classical modal logic.

This gives the truth lemma for classical modal logic.

**Lemma 29 (Truth Lemma).** For the calculus $\mathbf{RE}$, let $(W, N, \theta)$ be the $C$-canonical model for some set $C$ of global clauses. Then, for $M \in W$, $M \models \Gamma$ whenever $\Gamma \in M$, for all local clauses $\Gamma$.

*Proof.* By disjunction completeness, it suffices to show the claim for singleton clauses. The propositional cases and $\Box p \in M$ are easy. For the only interesting case assume $\neg\Box p \in M$, and assume for a contradiction that $\theta(p) \in N(M)$. By construction, there must be a variable $q \in \mathcal{V}$ with $\Box q \in M$ and $\theta(p) = \theta(q)$. That is $p \in M' \iff q \in M'$ for all maximally consistent local extensions $M'$ of $C$. By Corollary 25 and Lemma 27 we obtain the premisses of the modal rule that proves $M \vdash \epsilon$, contradiction.

**Remark 30.** In the proof of the truth lemma, the modal rule was only used in a very specific form, i.e. $D = D' = \epsilon$ in definition of the modal rule. The more general form of the rule is needed to establish Lemma 18. The reader is also invited to convince themselves that completeness fails without the more general form, for example to show that $C = \{G(\neg p \lor q), G(\neg q \lor p), G(\neg q \lor r), G(\neg r \lor q), \neg\Box p \lor \neg\Box q, \Box r\}$ is inconsistent.

We have used the rule $\mathbf{GRES}$ in the proof of Lemma 18. The rule $\mathbf{GERES}$ is hidden in the proof of Lemma 27. The reader is invited to convince themselves that $\mathbf{GERES}$ is needed to show the inconsistency of $\{G(\neg p \lor q \lor \Box r), G(p \lor \neg q), G(\neg \Box s), G(s), G(r), G(\neg \Box q)\}$.

**Corollary 31.** Let $C$ be a set of local or global clauses. If $C$ is unsatisfiable in the class of neighbourhood models, then $C \vdash \epsilon$.

## 4.1 Monotone Modal Logic

To show completeness for the resolution calculus for monotone modal logic, we follow the same approach, and start with a compatible inconsistency predicate.

**Lemma 32.** Let $\vdash$ be the calculus for monotone modal logic and let $C$ be a set of global clauses. Then the set $P_M$ containing

- the set $\{l, \neg l\}$ for every (propositional or modal) literal $l \in \text{Lit}(\mathcal{V})$, and

- the set $\{\Box p, \neg \Box q\}$ for every pair $p, q \in \mathcal{V}$ of propositions such that $C \vdash G(C)$ for a sub-clauses $C \subseteq \neg p \lor q$.

is a compatible inconsistency predicate for $\vdash$ and $C$.
- $W$ is the set of all maximally consistent local extensions of $C$

- $\theta(p) = \{M \in W \mid p \in M\}$

- $N(M) = \{\theta(p) \mid \Box p \in M\}$.

Here, consistent and maximally consistent refers to consistency in the modal resolution calculus $\mathbf{RES}_E$ for classical modal logic.

This gives the truth lemma for classical modal logic.

**Lemma 29 (Truth Lemma).** For the calculus $\mathbf{RE}$, let $(W, N, \theta)$ be the $C$-canonical model for some set $C$ of global clauses. Then, for $M \in W$, $M \models \Gamma$ whenever $\Gamma \in M$, for all local clauses $\Gamma$.

*Proof.* By disjunction completeness, it suffices to show the claim for singleton clauses. The propositional cases and $\Box p \in M$ are easy. For the only interesting case assume $\neg\Box p \in M$, and assume for a contradiction that $\theta(p) \in N(M)$. By construction, there must be a variable $q \in \mathcal{V}$ with $\Box q \in M$ and $\theta(p) = \theta(q)$. That is $p \in M' \iff q \in M'$ for all maximally consistent local extensions $M'$ of $C$. By Corollary 25 and Lemma 27 we obtain the premisses of the modal rule that proves $M \vdash \epsilon$, contradiction.

**Remark 30.** In the proof of the truth lemma, the modal rule was only used in a very specific form, i.e. $D = D' = \epsilon$ in definition of the modal rule. The more general form of the rule is needed to establish Lemma 18. The reader is also invited to convince themselves that completeness fails without the more general form, for example to show that $C = \{G(\neg p \lor q), G(\neg q \lor p), G(\neg q \lor r), G(\neg r \lor q), \neg\Box p \lor \neg\Box q, \Box r\}$ is inconsistent.

We have used the rule $\mathbf{GRES}$ in the proof of Lemma 18. The rule $\mathbf{GERES}$ is hidden in the proof of Lemma 27. The reader is invited to convince themselves that $\mathbf{GERES}$ is needed to show the inconsistency of $\{G(\neg p \lor q \lor \Box r), G(p \lor \neg q), G(\neg \Box s), G(s), G(r), G(\neg \Box q)\}$.

**Corollary 31.** Let $C$ be a set of local or global clauses. If $C$ is unsatisfiable in the class of neighbourhood models, then $C \vdash \epsilon$.

## 4.1 Monotone Modal Logic

To show completeness for the resolution calculus for monotone modal logic, we follow the same approach, and start with a compatible inconsistency predicate.

**Lemma 32.** Let $\vdash$ be the calculus for monotone modal logic and let $C$ be a set of global clauses. Then the set $P_M$ containing

- the set $\{l, \neg l\}$ for every (propositional or modal) literal $l \in \text{Lit}(\mathcal{V})$, and

- the set $\{\Box p, \neg \Box q\}$ for every pair $p, q \in \mathcal{V}$ of propositions such that $C \vdash G(C)$ for a sub-clauses $C \subseteq \neg p \lor q$.

is a compatible inconsistency predicate for $\vdash$ and $C$.
The proof is very similar to that of classical modal logic (Lemma 15 and Lemma 18). The canonical model construction is an adaptation of the construction for E where the construction ensures that the set of neighbourhoods is upward closed.

**Definition 33.** Let $C$ be a set of global clauses. The $C$-canonical model for the calculus $RES_{EM}$ is the triple $(W, N, \theta)$ where $W$ and $\theta$ are the same as for classical modal logic (Definition 28) and the neighbourhood function $N$ is defined by

$$N(M) = \{\alpha \subseteq W \mid \theta(p) \subseteq \alpha \text{ for some } \Box p \in M\}.$$

where $M \in W$ is a maximally consistent, local extension of $C$.

It is obvious that canonical models for $RES_{EM}$ are monotone by construction, but we need to re-establish the truth lemma for the calculus $RES_{EM}$ as the construction of the model has changed.

**Lemma 34 (Truth Lemma for EM).** For the calculus $RES_{EM}$, let $(W, N, \theta)$ be the $C$-canonical model for some set $C$ of global clauses. Then, for $M \in W$, $M \models \Gamma$ whenever $\Gamma \in M$, for all local clauses $\Gamma$.

The proof is in fact a simplification of the corresponding proof for classical modal logic, and we obtain completeness similar to Corollary 31.

**Corollary 35.** Monotone modal logic is complete, i.e. any consistent set $C$ of local or global clauses satisfies $C \vdash \epsilon$ whenever $C$ is unsatisfiable in the class of monotone neighbourhood models.

## 4.2 Logics with Unit

We now adapt the construction to also incorporate logics with unit, i.e the modal logics EN and EMN that – in addition to the frame conditions for E and EM – additionally require that the entire set of worlds is always a neighbourhood of any world. To show completeness for these logics, we need to provide a compatible inconsistency relation, which – in contrast to the logics E and EM – will no longer be binary.

**Lemma 36.** Let $\vdash$ be the calculus $RES_{EN}$ (resp. $RES_{EMN}$) and let $C$ be a set of global clauses. Let $U = \{\neg\Box p \mid C \vdash G(p)\}$. Then the set $P \cup U$ is compatible inconsistency predicate for $\vdash$ and $C$, where $P$ is the inconsistency relation for the calculus $RES_E$ (resp. $RES_{EM}$).

*Proof.* The inconsistency requirement follows as the predicate closely resembles the modal rules of the calculus. To see cut closure, suppose that $\{\neg\Box p\}$ and $\{\neg\Box q, \Box p\} \in P \cup U$. Then the premisses that derive inconsistency of both sets can be combined to derive inconsistency of the cut $\{\neg\Box q\}$. For compatibility, we additionally need to consider the case $n = 0$ from Example 17, and extend the inductive proof of Lemma 18, where LNRES as last applied rule precisely induces this case.
The proof is very similar to that of classical modal logic (Lemma 15 and Lemma 18). The canonical model construction is an adaptation of the construction for E where the construction ensures that the set of neighbourhoods is upward closed.

**Definition 33.** Let $\mathcal{C}$ be a set of global clauses. The $\mathcal{C}$-canonical model for the calculus $\mathbf{RES}_{\mathbf{EM}}$ is the triple $(W, N, \theta)$ where $W$ and $\theta$ are the same as for classical modal logic (Definition 28) and the neighbourhood function $N$ is defined by

$$N(M) = \{\alpha \subseteq W \mid \theta(p) \subseteq \alpha \text{ for some } \Box p \in M\}.$$

where $M \in W$ is a maximally consistent, local extension of $\mathcal{C}$.

It is obvious that canonical models for $\mathbf{RES}_{\mathbf{EM}}$ are monotone by construction, but we need to re-establish the truth lemma for the calculus $\mathbf{RES}_{\mathbf{EM}}$ as the construction of the model has changed.

**Lemma 34 (Truth Lemma for EM).** For the calculus $\mathbf{RES}_{\mathbf{EM}}$, let $(W, N, \theta)$ be the $\mathcal{C}$-canonical model for some set $\mathcal{C}$ of global clauses. Then, for $M \in W$, $M \models \Gamma$ whenever $\Gamma \in M$, for all local clauses $\Gamma$.

The proof is in fact a simplification of the corresponding proof for classical modal logic, and we obtain completeness similar to Corollary 31.

**Corollary 35.** Monotone modal logic is complete, i.e. any consistent set $\mathcal{C}$ of local or global clauses satisfies $\mathcal{C} \vdash \epsilon$ whenever $\mathcal{C}$ is unsatisfiable in the class of monotone neighbourhood models.

## 4.2 Logics with Unit

We now adapt the construction to also incorporate logics with unit, i.e the modal logics EN and EMN that – in addition to the frame conditions for E and EM – additionally require that the entire set of worlds is always a neighbourhood of any world. To show completeness for these logics, we need to provide a compatible inconsistency relation, which – in contrast to the logics E and EM – will no longer be binary.

**Lemma 36.** Let $\vdash$ be the calculus $\mathbf{RES}_{\mathbf{EN}}$ (resp. $\mathbf{RES}_{\mathbf{EMN}}$) and let $\mathcal{C}$ be a set of global clauses. Let $U = \{\neg\Box p \mid \mathcal{C} \vdash G(p)\}$. Then the set $P \cup U$ is compatible inconsistency predicate for $\vdash$ and $\mathcal{C}$, where P is the inconsistency relation for the calculus $\mathbf{RES}_{\mathbf{E}}$ (resp. $\mathbf{RES}_{\mathbf{EM}}$).

*Proof.* The inconsistency requirement follows as the predicate closely resembles the modal rules of the calculus. To see cut closure, suppose that $\{\neg\Box p\}$ and $\{\neg\Box q, \Box p\} \in P \cup U$. Then the premisses that derive inconsistency of both sets can be combined to derive inconsistency of the cut $\{\neg\Box q\}$. For compatibility, we additionally need to consider the case $n = 0$ from Example 17, and extend the inductive proof of Lemma 18, where LNRES as last applied rule precisely induces this case.
This allows us to show completeness, again with a slight variation of the canonical model construction. The definition of the canonical model just adds the entire set of worlds to all neighbourhoods.

**Definition 37.** The canonical model for the logic **EN** and **EMN** is the triple $(W, N, \theta)$ where $W$ and $N$ are as for the logic **E** (or **EM**) and $N(w) = N_0(w) \cup \{W\}$, where $N_0$ is the neighbourhood function of the canonical model for the logic **E** (resp. **EM**).

The truth lemma follows as before, where we apply the rule LNRES to show inconsistency in case $W \in N(\theta)$.

**Lemma 38 (Truth Lemma for EN and EMN).** Let $(W, N, \theta)$ be the canonical model for the logic **EN** or **EMN**, respectively, over a set $C$ of global clauses. Then, for $M \in W$, $M \models \Gamma$ whenever $\Gamma \in M$, for all local clauses $\Gamma$.

*Proof.* In addition to the cases for **E** and **EM**, consider, for a contradiction, that $\neg \Box p \in M$ and $M \models \Box p$ where $\theta(p) = W$. In this case, $C \vdash G(p)$ whence $M \vdash \epsilon$, contradicting consistency of $M$ using LNRES.

Completeness for **EN** and **EMN** follows as before.

**Corollary 39.** The calculi $\mathbf{RES}_{\mathbf{EN}}$ and $\mathbf{RES}_{\mathbf{EMN}}$ are complete, i.e. $C \vdash \epsilon$ whenever $C$ is inconsistent, for any set $C$ of global clauses.

## 4.3 Logics with Aggregation

We now turn to completeness for logics that additionally satisfy aggregation, i.e. the axiom $C$ from Table 1. Our proof strategy is entirely similar to that of the previous cases, and we start with a compatible inconsistency relation. The format of the LCRES-rules is precisely chosen for the inconsistency relation below to be closed under cut which necessitates to generalise the $C$-axiom from binary conjunctions to arbitrary finite conjunctions.

**Lemma 40.** Let $P$ be the inconsistency relation for the calculi $\mathbf{RES}_{\mathbf{E}}$, $\mathbf{RES}_{\mathbf{EM}}$, $\mathbf{RES}_{\mathbf{EN}}$ or $\mathbf{RES}_{\mathbf{EMN}}$, and let

$$ U = \{ \neg \Box p_0, \Box p_1, \dots, \Box p_n \mid \begin{array}{l} C \vdash G(C_i) \text{ for } i = 0, \dots, n \text{ and clauses} \\ C_0 \subseteq \neg p_0 \lor p_1 \lor \dots \lor p_n, C_i \subseteq \neg p_0 \lor p_i \text{ for } i = 1, \dots, n \end{array} \} $$

Then $P \cup U$ is a compatible inconsistency relation for a set $C$ of global clauses and the calculus $\mathbf{RES}_{\mathbf{EC}}$, $\mathbf{RES}_{\mathbf{EMC}}$, $\mathbf{RES}_{\mathbf{ECN}}$ or $\mathbf{RES}_{\mathbf{EMCN}}$, respectively.

The proof is as before, noting that the inconsistency predicate is again modelled on the shape of the modal rules. The canonical model now takes the following form, where we distinguish between the different logics.
This allows us to show completeness, again with a slight variation of the canonical model construction. The definition of the canonical model just adds the entire set of worlds to all neighbourhoods.

**Definition 37.** The canonical model for the logic **EN** and **EMN** is the triple $(W, N, \theta)$ where $W$ and $N$ are as for the logic **E** (or **EM**) and $N(w) = N_0(w) \cup \{W\}$, where $N_0$ is the neighbourhood function of the canonical model for the logic **E** (resp. **EM**).

The truth lemma follows as before, where we apply the rule LNRES to show inconsistency in case $W \in N(\theta)$.

**Lemma 38 (Truth Lemma for EN and EMN).** Let $(W, N, \theta)$ be the canonical model for the logic **EN** or **EMN**, respectively, over a set $C$ of global clauses. Then, for $M \in W$, $M \models \Gamma$ whenever $\Gamma \in M$, for all local clauses $\Gamma$.

*Proof.* In addition to the cases for **E** and **EM**, consider, for a contradiction, that $\neg \Box p \in M$ and $M \models \Box p$ where $\theta(p) = W$. In this case, $C \vdash G(p)$ whence $M \vdash \epsilon$, contradicting consistency of $M$ using LNRES.

Completeness for **EN** and **EMN** follows as before.

**Corollary 39.** The calculi $\mathbf{RES}_{\mathbf{EN}}$ and $\mathbf{RES}_{\mathbf{EMN}}$ are complete, i.e. $C \vdash \epsilon$ whenever $C$ is inconsistent, for any set $C$ of global clauses.

## 4.3 Logics with Aggregation

We now turn to completeness for logics that additionally satisfy aggregation, i.e. the axiom $C$ from Table 1. Our proof strategy is entirely similar to that of the previous cases, and we start with a compatible inconsistency relation. The format of the LCRES-rules is precisely chosen for the inconsistency relation below to be closed under cut which necessitates to generalise the $C$-axiom from binary conjunctions to arbitrary finite conjunctions.

**Lemma 40.** Let $P$ be the inconsistency relation for the calculi $\mathbf{RES}_{\mathbf{E}}$, $\mathbf{RES}_{\mathbf{EM}}$, $\mathbf{RES}_{\mathbf{EN}}$ or $\mathbf{RES}_{\mathbf{EMN}}$, and let

$$ U = \{ \neg \Box p_0, \Box p_1, \dots, \Box p_n \mid \begin{array}{l} C \vdash G(C_i) \text{ for } i = 0, \dots, n \text{ and clauses} \\ C_0 \subseteq \neg p_0 \lor p_1 \lor \dots \lor p_n, C_i \subseteq \neg p_0 \lor p_i \text{ for } i = 1, \dots, n \end{array} \} $$

Then $P \cup U$ is a compatible inconsistency relation for a set $C$ of global clauses and the calculus $\mathbf{RES}_{\mathbf{EC}}$, $\mathbf{RES}_{\mathbf{EMC}}$, $\mathbf{RES}_{\mathbf{ECN}}$ or $\mathbf{RES}_{\mathbf{EMCN}}$, respectively.

The proof is as before, noting that the inconsistency predicate is again modelled on the shape of the modal rules. The canonical model now takes the following form, where we distinguish between the different logics.
**Definition 41.** Let $\mathcal{C}$ be a set of global clauses. The canonical model for $\mathcal{C}$ and the logics $\mathbf{EC}$, $\mathbf{ECN}$, $\mathbf{EMC}$ or $\mathbf{EMCN}$, respectively, is the triple $(W, N, \theta)$ where $W$ and $\theta$ are as before (Definition 28) and $N$ is given by

$$
\begin{align*}
N_{\mathbf{EC}}(M) &= \{\theta(p_1) \cap \dots \cap \theta(p_n) \mid \Box p_1, \dots, \Box p_n \in M\} && \text{for } \mathbf{EC} \\
N_{\mathbf{ECN}}(M) &= N_{\mathbf{EC}}(M) \cup W && \text{for } \mathbf{ECN} \\
N_{\mathbf{EMC}}(M) &= \{\alpha \subseteq W \mid \beta \subseteq \alpha \text{ for some } \beta \in N_{\mathbf{EC}}(M)\} && \text{for } \mathbf{EMC} \\
N_{\mathbf{EMCN}}(M) &= N_{\mathbf{EMC}}(M) \cup \{W\} && \text{for } \mathbf{EMCN}
\end{align*}
$$

for a maximally consistent local extension $M \in W$ of $\mathcal{C}$.

As before, we have a truth lemma that gives completeness.

**Lemma 42.** Let RES be one of RES<sub>EC</sub>, RES<sub>ECN</sub>, RES<sub>EMC</sub> or RES<sub>EMCN</sub>, let (W, N, θ) be the canonical model for RES, and let C be a set of global clauses. Then M |= D whenever D ∈ M, for all local clauses D and all maximally RES-consistent local extensions M of C.

*Proof.* The interesting case here is **EC** as the others are extensions of **EC** that we have previously discussed. Again, we just consider $\neg\Box p \in M$ and assume for a contradiction that $M \models \Box p$. Then there are $p_1, \dots, p_n$ such that $\theta(p) = \theta(p_1) \cap \dots \cap \theta(p_n)$ and $\Box p_1, \dots, \Box p_n \in M$. From the former we conclude the premiss of LCRES1 or LCRES2 depending on the sub-clauses we derive through Corollary 25 and arrive at a contradiction to the consistency of M.

Completeness now follows as in the other cases we have discussed before.

**Corollary 43 (Completeness).** The calculi RES<sub>EC</sub>, RES<sub>ECN</sub>, RES<sub>EMC</sub> and RES<sub>EMCN</sub> are complete with respect to the classes of models EC, ECN, EMC and EMCN, respectively.

# 5 Conclusion and Future Work

We have presented the first resolution calculi for the cube of classical non-normal modal logics. The calculi manipulate sets of modal clauses of a very simple form. Their completeness is based on the notion of inconsistency predicate. Moreover, we have seen that resolution calculi appear to be modular, i.e. rules can just be combined to obtain a stronger calculus. Is this a coincidence? Are there general principles that enable this compositionality? This is what we are going to explore in a follow up paper. Also, the shape of our calculi, i.e. the modal resolution rules, when compared to the Hilbert axioms, insinuate that there might be a more principled way of synthesising resolution systems from Hilbert axioms. We aim to investigate this as a next step.
**Definition 41.** Let $\mathcal{C}$ be a set of global clauses. The canonical model for $\mathcal{C}$ and the logics **EC**, **ECN**, **EMC** or **EMCN**, respectively, is the triple $(W, N, \theta)$ where $W$ and $\theta$ are as before (Definition 28) and $N$ is given by

$$
\begin{align*}
N_{\mathbf{EC}}(M) &= \{\theta(p_1) \cap \dots \cap \theta(p_n) \mid \Box p_1, \dots, \Box p_n \in M\} && \text{for } \mathbf{EC} \\
N_{\mathbf{ECN}}(M) &= N_{\mathbf{EC}}(M) \cup W && \text{for } \mathbf{ECN} \\
N_{\mathbf{EMC}}(M) &= \{\alpha \subseteq W \mid \beta \subseteq \alpha \text{ for some } \beta \in N_{\mathbf{EC}}(M)\} && \text{for } \mathbf{EMC} \\
N_{\mathbf{EMCN}}(M) &= N_{\mathbf{EMC}}(M) \cup \{W\} && \text{for } \mathbf{EMCN}
\end{align*}
$$

for a maximally consistent local extension $M \in W$ of $\mathcal{C}$.

As before, we have a truth lemma that gives completeness.

**Lemma 42.** Let RES be one of RES<sub>EC</sub>, RES<sub>ECN</sub>, RES<sub>EMC</sub> or RES<sub>EMCN</sub>, let (W, N, θ) be the canonical model for RES, and let C be a set of global clauses. Then M |= D whenever D ∈ M, for all local clauses D and all maximally RES-consistent local extensions M of C.

*Proof.* The interesting case here is **EC** as the others are extensions of **EC** that we have previously discussed. Again, we just consider $\neg\Box p \in M$ and assume for a contradiction that $M \models \Box p$. Then there are $p_1, \dots, p_n$ such that $\theta(p) = \theta(p_1) \cap \dots \cap \theta(p_n)$ and $\Box p_1, \dots, \Box p_n \in M$. From the former we conclude the premiss of LCRES1 or LCRES2 depending on the sub-clauses we derive through Corollary 25 and arrive at a contradiction to the consistency of M.

Completeness now follows as in the other cases we have discussed before.

**Corollary 43 (Completeness).** The calculi RES<sub>EC</sub>, RES<sub>ECN</sub>, RES<sub>EMC</sub> and RES<sub>EMCN</sub> are complete with respect to the classes of models EC, ECN, EMC and EMCN, respectively.

# 5 Conclusion and Future Work

We have presented the first resolution calculi for the cube of classical non-normal modal logics. The calculi manipulate sets of modal clauses of a very simple form. Their completeness is based on the notion of inconsistency predicate. Moreover, we have seen that resolution calculi appear to be modular, i.e. rules can just be combined to obtain a stronger calculus. Is this a coincidence? Are there general principles that enable this compositionality? This is what we are going to explore in a follow up paper. Also, the shape of our calculi, i.e. the modal resolution rules, when compared to the Hilbert axioms, insinuate that there might be a more principled way of synthesising resolution systems from Hilbert axioms. We aim to investigate this as a next step.
References

1. Abadi, M., Manna, Z.: Modal Theorem Proving. In: J.H.Siekmann (ed.) Proc. CADE-8. Lecture Notes in Computer Science, vol. 230, pp. 172–189. Springer (1986)

2. Areces, C., de Nivelle, H., de Rijke, M.: Prefixed Resolution: A Resolution Method for Modal and Description Logics. In: Ganzinger, H. (ed.) Proc. CADE-16. Lecture Notes in Computer Science, vol. 1632, pp. 187–201. Springer (1999)

3. Auffray, Y.: Linear Strategy for Propositional Modal Resolution. Information Processing Letters 28(2), 87–92 (1988)

4. del Cerro, L.F.: Resolution Modal Logics. In: Proceedings of Advanced NATO Study Institute on Logics and Models for Verification and Specification of Concurrent Systems. pp. 46–78. La Colle-sur-Loup, France (Oct 1984)

5. del Cerro, L.F.: A Simple Deduction Method for Modal Logic. Information Processing Letters 14(2), 49–51 (1982)

6. Chan, M.C.: The Recursive Resolution Method for Modal Logic. New Generation Computing 5, 155–183 (1987)

7. Chellas, B.F.: Modal Logic. Cambridge (1980)

8. Cialdea, M.: Resolution for some First-Order Modal Systems. Theoretical Computer Science 85, 213–229 (1991)

9. Dalmonte, T., Lellmann, B., Olivetti, N., Pimentel, E.: Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity. Journal of Logic and Computation 31(1), 67–111 (2021)

10. Dalmonte, T., Olivetti, N., Negri, S.: Non-normal modal logics: Bi-neighbourhood semantics and its labelled calculi. In: Bezhanishvili, G., D'Agostino, G., Metcalfe, G., Studer, T. (eds.) Proc. AiML 2018 (2018)

11. Duarte, A., Korovin, K.: Implementing superposition in iprover (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Proc. IJCAR 2020. Lecture Notes in Computer Science, vol. 12167, pp. 388–397. Springer (2020)

12. Elgesem, D.: The modal logic of agency. Nordic Journal of Philosophical Logic 2, 1–46 (1997)

13. Enjalbert, P., del Cerro, L.F.: Modal Resolution in Clausal Form. Theoretical Computer Science 65, 1–33 (1989)

14. Fitting, M.C.: Destructive Modal Resolution. CUNY Technical Report (August 1989)

15. Gilbert, D.R., Maffezioli, P.: Modular sequent calculi for classical modal logics. Studia Logica 103(1), 175–217 (2015)

16. Giunchiglia, E., Tacchella, A., Giunchiglia, F.: SAT-based decision procedures for classical modal logics. Journal of Automated Reasoning 28(2), 143–171 (2002)

17. Gleißner, T., Steen, A.: Leo-III (2022), https://doi.org/10.5281/zenodo.4435994, retrieved July 24, 2023

18. Goré, R., Kikkert, C.: Cegar-tableaux: Improved modal satisfiability via modal clause-learning and sat. In: Das, A., Negri, S. (eds.) Proc. TABLEAUX 2021. Lecture Notes in Computer Science, vol. 12842, pp. 74–91. Springer (2021)

19. Goré, R., Olesen, K., Thomson, J.: Implementing tableau calculi using BDDs: BDDTab system description. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Proc. IJCAR 2014. Lecture Notes in Computer Science, vol. 8562, pp. 337–343. Springer (2014)

20. Götzmann, D., Kaminski, M., Smolka, G.: Spartacus: A tableau prover for hybrid logic. Electron. Notes Theor. Comput. Sci 262 (2010)
References

1. Abadi, M., Manna, Z.: Modal Theorem Proving. In: J.H.Siekmann (ed.) Proc. CADE-8. Lecture Notes in Computer Science, vol. 230, pp. 172–189. Springer (1986)

2. Areces, C., de Nivelle, H., de Rijke, M.: Prefixed Resolution: A Resolution Method for Modal and Description Logics. In: Ganzinger, H. (ed.) Proc. CADE-16. Lecture Notes in Computer Science, vol. 1632, pp. 187–201. Springer (1999)

3. Auffray, Y.: Linear Strategy for Propositional Modal Resolution. Information Processing Letters 28(2), 87–92 (1988)

4. del Cerro, L.F.: Resolution Modal Logics. In: Proceedings of Advanced NATO Study Institute on Logics and Models for Verification and Specification of Concurrent Systems. pp. 46–78. La Colle-sur-Loup, France (Oct 1984)

5. del Cerro, L.F.: A Simple Deduction Method for Modal Logic. Information Processing Letters 14(2), 49–51 (1982)

6. Chan, M.C.: The Recursive Resolution Method for Modal Logic. New Generation Computing 5, 155–183 (1987)

7. Chellas, B.F.: Modal Logic. Cambridge (1980)

8. Cialdea, M.: Resolution for some First-Order Modal Systems. Theoretical Computer Science 85, 213–229 (1991)

9. Dalmonte, T., Lellmann, B., Olivetti, N., Pimentel, E.: Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity. Journal of Logic and Computation 31(1), 67–111 (2021)

10. Dalmonte, T., Olivetti, N., Negri, S.: Non-normal modal logics: Bi-neighbourhood semantics and its labelled calculi. In: Bezhanishvili, G., D'Agostino, G., Metcalfe, G., Studer, T. (eds.) Proc. AiML 2018 (2018)

11. Duarte, A., Korovin, K.: Implementing superposition in iprover (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Proc. IJCAR 2020. Lecture Notes in Computer Science, vol. 12167, pp. 388–397. Springer (2020)

12. Elgesem, D.: The modal logic of agency. Nordic Journal of Philosophical Logic 2, 1–46 (1997)

13. Enjalbert, P., del Cerro, L.F.: Modal Resolution in Clausal Form. Theoretical Computer Science 65, 1–33 (1989)

14. Fitting, M.C.: Destructive Modal Resolution. CUNY Technical Report (August 1989)

15. Gilbert, D.R., Maffezioli, P.: Modular sequent calculi for classical modal logics. Studia Logica 103(1), 175–217 (2015)

16. Giunchiglia, E., Tacchella, A., Giunchiglia, F.: SAT-based decision procedures for classical modal logics. Journal of Automated Reasoning 28(2), 143–171 (2002)

17. Gleißner, T., Steen, A.: Leo-III (2022), https://doi.org/10.5281/zenodo.4435994, retrieved July 24, 2023

18. Goré, R., Kikkert, C.: Cegar-tableaux: Improved modal satisfiability via modal clause-learning and sat. In: Das, A., Negri, S. (eds.) Proc. TABLEAUX 2021. Lecture Notes in Computer Science, vol. 12842, pp. 74–91. Springer (2021)

19. Goré, R., Olesen, K., Thomson, J.: Implementing tableau calculi using BDDs: BDDTab system description. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Proc. IJCAR 2014. Lecture Notes in Computer Science, vol. 8562, pp. 337–343. Springer (2014)

20. Götzmann, D., Kaminski, M., Smolka, G.: Spartacus: A tableau prover for hybrid logic. Electron. Notes Theor. Comput. Sci 262 (2010)
21. Haken, A.: The intractability of resolution. Theoretical Computer Science 39(2-3), 297-308 (1985)

22. Indrzejczak, A.: Sequent calculi for monotonic modal logics. Bulletin of the Section of logic 34(3), 151-164 (2005)

23. Indrzejczak, A.: Admissibility of cut in congruent modal logics. Logic and Logical Philosophy 21, 189-203 (2011)

24. Kaminski, M., Tebbi, T.: InKreSAT: Modal reasoning via incremental reduction to SAT. In: Bonacina, M.P. (ed.) Proc. CADE-24. pp. 436-442. Lecture Notes in Artificial Intelligence (2013)

25. Lavendhomme, R., Lucas, T.: Sequent calculi and decision procedures for weak modal systems. Studia Logica 65, 121-145 (2000)

26. Lellmann, B., Pimentel, E.: Modularisation of sequent calculi for normal and non-normal modalities. ACM Transactions on Computational Logic 20(2), 7:1-7:46 (2019)

27. McCune, W.W.: OTTER Users' Guide, Version 3.3 (2003), Argonne National Laboratory

28. McCune, W.W.: Prover9 and mace4 (2010), http://www.cs.unm.edu/~mccune/prover9/, retrieved July 24, 2023

29. Mints, G.: Gentzen-Type Systems and Resolution Rules, Part 1: Propositional Logic. In: Proc. COLOG 1988. Lecture Notes in Computer Science, vol. 417, pp. 198-231. Springer (1990)

30. Nalon, C., Dixon, C.: Clausal resolution for normal modal logics. Journal of Algorithms 62, 117-134 (2007)

31. Nalon, C., Dixon, C., Hustadt, U.: Modal resolution: Proofs, layers, and refinements. ACM Transactions on Computational Logic 20(4), 23:1-23:38 (2019)

32. Nalon, C., Hustadt, U., Dixon, C.: KSP: A resolution-based prover for multimodal K. In: Olivetti, N., Tiwari, A. (eds.) Proc. IJCAR 2016. pp. 406-415. Springer (2016)

33. Nalon, C., Hustadt, U., Dixon, C.: KSP: A resolution-based prover for multimodal K, abridged report. In: Sierra, C. (ed.) Proc. IJCAI 2017. pp. 4919-4923. IJCAI/AAAI Press (2017)

34. Nalon, C., Hustadt, U., Dixon, C.: KSP a resolution-based theorem prover for K<sub>n</sub>: Architecture, refinements, strategies and experiments. Journal of Automated Reasoning 64(3), 461-484 (2020)

35. Nalon, C., Hustadt, U., Papacchini, F., Dixon, C.: Local reductions for the modal cube. In: Proc. IJCAR 2022 (2022)

36. Nalon, C., Marcos, J., Dixon, C.: Clausal resolution for modal logics of confluence. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Proc. IJCAR 2014, Lecture Notes in Computer Science, vol. 8562, pp. 322-336. Springer (2014)

37. Negri, S.: Proof theory for non-normal modal logics: The neighbourhood formalism and basic results. IfCoLog Journal of Applied Logics 4(4), 1241-1286 (2017)

38. de Nivelle, H., Schmidt, R.A., Hustadt, U.: Resolution-Based Methods for Modal Logics. Logic Journal of the IGPL 8(3), 265-292 (2000)

39. Ohlbach, H.J.: Semantics-Based Translation Methods for Modal Logics. Journal of Logic and Computation 1(5), 691-746 (1990)

40. Ohlbach, H.J., Schmidt, R.A., Hustadt, U.: Translating Graded Modalities into Predicate Logics. In: Wansing, H. (ed.) Proof Theory of Modal Logic, Applied Logic Series, vol. 2, pp. 253-291. Kluwer Academic Publishers (1996)

41. Orlandelli, E.: Proof analysis in deontic logics. In: Cariani, F., Grossi, D., Meheus, J., Parent, X. (eds.) Proc. DEON 2014. Lecture Notes in Computer Science, vol. 8554, pp. 139-148. Springer (2014)
21. Haken, A.: The intractability of resolution. Theoretical Computer Science 39(2-3), 297-308 (1985)

22. Indrzejczak, A.: Sequent calculi for monotonic modal logics. Bulletin of the Section of logic 34(3), 151-164 (2005)

23. Indrzejczak, A.: Admissibility of cut in congruent modal logics. Logic and Logical Philosophy 21, 189-203 (2011)

24. Kaminski, M., Tebbi, T.: InKreSAT: Modal reasoning via incremental reduction to SAT. In: Bonacina, M.P. (ed.) Proc. CADE-24. pp. 436-442. Lecture Notes in Artificial Intelligence (2013)

25. Lavendhomme, R., Lucas, T.: Sequent calculi and decision procedures for weak modal systems. Studia Logica 65, 121-145 (2000)

26. Lellmann, B., Pimentel, E.: Modularisation of sequent calculi for normal and non-normal modalities. ACM Transactions on Computational Logic 20(2), 7:1-7:46 (2019)

27. McCune, W.W.: OTTER Users' Guide, Version 3.3 (2003), Argonne National Laboratory

28. McCune, W.W.: Prover9 and mace4 (2010), http://www.cs.unm.edu/~mccune/prover9/, retrieved July 24, 2023

29. Mints, G.: Gentzen-Type Systems and Resolution Rules, Part 1: Propositional Logic. In: Proc. COLOG 1988. Lecture Notes in Computer Science, vol. 417, pp. 198-231. Springer (1990)

30. Nalon, C., Dixon, C.: Clausal resolution for normal modal logics. Journal of Algorithms 62, 117-134 (2007)

31. Nalon, C., Dixon, C., Hustadt, U.: Modal resolution: Proofs, layers, and refinements. ACM Transactions on Computational Logic 20(4), 23:1-23:38 (2019)

32. Nalon, C., Hustadt, U., Dixon, C.: KSP: A resolution-based prover for multimodal K. In: Olivetti, N., Tiwari, A. (eds.) Proc. IJCAR 2016. pp. 406-415. Springer (2016)

33. Nalon, C., Hustadt, U., Dixon, C.: KSP: A resolution-based prover for multimodal K, abridged report. In: Sierra, C. (ed.) Proc. IJCAI 2017. pp. 4919-4923. IJCAI/AAAI Press (2017)

34. Nalon, C., Hustadt, U., Dixon, C.: KSP a resolution-based theorem prover for K<sub>n</sub>: Architecture, refinements, strategies and experiments. Journal of Automated Reasoning 64(3), 461-484 (2020)

35. Nalon, C., Hustadt, U., Papacchini, F., Dixon, C.: Local reductions for the modal cube. In: Proc. IJCAR 2022 (2022)

36. Nalon, C., Marcos, J., Dixon, C.: Clausal resolution for modal logics of confluence. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Proc. IJCAR 2014, Lecture Notes in Computer Science, vol. 8562, pp. 322-336. Springer (2014)

37. Negri, S.: Proof theory for non-normal modal logics: The neighbourhood formalism and basic results. IfCoLog Journal of Applied Logics 4(4), 1241-1286 (2017)

38. de Nivelle, H., Schmidt, R.A., Hustadt, U.: Resolution-Based Methods for Modal Logics. Logic Journal of the IGPL 8(3), 265-292 (2000)

39. Ohlbach, H.J.: Semantics-Based Translation Methods for Modal Logics. Journal of Logic and Computation 1(5), 691-746 (1990)

40. Ohlbach, H.J., Schmidt, R.A., Hustadt, U.: Translating Graded Modalities into Predicate Logics. In: Wansing, H. (ed.) Proof Theory of Modal Logic, Applied Logic Series, vol. 2, pp. 253-291. Kluwer Academic Publishers (1996)

41. Orlandelli, E.: Proof analysis in deontic logics. In: Cariani, F., Grossi, D., Meheus, J., Parent, X. (eds.) Proc. DEON 2014. Lecture Notes in Computer Science, vol. 8554, pp. 139-148. Springer (2014)
42. Orlandelli, E.: Sequent calculi and interpolation for non-normal modal and deontic logics. Logic and Logical Philosophy **30**(1), 139–183 (2020)

43. Pacuit, E.: Neighborhood Semantics for Modal Logic. Springer (2017)

44. Papacchini, F., Nalon, C., Hustadt, U., Dixon, C.: Efficient local reductions to basic modal logic. In: Platzer, A., Sutcliffe, G. (eds.) Proc. CADE 28. Lecture Notes in Computer Science, vol. 12699, pp. 76–92. Springer (2021)

45. Plaisted, D.A., Greenbaum, S.A.: A Structure-Preserving Clause Form Translation. Journal of Logic and Computation **2**, 293–304 (1986)

46. Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. The Journal of the ACM **12**(1), 23–41 (Jan 1965)

47. Schulz, S.: E 2.6 (2022), http://wwwlehre.dhbw-stuttgart.de/~sschulz/E/Download.html, retrieved July 24, 2023

48. Sutcliff, G. (ed.): Proceedings of the 11th IJCAR ATP System Competition (CASC-J11) (2022), https://www.tptp.org/CASC/J11/, retrieved July 24, 2023

49. The SPASS Team: Spass 3.9 (2016), http://www.spass-prover.org/ retrieved July 24, 2023

50. The Vampire Team: Vampire 4.7 (2022), https://github.com/vprover/vampire/releases, retrieved July 24, 2023

51. Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description. In: Furbach, U., Shankar, N. (eds.) Proc. IJCAR 2006. pp. 292–297. Lecture Notes in Computer Science (2006)

52. Vardi, M.Y.: On the complexity of epistemic reasoning. In: Proc. LICS 1989. pp. 243–252. IEEE Computer Society (1989)
42. Orlandelli, E.: Sequent calculi and interpolation for non-normal modal and deontic logics. Logic and Logical Philosophy **30**(1), 139–183 (2020)

43. Pacuit, E.: Neighborhood Semantics for Modal Logic. Springer (2017)

44. Papacchini, F., Nalon, C., Hustadt, U., Dixon, C.: Efficient local reductions to basic modal logic. In: Platzer, A., Sutcliffe, G. (eds.) Proc. CADE 28. Lecture Notes in Computer Science, vol. 12699, pp. 76–92. Springer (2021)

45. Plaisted, D.A., Greenbaum, S.A.: A Structure-Preserving Clause Form Translation. Journal of Logic and Computation **2**, 293–304 (1986)

46. Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. The Journal of the ACM **12**(1), 23–41 (Jan 1965)

47. Schulz, S.: E 2.6 (2022), http://wwwlehre.dhbw-stuttgart.de/~sschulz/E/Download.html, retrieved July 24, 2023

48. Sutcliff, G. (ed.): Proceedings of the 11th IJCAR ATP System Competition (CASC-J11) (2022), https://www.tptp.org/CASC/J11/, retrieved July 24, 2023

49. The SPASS Team: Spass 3.9 (2016), http://www.spass-prover.org/ retrieved July 24, 2023

50. The Vampire Team: Vampire 4.7 (2022), https://github.com/vprover/vampire/releases, retrieved July 24, 2023

51. Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description. In: Furbach, U., Shankar, N. (eds.) Proc. IJCAR 2006. pp. 292–297. Lecture Notes in Computer Science (2006)

52. Vardi, M.Y.: On the complexity of epistemic reasoning. In: Proc. LICS 1989. pp. 243–252. IEEE Computer Society (1989)