Non-normal modal logics, interpreted on neighbourhood models which generalise the usual relational semantics, have found application in several areas, such as epistemic, deontic, and coalitional reasoning. We present here preliminary results on reasoning in a family of modal description logics obtained by combining ALC with non-normal modal operators. First, we provide a framework of terminating, correct, and complete tableau algorithms to check satisfiability of formulas in such logics with the semantics based on varying domains. We then investigate the satisfiability problems in fragments of these languages obtained by restricting the application of modal operators to formulas only, and interpreted on models with constant domains, providing tight complexity results.
Contexts involving epistemic and doxastic [
The semantics of modal operators is usually given in terms of relational models, based on
frames consisting of a set of possible worlds equipped with suitable accessibility relations.
However, all the modal systems interpreted by means of this kind of semantics, known as
normal, validate principles that have been considered problematic or debatable for the
aforementioned applications, leading to counterintuitive or unacceptable conclusions. Among the
unpleasant features discussed in the literature, one encounters for instance the problem of
logical omniscience [
To avoid the unwanted consequences of the relational semantics, several non-normal modal
logics have been proposed and studied, tracing back to the seminal works by C.I. Lewis [
Non-normal modalities have been widely investigated as a way to extend propositional
logic. A further line of research focuses on the behaviour of modal operators interpreted on
neighbourhood frames in combination with first-order logic. In this direction, a few works have
provided completeness results for first-order non-normal modal logics [
In this paper, we investigate satisfiability of non-normal modal extensions of description logics. In particular, we study the logics characterised by the class of all neighbourhood frames (E), supplemented neighbourhood frames (M), neighbourhood frames closed under intersection (C), and neighbourhood frames containing the unit (N), and combine them with the prototypical ALC description logic. We provide a framework of terminating, correct, and complete tableau algorithms to check satisfiability in such logics interpreted in neighbourhood models with varying domains (in this kind of semantics, the domains of the interpretations at each world can differ; cf. Section 2 for details). We then investigate the satisfiability problems in fragments of these languages obtained by restricting the application of modal operators to formulas only, and provide complexity upper bounds with constant domains (in this case the domains of the interpretations at every world are the same). We leave satisfiability checking procedures for non-restricted languages interpreted on models with constant domain as open problems.
Full proof details are provided in an extended version of this paper [
In this section, we provide preliminary definitions for non-normal modal description logics, first introducing their syntax, and then giving their semantics based on neighbourhood models. Syntax Let NC and NR be countably infinite and pairwise disjoint sets of concept names and role names respectively. An MLnALC concept is an expression of the form
C ::= A | ¬C | C ⊓ C | ∃r.C | 2iC, where A ∈ NC, r ∈ NR, and 2i, with i ∈ I = {1, . . . , n}, are modal operators called boxes. A concept inclusion (CI ) is an expression of the form C ⊑ D, where C, D are MLnALC concepts. An MLnALC formula takes the form ϕ ::= C ⊑ D | ¬ϕ | ϕ ∧ ϕ | 2iϕ, where i ∈ I. We will use the following standard definitions for concepts: ⊥ := A ⊓ ¬A, ⊤ := ¬⊥; ∀r.C := ¬∃r.¬C; (C ⊔ D) := ¬(¬C ⊓ ¬D); ◇iC := ¬2i¬C (operators ◇i are called diamonds). Concepts of the form 2iC, ◇iC are called modalised concepts. Analogous conventions also hold for formulas, for which we set true := (⊥ ⊑ ⊤).
Semantics A neighbourhood frame, or simply frame, is a pair F = (W, {Ni}i∈I ), where W is a non-empty set of worlds and, for each i ∈ I = {1, . . . , n}, Ni : W → 22W is called a neighbourhood function. A frame is: supplemented if, for all i ∈ I, w ∈ W, α, β ⊆ W, α ∈ Ni(w) and α ⊆ β implies β ∈ Ni(w); closed under intersection if, for all i ∈ I, w ∈ W, α, β ⊆ W, α ∈ Ni(w) and β ∈ Ni(w) implies α ∩ β ∈ Ni(w); and contains the unit if, for all i ∈ I, w ∈ W, W ∈ Ni(w). An MLnALC varying domain neighbourhood model, or simply model, based on a neighbourhood frame F is a pair M = (F , I), where F = (W, {Ni}i∈I ) is a neighbourhood frame and I is a function associating with every w ∈ W an ALC interpretation Iw = (Δw, ·Iw ), with non-empty domain Δw, and where ·Iw is a function such that: for all A ∈ NC, AIw ⊆ Δw; for all r ∈ NR, rIw ⊆ Δw×Δw. An MLnALC constant domain neighbourhood model is defined in the same way, except that, for all w, w′ ∈ W, we have that Δw = Δw′ . Given a model M = (F , I) and a world w ∈ W of F (or simply w in F ), the interpretation CIw of a concept C in w is defined as:
(¬D)Iw = Δw \ DIw , (D ⊓ E)Iw = DIw ∩ EIw , (∃r.D)Iw = {d ∈ Δw | ∃e ∈ DIw : (d, e) ∈ rIw }, (2iD)Iw = {d ∈ Δw | JDKdM ∈ Ni(w)}, where, for all d ∈ Sw∈W Δw, the set JDKdM = {v ∈ W | d ∈ DIv } is called the truth set of D with respect to d. We say that a concept C is satisfied in M if there is w in F such that CIw 6= ∅, and that C is satisfiable (over varying or constant neighbourhood models, respectively) if there is a (varying or constant domain, respectively) neighbourhood model in which it is satisfied. The satisfaction of an MLnALC formula ϕ in w of M, written M, w |= ϕ, is defined as follows: M, w |= C ⊑ D iff
M, w |= ¬ψ iff M, w |= ψ ∧ χ iff
CIw ⊆ DIw , M, w 6|= ψ,
M, w |= ψ and M, w |= χ, M, w |= 2iψ iff
JψKM ∈ Ni(w), where JψKM = {v ∈ W | M, v |= ψ} is the truth set of ψ. As a consequence of the above definition, we obtain the following condition for diamond formulas: M, w |= ◇iψ iff J¬ψKM ∈/ Ni(w). Given a neighbourhood frame F = (W, {Ni}i∈I ) and a neighbourhood model M = (F , I), we say that ϕ is satisfied in M if there is w ∈ W such that M, w |= ϕ, and that ϕ is satisfiable (over varying or constant domain neighbourhood models, respectively) if it is satisfied in some (varying or constant domain, respectively) neighbourhood model.
Given a class of frames C, by the MLnALC formula satisfiability problem on (varying or constant domain, respectively) neighbourhood models based on a frame in C we mean the problem of deciding whether an MLnALC formula is satisfied in a (varying or constant domain, respectively) neighbourhood model based on a frame in C. In the following, let Log = {E, M, C, N}. Given L ∈ Log, the LnALC formula satisfiability problem on (varying or constant domain, respectively) neighbourhood models is the MLnALC formula satisfiability problem on (varying or constant domain, respectively) neighbourhood models based on a frame in the class of: • all neighbourhood frames, for L = E; • supplemented neighbourhood frames, for L = M; • neighbourhood frames closed under intersection, for L = C; and • neighbourhood frames containing the unit, for L = N. 3. Tableaux for Non-normal Modal Description Logics In this section, we provide terminating, sound and complete tableau algorithms to check satisfiability of formulas in varying domain neighbourhood models. The notation partly adheres to that of Gabbay et al. [28], while the model construction in the soundness proof is based on the strategy of Dalmonte et al. [29].
We require the following preliminary notions. For a concept or formula γ, we denote by ¬˙ γ the negation of γ put in negation normal form (NNF ), defined as usual. Given an MLnALC formula ϕ, we assume without loss of generality that ϕ is in NNF, it contains CIs only of the form ⊤ ⊑ C, and every concept occurring in ϕ is also in NNF. We define the weight |C| of a concept C in NNF as follows: |A| = |¬A| = 0; |∃r.D| = |∀r.D| = |◇iD| = |2iD| = |D| + 1; |D ⊓ E| = |D ⊔ E| = |D| + |E| + 1. The weight |ϕ| of a formula ϕ in NNF is defined as: |(C ⊑ D)| = |¬(C ⊑ D)| = 0; 2iψ = |ψ| + 1; |ψ ∧ χ| = |ψ ∨ χ| = |ψ| + |χ| + 1. Observe that, for a concept or formula γ, we have that |γ| = | ¬˙γ|. We denote by con(ϕ) and for(ϕ) the set of subconcepts and subformulas of ϕ, respectively, and then we set con¬˙ (ϕ) = con(ϕ) ∪ { ¬˙C | C ∈ con(ϕ)} and for ¬˙(ϕ) = for(ϕ) ∪ {¬˙ ψ | ψ ∈ for(ϕ)}. The set rol(ϕ) is the set of role names occurring in ϕ. Let Fg(ϕ) = for¬˙ (ϕ) ∪ con¬˙ (ϕ) ∪ rol(ϕ). Note that, by our assumption on the form of CIs in ϕ, we have ⊤ ∈ con ¬˙(ϕ).
Moreover, let NV be a countable set of variables, well-ordered by the relation <, and let NL be a countable set of labels. Given an MLnALC formula ϕ, an n-labelled constraint for ϕ takes the form n : ψ, or n : C(x), or n : r(x, y), where n ∈ NL, ψ ∈ for¬˙ (ϕ), x, y ∈ NV, C ∈ con¬˙ (ϕ), and r ∈ rol(ϕ). An n-labelled constraint system for ϕ is a set Sn of n-labelled constraints for ϕ. (A labelled constraint for ϕ is an n-labelled constraint for ϕ, for some n ∈ NL, and similarly for a labelled constraint system for ϕ). A completion set T is a non-empty union of labelled constraint systems for ϕ, and we set LT = {n ∈ NL | Sn ∈ T}.
Concerning variables, we adopt the following terminology. A variable x occurs in Sn if Sn contains n-labelled constraints of the form n : C(x) or n : r(τ, τ ′), where τ = x, or τ ′ = x, and n ∈ NL. In addition, x is said to be fresh for Sn if x does not occur in Sn and x > y, for every y that occurs in S. (These notions can be used with respect to T, whenever Sn ⊆ T). Without loss of generality, we assume that, whenever x occurs in Sn, the n-labelled constraint n : ⊤(x) is in Sn . Also, if n : r(x, y) ∈ Sn, we call y an r-successor of x with respect to Sn. Finally, given variables x, y in an n-labelled constraint system Sn, we say that x is blocked by y in Sn if x > y and {C | n : C(x) ∈ Sn} ⊆ {C | n : C(y) ∈ Sn}.
A completion set T contains a clash if {m : ψ, m : ¬ψ} ⊆ T, or {m : C(x), m : ¬C(x)} ⊆ T, for some m ∈ NL, and formula ψ or concept C. A completion set with no clash is clash-free. Given L ∈ Log, a completion set is LnALC-complete if no LnALC-rule from Figure 1 is applicable to T, where γj is either ψj ∈ for¬˙ (ϕ) or Cj (xj ), with Cj ∈ con¬˙ (ϕ), for j = 1, . . . , k, and δ is either χ ∈ for¬˙ (ϕ) or D(y), with D ∈ con¬˙ (ϕ), with respect to the following application conditions associated to each LnALC-rule: (R∧) {n : ψ, n : χ} 6⊆ T; (R∨) {n : ψ, n : χ} ∩ T = ∅; (R⊓) {n : C(x), n : D(x)} 6⊆ T; (R⊔) {n : C(x), n : D(x)} ∩ T = ∅; (R∃) x is not blocked by any variable in Sn, there is no z such that {n : r(x, z), n : C(z)} ⊆ T, and y is the <-minimal variable fresh for Sn; (R∀) n : C(y) ∈/ T; (R=) x occurs in an n-labelled constraint in T and n : C(x) ∈/ T; (R6=) x is the <-minimal variable fresh for Sn, and there is no y such that n : ¬˙C(y) ∈ T; (RL) m is fresh for T, and there is no o ∈ NL such that {o : γ1, . . . , o : γk, o : δ} ⊆ T, or {o : ¬˙ γj , o : ¬˙ δ} ⊆ T, for some j ≤ l, where k and l are as in Figure 1.
The LnALC-rules essentially state how to extend a completion set on the basis of the information contained in it. Branching rules entail a non-deterministic choice in the expansion of the completion set. For each L ∈ Log, we now define an algorithm based on LnALC-rules for checking the LnALC formula satisfiability. We then prove that the algorithm terminates for every formula ϕ, and that it is sound and complete with respect to LnALC satisfiability. Definition 1 (LnALC tableau algorithm for ϕ). Given an MLnALC formula ϕ, the LnALC tableau algorithm for ϕ runs as follows: set the initial completion set Tϕ = {0 : ϕ, 0 : ⊤(x)}, and expand it by means of the LnALC-rules until a clash or an LnALC-complete completion set is obtained.
In the rest of this section, we prove termination, soundness and completeness of the tableau algorithms given above. We start by showing that the LnALC tableau algorithm terminates. Theorem 1 (Termination). Having started on the initial completion set Tϕ = {0 : ϕ, 0 : ⊤(x)}, the LnALC tableau algorithm for ϕ terminates after at most 2p(|Fg(ϕ)|) steps, where p is a polynomial function.
Proof. We first require the following claims.
Claim 1.1. Let T be a completion set obtained by applying the LnALC tableau algorithm for ϕ. For each n ∈ LT, the number of n-labelled constraints for ϕ in T does not exceed 2q(|Fg(ϕ)|), where q is a polynomial function. n : ψ ∧ χ n : ψ , n : χ (R⊓) n : C ⊓ D(x) n : C(x) , n : D(x) (R∨)
n : ψ ∨ χ (R∃) (R=) n : ψ n : χ n : ∃r.C(x) n : r(x, y) , n : C(y) n : ∀r.C(x) , n : r(x, y) n : C(y) n : ⊤ ⊑ C n : C(x) n : ¬(⊤ ⊑ C) n : ¬˙C(x) n : C(x) n : D(x) (R⊔)
n : C ⊔ D(x) (R∀) (R6=) m : γ1, . . . , m : γk, m : δ (0) m : ¬˙γ1, m : ¬˙δ . .
. m : ¬˙γk, m : ¬˙δ (1) (l) (RL)
n : 2iγ1, . . . , n : 2iγk, n : ◇iδ Proof of Claim. We remark that, for each Sn ⊆ T, the LnALC tableaux algorithm behaves exactly like a standard (non-modal) ALC tableaux algorithm (cf. e.g. [28, Theorem 15.4], noting also that in our case we do not have to deal with individual names).
Claim 1.2. Let T be a completion set obtained by applying the LnALC tableau algorithm for ϕ. For L ∈ {E, M, N}, |LT| ≤ |Fg(ϕ)|2. For L = C, |LT| ≤ 2|Fg(ϕ)| · |Fg(ϕ)|.
Proof of Claim. Labels n are generated in T by means of the application of the rule RL. For L ∈ {E, M, N}, this rule is applied to two n-labelled contraints n : 2iγ, n : ◇iδ (for L = N possibly also to a single constraint n : ◇iδ), while for L = C it is applied to k + 1 n-labelled contraints n : 2iγ1, ...n : 2iγk, n : ◇iδ. By the application condition of RL, each such combination of constraints generates at most one label m. Therefore, the number of labels that can be generated in T is bounded by the number of possible such combinations, which is at most |Fg(ϕ)|2, for L ∈ {E, M, N}, and at most 2|Fg(ϕ)| · |Fg(ϕ)|, for L = C.
The theorem is then a consequence of the following observations. Given a completion set T constructed by the LnALC tableau algorithm, we have by Claim 1.2 that the number of applications of rule RL is bounded by |LT|, which is at most |Fg(ϕ)|2, for L ∈ {E, M, N}, and at most 2|Fg(ϕ)| · |Fg(ϕ)|, for L = C. Moreover, since every application of the rules R∧ and R∨ introduces a new formula to an n-labelled constraint, the total number of such rule applications is bounded by |LT| · |Fg(ϕ)|. Finally, by Claim 1.1, the number of applications of rules R⊓, R⊔, R∀, R∃, R=, R6= per label n is bounded by 2q(|Fg(ϕ)|), where q is a polynomial function, since these rules add a new constraint to an n-labelled constraint system. Thus, the overall number of such rule applications is bounded by |LT| · 2q(|Fg(ϕ)|).
Theorem 2 (Soundness). If, having started on the initial completion set Tϕ, the LnALC tableau algorithm constructs an LnALC-complete and clash-free completion set for ϕ, then ϕ is LnALC satisfiable.
Proof. Given an LnALC-complete and clash-free completion set T for ϕ, define, for n ∈ LT, ψ ∈ for¬˙ (ϕ), C ∈ con ¬˙(ϕ), and x occurring in T, ⌊C⌋x = {n ∈ LT | n : C(x) ∈ Sn}, ⌊ψ⌋ = {n ∈ LT | n : ψ ∈ Sn}, ⌈C⌉x = LT \ {n ∈ LT | n : ¬˙C(x) ∈ Sn}, ⌈ψ⌉ = LT \ {n ∈ LT | n : ¬˙ψ ∈ Sn}.
Moreover, define Γxn = {ψ | n : ψ ∈ Sn} ∪ {C | n : C(x) ∈ Sn} and let γ, δ range over MLnALC formulas or concepts, where: ⌊γ⌋x = ⌊ψ⌋, if γ = ψ, and ⌊γ⌋x = ⌊C⌋x, if γ = C; and similarly for ⌈γ⌉x. We set M = (F , I), with F = (W, {Ni}i∈I ) and In = (Δn, ·In), for n ∈ W, defined as follows: • W = LT; • for every i ∈ I = {1, . . . , n}, we set Ni : W → 22W such that: – for L = E:
Ni(n) = α | for some 2iγ ∈ Γxn : ⌊γ⌋x ⊆ α ⊆ ⌈γ⌉x ; – for L = M: Ni(n) = α | for some 2iγ ∈ Γxn : ⌊γ⌋x ⊆ α ; – for L = C:
Ni(n) = α | for some 2iγ1 ∈ Γxn1, . . . , 2iγk ∈ Γxnk :
k k
Tj=1⌊γj⌋xj ⊆ α ⊆ Tj=1⌈γj⌉xj ; – for L = N:
Ni(n) = α | for some 2iγ ∈ Γxn : ⌊γ⌋x ⊆ α ⊆ ⌈γ⌉x ∪ W; • Δn = {x ∈ NV | x occurs in Sn}; • AIn = {x ∈ Δn | n : A(x) ∈ Sn}; First, we observe the following.
• rIn = {(x, y) ∈ Δn × Δn | n : r(x, y) ∈ Sn or n : r(z, y) ∈ Sn, for some z blocking x in Sn }. • For L = M, we have that M = (F , I) is such that F = (W, {Ni}i∈I ) is supplemented.
Indeed, for all n ∈ W, α, β ⊆ W, suppose that α ∈ Ni(n) and α ⊆ β. By definition, this implies that: for some 2iγ ∈ Γxn, ⌊γ⌋x ⊆ α ⊆ β. Hence, β ∈ Ni(n). • For L = C, we have that M = (F , I) is such that F = (W, {Ni}i∈I ) is closed under intersection. Indeed, for all n ∈ W, α, β ⊆ W, suppose that α ∈ Ni(n) and k β ∈ Ni(n). Now suppose that, for some 2iγ1 ∈ Γxn1 , . . . , 2iγk ∈ Γxnk : Tj=1⌊γj ⌋xj ⊆ α ⊆ Tjk=1⌈γj ⌉xj and, for some 2iδ1 ∈ Γyn1 , . . . , 2iδh ∈ Γynh : Tjh=1⌊δj ⌋yj ⊆ β ⊆ Tjh=1⌈δj ⌉yj . Then for some 2iγ1 ∈ Γxn1 , . . . , 2iγk ∈ Γxnk and some 2iδ1 ∈ Γyn1 , . . . , 2iδh ∈ Γynh the following holds, which in turn implies that α ∩ β ∈ Ni(n): k h k h
Tj=1⌊γj ⌋xj ∩ Tj=1⌊δj ⌋yj ⊆ α ∩ β ⊆ Tj=1⌈γj ⌉xj ∩ Tj=1⌈δj ⌉yj • For L = N, we have that M = (F , I), with F = (W, {Ni}i∈I ), is such that F contains the unit. Indeed, by construction, for all n ∈ W, W ∈ Ni(n).
We then require the following claims.
Claim 2.1. For every n ∈ W, C ∈ con¬˙ (ϕ), and x ∈ Δn: if n : C(x) ∈ Sn, then x ∈ CIn . Proof of Claim. We show the claim by induction on the weight of C (in NNF). The base case of C = A comes immediately from the definitions. For the base case of C = ¬A, suppose that n : ¬A(x) ∈ Sn. Since T is clash-free, we have that n : A(x) 6∈ Sn, and thus x 6∈ AIn by definition of AIn , meaning x ∈ (¬A)In . The inductive cases of C = D⊓E and C = D⊔E come from the fact that Sn is closed under R⊓ and R⊔, respectively, and straightforward applications of the inductive hypothesis. We show the remaining cases (cf. also [28, Claim 15.2]). x C = ∃r.D. Let n : ∃r.D(x) ∈ Sn, meaning that ∃r.D ∈ Γn. We distinguish two cases. • x is not blocked by any variable in Sn. Since Sn is closed under R∃, there exists y occurring in Sn such that n : r(x, y) ∈ Sn and n : D(y) ∈ Sn. Thus, by definition, (x, y) ∈ rIn and n : D(y) ∈ Sn. By inductive hypothesis, we obtain that x ∈ (∃r.D)In . • x is blocked by a variable in Sn, implying that there exists a <-minimal (since < is a well-ordering) y occurring in Sn such that y < x and {E | n : E(x) ∈ Sn} ⊆ {E | n : E(y) ∈ Sn}. In turn, this implies that y is not blocked by any other variable z in Sn (for otherwise z would block x, with z < y, against the fact that y is <-minimal). By reasoning as in the case above, since y is not blocked and Sn is closed under R∃, we have a variable z occurring in Sn such that n : r(y, z) ∈ Sn and n : D(x) ∈ Sn. Since y blocks x, by definition we have that (x, z) ∈ rIn , and by inductive hypothesis we get from n : D(z) that z ∈ DIn . Thus, x ∈ (∃r.D)In .
C = ∀r.D. Let n : ∀r.D(x) ∈ Sn, meaning that ∀r.D ∈ Γxn, and suppose that (x, y) ∈ rIn . By definition, either n : r(x, y) ∈ Sn or n : r(z, y) ∈ Sn, for some z blocking x in Sn. In the former case, since Sn is closed under R∀, we get that n : D(y) ∈ Sn. In the latter case, since z blocks x in Sn, we obtain n : ∀r.D(z) ∈ Sn; again, since Sn is closed under R∀, this implies that n : D(y) ∈ Sn. Hence, in both cases, we have n : D(y) ∈ Sn. By inductive hypothesis, this means that y ∈ DIn . Since y was arbitrary, we conclude that x ∈ (∀r.D)In .
C = 2iD. Let n : 2iD(x) ∈ Sn, meaning that 2iD ∈ Γxn. Consider L ∈ Log. L = E. We have by inductive hypothesis that ⌊D⌋x = {n ∈ W | n : D(x) ∈ Sn} ⊆ {n ∈ W | x ∈ DIn } = JDKxM. By inductive hypothesis (since | ¬˙D| = |D|), we also have that L = M. We have by inductive hypothesis that ⌊D⌋x = {n ∈ W | n : D(x) ∈ Sn} ⊆ {n ∈ W | x ∈ DIn } = JDKxM. Thus, we have 2iD ∈ Γxn such that ⌊D⌋x ⊆ JDKxM. By definition, this means JDKxM ∈ Ni(n), as required.
L ∈ {C, N}. These cases are analogous to the case for L = E.
C = ◇iD. Let n : ◇iD(x) ∈ Sn. Consider L ∈ Log.
L = C. We distinguish two cases. (i) There exist no 2iγ1 ∈ Γyn1 , . . . , 2iγk ∈ Γynk . As for L = E, we obtain x ∈ (◇iD)In . (ii) There exist 2iγ1 ∈ Γyn1 , . . . , 2iγk ∈ Γynk . Since T is LnALC-complete, there exists m ∈ W such that: γ1 ∈ Γym1 , . . . , γk ∈ Γymk and D ∈ Γxm; or ¬˙γj ∈ Γymj and ¬˙ D ∈ Γxm, for some j ≤ k. By inductive hypothesis, the previous step implies that there exists m ∈ W such that: γ1 ∈ Γym1 , . . . , γk ∈ Γymk and x ∈ DIm ; or ¬˙ γj ∈ Γymj and x ∈ ¬˙DIm , for some j ≤ k. Equivalently, it is not the case that, for every v ∈ W: γ1 ∈ Γym1 , . . . , γk ∈ Γymk implies x 6∈ DIm ; and for all j ≤ k, x ∈ ¬˙ DIm implies ¬˙γj 6∈ Γymj . In other words, it is not the case that: Tj=1⌊γj ⌋yj ⊆ W \ JDKxM; and k k
W \ JDKxM ⊆ Tj=1⌈γl⌉yl . Thus, W \ JDKxM 6∈ Ni(n), i.e., x ∈ (◇iD)In , as required. L = N. We distinguish two cases. (i) There exists no 2iγ ∈ Γyn. This means that Ni(n) = W.
Since T is LnALC-complete, there exists m ∈ W such that D ∈ Γxm, i.e., m : D(x) ∈ Sm. By inductive hypothesis, this implies x ∈ DIm , that is, JDKxM 6= ∅. This holds iff W \ JDKxM 6= y W, and thus W \ JDKxM 6∈ Ni(n). Hence, x ∈ (◇iD)In . (ii) There exists 2iγ ∈ Γn. We then reason similarly to the case for L = C.
Claim 2.2. For every w ∈ W and ψ ∈ con¬˙ (ϕ): if n : ψ ∈ Sn, then M, w |= ψ. Proof of Claim. We prove the claim by induction on the weight of ϕ (in NNF).
ψ = (⊤ ⊑ C). Let n : ⊤ ⊑ C ∈ Sn and let x ∈ Δn. Since Sn is closed under (R=) and x occurs in Sn, we have that n : C(x) ∈ Sn. By Claim 2.1, we have that x ∈ CIn . Given that x is arbitrary, we conclude that M, n |= ⊤ ⊑ C.
ψ = ¬(⊤ ⊑ C). Let n : ¬(⊤ ⊑ C) ∈ Sn. Since Sn is closed under (R6=), there exists x occurring in Sn such that n : ¬˙C(x) ∈ Sn. By Claim 2.1, we obtain that x ∈ ( ¬˙C)In , for some x ∈ Δw. Hence, M, n |= ¬(⊤ ⊑ C).
The inductive cases of ψ = χ∧ϑ and ψ = χ∨ϑ follow from the definitions and straighforward applications of the inductive hypothesis. Moreover the inductive cases of ψ = 2iχ and ψ = ◇iχ can be proved analogously to Claim 2.1.
Since, by definition, we have 0 : ϕ ∈ S0 ⊆ T, thanks to Claim 2.2 we obtain M, 0 |= ϕ.
Theorem 3 (Completeness). If ϕ is LnALC satisfiable, then, having started on the initial completion set Tϕ, the LnALC tableau algorithm constructs an LnALC-complete and clash-free completion set for ϕ.
Proof. Let M = (F , I) be an LnALC-model satisfying ϕ, with F = (W, {N }i∈I ), i.e., M, wϕ |= ϕ, for some wϕ ∈ W. We require the following definitions and technical results. First, we let γ, δ (possibly indexed) range over MLnALC concepts and formulas, with JγKdM = JψKM, if γ = ψ, and JγKdM = JCKdM, if γ = C. Then, for w ∈ W and d ∈ Sv∈W Δv, define Φdw = {ψ ∈ for¬˙ (ϕ) | M, w |= ψ} ∪ {C ∈ con¬˙ (ϕ) | d ∈ CIw }. Observe that, if C ∈ Φdw, then d ∈ Δw. We now show that the following holds.
Claim 3.1. For every w ∈ W and every d1, . . . , dk, e ∈ Sv∈W Δv: if 2iγ1 ∈ Φdw1 , . . . , 2iγk ∈ Φdwk and ◇iδ ∈ Φew, then there exists v ∈ W such that: (0) γ1 ∈ Φvd1 , . . . , γk ∈ Φvdk and δ ∈ Φev; or (1) ¬˙γ1 ∈ Φvd1 and ¬˙ δ ∈ Φev; or . .
.
(l) ¬˙γl ∈ Φvdk and ¬˙ δ ∈ Φev; where: for L = E, k = l = 1; for L = M, k = 1 and l = 0; for L = C, k ≥ 1 and l = k; for L = N, k = l = 1 or k = l = 0.
Proof. We consider each L ∈ Log.
L = E. Assume 2iγ ∈ Φdw, ◇iδ ∈ Φew, meaning that JγKdM ∈ Ni(w) and W \ JδKeM 6∈ Ni(w), i.e., J¬˙ δKeM 6∈ Ni(w). Towards a contradiction, suppose that, for every v ∈ W, the following holds: (γ 6∈ Φvd or δ 6∈ Φev) and ( ¬˙γ 6∈ Φvd or ¬˙δ 6∈ Φev). Equivalently, for every v ∈ W: (γ ∈ Φvd implies δ 6∈ Φev) and ( ¬˙δ ∈ Φev implies ¬˙ γ 6∈ Φvd). By definition, we have that γ ∈ Φvd iff ¬˙ γ 6∈ Φvd and δ 6∈ Φev iff ¬˙δ ∈ Φev. Thus, the previous step means: (JγKdM ⊆ J ¬˙δKeM) and (J ¬˙δKeM ⊆ JγKdM), i.e., JγKdM = J ¬˙δKeM, contradicting the assumption that JγKdM ∈ Ni(w) and J ¬˙δKeM 6∈ Ni(w).
L = M. Assume 2iγ ∈ Φdw, ◇iδ ∈ Φew, meaning that JγKdM ∈ Ni(w) and W \ JδKeM 6∈ Ni(w), i.e., J¬˙ δKeM 6∈ Ni(w). Towards a contradiction, suppose that, for every v ∈ W, the following holds: γ 6∈ Φvd or δ 6∈ Φev. Equivalently, for every v ∈ W: γ ∈ Φvd implies δ 6∈ Φev. By definition, the previous step means JγKdM ⊆ J¬˙ δKeM. Since M is supplemented, we have that J ¬˙δKeM ∈ Ni(w), which is impossible.
L = C. Assume 2iγ1 ∈ Φdw1 , . . . , 2iγk ∈ Φdwk , ◇iδ ∈ Φew, meaning that Jγj KdMj ∈ Ni(w), for j = 1, . . . , k, and W \ JδKeM 6∈ Ni(w), i.e., J ¬˙δKeM 6∈ Ni(w). Towards a contradiction, suppose that, for every v ∈ W, none of the following holds: (0) γ1 ∈ Φvd1 , . . . , γk ∈ Φvdk and δ ∈ Φev; (1) ¬˙γ1 ∈ Φvd1 and ¬˙δ ∈ Φev; ...; (k) ¬˙γk ∈ Φvdk and ¬˙δ ∈ Φev. Equivalently, for every v ∈ W, it holds that (0) γ1 ∈ Φvd1 , . . . , γk ∈ Φvdk implies δ 6∈ Φev; and (1) ¬˙δ ∈ Φev implies ¬˙γ1 6∈ Φvd1 ; ... and (k) ¬˙δ ∈ Φev implies ¬˙ γk 6∈ Φvdk . By definition, from the k previous step we obtain (0) Tj=1Jγj KdMj ⊆ J ¬˙δKeM; and (1) J ¬˙δKeM ⊆ Jγ1KdM1 ; ... and (k) k J ¬˙δKeM ⊆ JγkKdMk . Hence Tj=1Jγj KdMj = J ¬˙δKeM. Since M is closed under intersection, we obtain J ¬˙δKeM ∈ Ni(w), a contradiction.
L = N. We distinguish two cases: (i) Let k = l = 0. That is, there exists no 2iγ ∈ Φdw, while ◇iδ ∈ Φew, meaning that W \ JδKeM 6∈ Ni(w). Towards a contradiction, suppose that, for every v ∈ W, δ 6∈ Φev. Since, by definition, we have δ 6∈ Φev iff ¬˙δ ∈ Φev, the previous step means that W ⊆ J ¬˙δKeM, and hence JδKeM = ∅. Thus, W 6∈ Ni(w), contradicting the fact that M contains the unit. (ii) Let k = l = 1. Hence, there exists 2iγ ∈ Φew and ◇iδ ∈ Φew. We then reason similarly to the case for L = E.
Given a completion set T for ϕ and Sn ⊆ T, let Γxn = {ψ | n : ψ ∈ Sn} ∪ {C | n : C(x) ∈ Sn}. We say that a completion set T for ϕ is M-compatible if there exists a function π from LT to W, and, for every n ∈ LT, there exists a function πn from the set of variables occurring in Sn to Δπ(n), such that γ ∈ Γxn implies γ ∈ Φππn(n(x)). We then require the following claim. Claim 3.2. If a completion set T for ϕ is M-compatible, then for every LnALC-rule R applicable to T there exists a completion set T′ obtained from T by an application of R such that T′ is M-compatible.
Proof. Given an M-compatible completion set T for ϕ and a label n ∈ LT, let π and πn be the functions provided by the definition of M-compatibility. We need to consider each LnALC-rule R. For R ∈ {R∧, R∨, R⊓, R⊔, R∀, R∃, R=, R6=}, we proceed similarly to [28, Claim 15.14]. Here we consider the case of RL: Suppose that RL is applicable to T. Let 2iγ1 ∈ Γxn1 , . . . , 2iγk ∈ Γxnk , ◇iδ ∈ Γyn. Since T is M-compatible, we have that 2iγ1 ∈ Φππn(n(x)1), . . . , 2iγk ∈ Φππn(n(x)k) and ◇iδ ∈ Φππn(n(y)). Thus, by Claim 3.1, there exists v ∈ W such that: γ1 ∈ Φvπn(x1), . . . , γk ∈ Φvπn(xk) and δ ∈ Φvπn(y); or ¬˙γj ∈ Φvπn(xj) and ¬˙δ ∈ Φvπn(y), for some j ≤ l; where: for L = E, k = l = 1; for L = M, k = 1 and l = 0; for L = C, k ≥ 1 and l = k; for L = N, k = l = 1 or k = l = 0. By applying the rule RL accordingly, one can obtain T′ by adding m : γ1, . . . , m : γk, m : δ, or m : ¬˙γj , m : ¬˙δ, for some j ≤ l, to T (recall that m is fresh for T and γj is either ψj ∈ for¬˙ (ϕ) or Cj (xj ), with Cj ∈ con¬˙ (ϕ), for j = 1, . . . , k, and δ is either χ ∈ for¬˙ (ϕ) or D(y), with D ∈ con¬˙ (ϕ)). By extending π with π(m) = v, and πm with πm(x1) = πn(x1), . . . , πm(xk) = πn(xk), πm(y) = πn(y), we obtain that T′ is M-compatible.
To conclude, let Tϕ = {0 : ϕ, 0 : ⊤(x)} be the initial completion set for ϕ. Define π(0) = wϕ (where M, wϕ |= ϕ) and π0(x) = d, for an arbitrary d ∈ Δwϕ . Clearly, these functions ensure that Tϕ is M-compatible. By Claim 3.2, we can apply the LnALC-rules so that the obtained completion sets are M-compatible as well. From Theorem 1, we have that the LnALC tableau algorithm eventually terminates, returning an LnALC-complete completion set for ϕ that is clash-free by construction.
By Theorem 1, we have that the non-deterministic LnALC tableau algorithm terminates after exponentially many steps in the size of the input formula. By Theorems 2 and 3, such algorithm is sound and complete with respect to satisfiability in varying domain neighbourhood models. Thus, we obtain the following result.
Theorem 4. The LnALC formula satisfiability problem on varying domain neighbourhood models is decidable in NExpTime.
To conclude this section, we observe that as an immediate consequence of the above results
we also obtain a (constructive) proof of the following kind of exponential model property.
Corollary 5. For L ∈ {E, M, N} (respectively, L = C), every LnALC satisfiable formula ϕ has
a model with at most p(|Fg(ϕ)|) (respectively, at most 2p(|Fg(ϕ)|)) worlds, each of them having a
domain with at most 2q(|Fg(ϕ)|) elements, where p and q are polynomial functions.
Proof. By Theorem 3, if ϕ is LnALC satisfiable, then there is a LnALC-complete and clash-free
completion set T for it. Then by Theorem 2, there exists a model M = (W, {Ni}i∈I , I) for
ϕ where W = LT and for each n ∈ W, Δn = {x ∈ NV | x occurs in Sn}. By Theorem 1,
Claim 1.2, it follows |W| ≤ |Fg(ϕ)|2 for L ∈ {E, M, N}, and |W| ≤ 2|Fg(ϕ)| · |Fg(ϕ)| for
L = C, finally by Theorem 1, Claim 1.1, for each n ∈ W, |Δn| does not exceed 2q(|Fg(ϕ)|),
where p and q are polynomial functions.
4. Reasoning in Fragments without Modalised Concepts
An ALC-MLn formula is defined similarly to the MLnALC case, by disallowing modalised
concepts. Given L ∈ Log, the ALC-Ln formula satisfiability problem on constant domain
neighbourhood models is the ALC-MLn formula satisfiability problem on constant domain neighbourhood
models based on neighbourhood frames in the respective class for L (cf. Section 2). An MLn
formula, instead, is defined analogously to ALC-MLn, except that we built it from the
standard propositional (rather than ALC) language over a countable set of propositional letters
NP. The semantics of MLn formulas is given in terms of propositional neighbourhood models
(or simply models) MP = (W, {Ni}i∈I , V), where (W, {Ni}i∈I ) is a neighbourhood frame,
with I = {1, . . . , n} in the following, and V : NP → 2W is a function mapping propositional
letters to sets of worlds (see [
In Dalmonte et al. [
Vpπ∈NP(w) π ∧ Vpπ∈NP(w) ¬π, where NP(w) = {pπ ∈ NP(ϕ) | w ∈ V(pπ)} and NP(w) = NP(ϕ) \ NP(w). We now formalise the connection between ALC-MLn formulas and their propositional abstractions with the following lemma, where L ∈ {C, N}, obtained by adapting the proof of Dalmonte et al. [24, Lemma 1].
Lemma 6. A formula ϕ is ALC-Ln satisfiable on constant domain neighbourhood models iff ϕprop is satisfied in a ϕ-consistent Ln model.
We assume that the primitive connectives used to build propositional formulas are ¬ and ∧ (∨ is expressed using ¬ and ∧), and we denote by sub(ϕprop) the set of subformulas of ϕprop closed under single negation. A valuation for a propositional MLn formula ϕprop is a function ν : sub(ϕprop) → {0, 1} that satisfies the following conditions: (1) for all ¬ψ ∈ sub(ϕprop), ν(ψ) = 1 iff ν(¬ψ) = 0; (2) for all ψ1 ∧ ψ2 ∈ sub(ϕprop), ν(ψ1 ∧ ψ2) = 1 iff ν(ψ1) = 1 and ν(ψ2) = 1; and (3) ν(ϕprop) = 1. We say that a valuation for ϕprop is ϕ-consistent if any propositional neighbourhood model of the form ({w}, {Ni}i∈I , V) satisfying w ∈ V(pπ) iff ν(pπ) = 1, for all pπ ∈ NP(ϕ), is ϕ-consistent. We now establish that satisfiability of ϕprop in a ϕ-consistent Cn (respectively, Nn) model is characterized by the existence of a ϕ-consistent valuation satisfying the property described in Lemma 7 (respectively, Lemma 8). Lemma 7. A formula ϕprop is satisfied in a ϕ-consistent Cn model iff there is a ϕ-consistent valuation ν for ϕprop such that if 2iψ1, . . . , 2iψk are in sub(ϕprop), ν(2iψj ) = 1 for all 1 ≤ j < k, and ν(2iψk) = 0, then either (Vjk=−11 ψj ∧ ¬ψk) or (¬ψj ∧ ψk) for some 1 ≤ j < k is satisfied in a ϕ-consistent Cn model.
Proof. (⇒) Suppose that ϕprop is satisfied in a world w of a ϕ-consistent Cn model MP = (W, {Ni}i∈I , V). That is, MP, w |= ϕprop. We define a ϕ-consistent valuation for ϕprop by setting ν(ψ) = 1 if MP, w |= ψ and ν(ψ) = 0 if MP, w 6|= ψ. It is easy to check that ν is indeed a ϕ-consistent valuation (given that MP is a ϕ-consistent Cn model). Assume 2iψ1, . . . , 2iψk are in sub(ϕprop), ν(2iψj ) = 1 for all 1 ≤ j < k, and ν(2iψk) = 0. Then MP, w |= 2iψj for all 1 ≤ j < k, and MP, w 6|= 2iψk. By definition, (2iψ1 ∧. . .∧2iψk−1) → 2i(ψ1 ∧. . .∧ψk−1) holds in Cn models. So MP, w |= 2i(ψ1 ∧ . . . ∧ ψk−1) and MP, w 6|= 2iψk. This means that ν(2i(Vjk=−11 ψj )) = 1 while ν(2iψk) = 0. By definition, V(Vjk=−11 ψj ) ∈ Ni(w) and V(ψk) 6∈ Ni(w). So, V(Vjk=−11 ψj ) 6= V(ψk). Then, there is a world u in the symmetrical difference of these sets such that MP, u |= (Vjk=−11 ψj ∧ ¬ψk) ∨ (¬(Vjk=−11 ψj ) ∧ ψk).
(⇐) Suppose there is a ϕ-consistent valuation ν for ϕprop such that if 2iψ1, . . . , 2iψk are in sub(ϕprop), ν(2iψj ) = 1 for all 1 ≤ j < k, and ν(2iψk) = 0, then there is a ϕ-consistent Cn model
MPVjk=−11 ψj,ψk = (WVjk=−11 ψj,ψk , {NVjk=−11 ψj,ψki }i∈I , VVjk=−11 ψj,ψk ) and a world wVjk=−11 ψj,ψk ∈ WVjk=−11 ψj,ψk such that
Let M1P, . . . , MPm be an enumeration of the models MPVjk=−11 ψj,ψk , as above. That is, we take one model MPVlk=−11 ψl,ψk for each pair j = Vlk=−11 ψl, ψk where MjP = (Wj, {Nji}i∈I , Vj), and let w1, . . . , wm be an enumeration of the worlds wVlk=−11 ψl,ψk , with j = Vlk=−11 ψl, ψk and wj ∈ Wj. We assume without loss of generality that Wj ∩ Wk = ∅ for j 6= k.
In the following, we define a ϕ-consistent Cn model MP = (W, {Ni}i∈I , V) for ϕprop. Intuitively, we construct MP by taking the union of each MjP with the addition of a new world w that will satisfy ϕprop. We define W as S1≤j≤n Wj ∪ {w}, where w is fresh. Before defining Ni and V, we define the function J : sub(ϕprop) → 2W with J (ψ) = S0≤j≤m Vj(ψ) for all ψ ∈ sub(ϕprop), where V0 : sub(ϕ) → 2{w} is the function that assigns ψ to {w}, if ν(ψ) = 1, and to ∅, otherwise (Vj, for 1 ≤ j ≤ m, is as above). By construction, we have that J (¬ψ) = W \ J (ψ) and J (ψ1 ∧ ψ2) = J (ψ1) ∩ J (ψ2). We define the assignment V as the function V : NP(ϕ) → 2W satisfying V(pπ) = J (pπ) for all pπ ∈ NP(ϕ).
It remains to define Ni, for i ∈ I. For u ∈ Wj we first put α ⊆ W in Ni(u) precisely when MjP, u |= 2iψα and α = J (ψα) for some 2iψα ∈ sub(ϕ). Then, we close Ni under intersection so that MP is a Cn model. The next two claims establish that Ni is as expected. Claim 7.1. If β ∈ Ni(u) and β = J (ψ) for some 2iψ ∈ sub(ϕprop), then MjP, u |= 2iψ. Proof of Claim. Indeed, since β = J (ψ) ∈ Ni(u), we must have that MjP, u |= 2iψ1,β, . . . , MjP, u |= 2iψm,β and β = Tlm=1 J (ψl,β) for some 2iψ1,β, . . . , 2iψm,β ∈ sub(ϕprop). Since Ni is closed under intersection, in fact, we have that MjP, u |= 2i(Vlm=1 ψl,β). But since J (ψ) = Tim=1 J (ψi,β), we also have Vj(ψ) = Tlm=1 Vj(ψl,β) (recall that Wj ∩ Wk = ∅ for k 6= j), so MjP, u |= 2iψ iff MjP, u |= 2i(Vlm=1 ψl,β). It follows that MjP, u |= 2iψ.
Regarding the fresh world w introduced above in W, we first put α ⊆ W in Ni(w) precisely when ν(2iψα) = 1 and α = J (ψα) for some 2iψα ∈ sub(ϕprop). Then, we again close Ni under intersection so that MP is a Cn model.
Claim 7.2. If β ∈ Ni(w) and β = J (Vlk=−11 ψl) for some 2iψ1, . . . , 2iψk−1 ∈ sub(ϕprop) then ν(2iψl) = 1 for all 1 ≤ l < k.
Proof of Claim. Indeed, since β = J (Vlk=−11 ψl) ∈ Ni(w) we must have that ν(2iψ1,β) = 1, . . . , ν(2iψm,β) = 1 and β = Tim=1 J (ψi,β) for some 2iψ1,β, . . . , 2iψm,β ∈ sub(ϕprop). Suppose now that ν(Vlk=−11 ψl) = 0. Then, by assumption, there exists a structure MjP = (Wj, {Nji}i∈I , Vj) and a world wj ∈ Wj such that MjP, wj |= (Vlk=−11 ψl,β ∧ ¬(Vlk=−11 ψl)) ∨ (¬(Vlk=−11 ψl,β) ∧ (Vlk=−11 ψl)). It follows that Vj(Vlk=−11 ψl,β) 6= Vj(Vlk=−11 ψl). Consequently J (Vlk=−11 ψl,β) 6= J (Vlk=−11 ψl), which is a contradiction.
We now show by induction on the structure of formulas that V and J agree on sub(ϕprop). This holds by construction for atomic propositions. It is easy to deal with propositional connectives, since we know that J (¬ψ) = W \ J (¬ψ) and J (ψ1 ∧ ψ2) = J (ψ1) ∩ J (ψ2) and similarly for V. Assume inductively that V(ψ) = J (ψ). Suppose first that u ∈ J (2iψ). Then, either u = w and ν(2iψ) = 1 or u ∈ Wj and MjP, u |= 2iψ. In either case we have that J (ψ) ∈ Ni(u). Since V(ψ) = J (ψ), it follows that MP, u |= 2iψ, that is, u ∈ V(2iψ). Suppose now that u ∈ V(2iψ), that is, MP, u |= 2iψ, or, equivalently, V(ψ) ∈ Ni(u). Since V(ψ) = J (ψ) it follows that either u = w and ν(2iψ) = 1 or u ∈ Wj and MjP, u |= 2iψ. In either case we have that u ∈ J (2iψ).
Since ν(ϕprop) = 1, we have that w ∈ J (ϕprop), and consequently w ∈ V(ϕprop). That is, MP, w |= ϕprop. The fact that MP is a Cn model follows from the definition of Ni. The fact that MP is a ϕ-consistent model follows from the fact that ν, used to construct the assignment related to w, is ϕ-consistent and the models M1P, . . . , MPm, used to define the remaining worlds in W, are all ϕ-consistent models.
The following result can be proved by adapting the proof of the previous lemma. Lemma 8. A formula ϕprop is satisfied in a ϕ-consistent Nn model iff there is a ϕ-consistent valuation ν for ϕprop such that 1. if 2iψ is in sub(ϕprop) and ν(2iψ) = 0, then ¬ψ is satisfied in a ϕ-consistent Nn model; 2. if 2iψ1 and 2iψ2 are in sub(ϕprop), ν(2iψ1) = 1, and ν(2iψ2) = 0, then (ψ1 ∧ ¬ψ2) ∨ (¬ψ1 ∧ ψ2) is satisfied in a ϕ-consistent Nn model.
To determine satisfiability of ϕprop in a ϕ-consistent model, we use Lemma 6 and the characterizations above. To establish complexity results, we use the fact that there are only quadratically many subformulas in ϕprop. Satisfiability in ALC is ExpTime-complete and so, one can determine in exponential time whether a valuation is ϕ-consistent. For an ExpTime upper bound, one can deterministically compute all possible ϕ-consistent valuations for (Vjk=−11 ψj ∧ ¬ψk) (or (ψ1 ∧ ¬ψ2)) and decide satisfiability of ϕprop by a ϕ-consistent model using a bottom-up strategy (as in [31]). Since satisfiability in ALC is ExpTime-hard, our upper bound is tight. Theorem 9. The ALC-Cn and ALC-Nn formula satisfiability problems on constant domain neighbourhood models are ExpTime-complete.
In this paper, we have presented first results on reasoning in non-normal modal description logics. After providing motivations and preliminaries for these logics, we have focused on the following two aspects. First, we have introduced terminating, sound and complete tableaux algorithms for checking satisfiability of multi-modal description logics formulas in varying domain neighbourhood models based on classes of frames that characterise different non-normal systems, that is, En, Mn, Cn, and Nn. We have then studied the complexity of the satisfiability problem restricted to fragments where modal operators can be applied to formulas only (thus without modalised concepts) and interpreted on neighbourhood models with constant domains. As future work, we plan to investigate along the following directions.
First, we are interested in adapting our tableau algorithms to check satisfiability of formulas on neighbourhood models with constant domains. This requires to address the introduction of fresh variables that do not occur in other previously expanded labelled constraints systems. For instance, by applying the MnALC-rules to the n-labelled constraint system Sn = {n : ◇i∃r.A(x), 2i¬A(x)}, we obtain the m-labelled constraint system Sm = {m : ∃r.A(x), m : ¬A(x), m : r(x, y), m : A(y)}. The fresh variable y in Sm does not allow us to directly extract a model with constant domain, since there would be no object in the domain of the world associated with Sn capable of representing y correctly.
A possible solution could be to define a suitable notion of quasimodel [28], to equivalently
characterise satisfiability on constant domain neighbourhood models in terms of structures
representing “abstractions” of the actual models of a formula. The representation of domain
objects across worlds would be given in terms of suitably defined functions, called runs, to
guarantee that they are well-behaved with respect to their modal properties, and that they do
not violate the constant domain assumption. A similar approach is followed by Seylan and
Erdur [
In addition, we are interested in tight complexity results for LnALC formula satisfiability, with respect to varying and constant domain neighbourhood models. It is known that ALC formula satisfiability is ExpTime-complete. However, we do not know whether the upper bound for LnALC formula satisfiability problem on varying or constant domain neighbourhood models can be improved to ExpTime-membership, for any L ∈ {E, M, C, N}. It has to be noted that, at the propositional level, the formula satisfiability problem for the systems E, M, and N is known to be NP-complete, with a rise to PSpace-completeness for systems containing C [30].
Finally, we plan to consider satisfiability in other combinations and extensions of non-normal modal description logics. This would naturally lead us to consider both the straightforward cases of MC, MN and CN of the classical cube [32], as well as other logics tailored to applications in knowledge representation contexts. In particular, we intend to investigate non-normal modal description logics in epistemic, coalitional, and deontic settings.
Ozaki is supported by the Norwegian Research Council grant umber 316022 (OLEARN). [28] D. M. Gabbay, A. Kurucz, F. Wolter, M. Zakharyaschev, Many-dimensional Modal Logics:
Theory and Applications, Elsevier, 2003. [29] T. Dalmonte, B. Lellmann, N. Olivetti, E. Pimentel, Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity, Journal of Logic and Computation 31 (2021) 67–111. [30] M. Y. Vardi, On the complexity of epistemic reasoning, in: LICS, 1989, pp. 243–252. [31] F. Baader, S. Ghilardi, C. Lutz, LTL over description logic axioms, ACM T. Comput. Logic 13 (2012) 21:1–21:32. [32] B. Lellmann, E. Pimentel, Modularisation of sequent calculi for normal and non-normal modalities, ACM Trans. Comput. Log. 20 (2019) 7:1–7:46.