=Paper=
{{Paper
|id=Vol-2373/paper-14
|storemode=property
|title=On Non-normal Modal Description Logics
|pdfUrl=https://ceur-ws.org/Vol-2373/paper-14.pdf
|volume=Vol-2373
|authors=Tiziano Dalmonte,Andrea Mazzullo,Ana Ozaki
|dblpUrl=https://dblp.org/rec/conf/dlog/DalmonteMO19
}}
==On Non-normal Modal Description Logics==
https://ceur-ws.org/Vol-2373/paper-14.pdf
On Non-normal Modal Description Logics
Tiziano Dalmonte1 , Andrea Mazzullo2 , and Ana Ozaki2
1
Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France
tiziano.dalmonte@etu.univ-amu.fr
2
Free University of Bozen-Bolzano
surname@inf.unibz.it
Abstract. Non-normal modal logics based on neighbourhood semantics
can be used to formalise normative, epistemic and coalitional reasoning
in autonomous and multi-agent systems, since they do not validate prin-
ciples known to be problematic in applications. These principles, satisfied
by all modal logics interpreted over relational frames, also affect several
modal description logics (MDLs) used in knowledge representation. We
study non-normal MDLs, obtained by extending ALC-based languages
with non-normal modal operators. These logics increase the expressive
power of their propositional counterparts, and allow for complex mod-
elling of obligations, beliefs, abilities and strategies. On the computa-
tional side, standard reasoning tasks are not more difficult than in basic
normal MDLs, with a NExpTime upper bound for satisfiability that can
be lowered further in fragments with modal operators only over axioms.
1 Introduction
Several approaches to the formal study of normative, epistemic and action-based
notions are based on modal logic (ML) operators [9, 14, 16]. In the normative
setting, for instance, the so-called standard deontic logic (SDL) extends propo-
sitional logic with unary operators, intuitively interpreted as ‘it is obligatory’
and ‘it is permitted’. First-order extensions have been considered as well [16].
Research on autonomous systems [11], machine ethics [2], and normative multi-
agent systems [21] is drawing attention to challenging application scenarios for
deontic logics in computer science. Other motivations come from knowledge man-
agement in legal domains (e.g. legal ontologies and expert systems [8, 13]), Se-
mantic Web applications (e.g. legislative XML and RuleML [5, 18]), as well as
verification of normative systems, and modelling of the normative behaviour of
organisations (e.g. company policies specifications or contracting [19]).
The semantics of MLs, and of SDL in particular, is traditionally based on
relational frames, consisting of a set of possible worlds endowed with a binary
accessibility relation [9, 16]. These structures, used to interpret modal operators
(e.g. deontic, epistemic, dynamic, etc.), represent the connections between possi-
ble situations. For instance, in SDL, a proposition is said to be obligatory in some
possible world w, if it holds in all worlds related to w, interpreted as morally
ideal alternatives to w. However, all the so-called normal MLs, based on this
2 T. Dalmonte et al.
semantics, face the problem of validating principles that, in several applications,
can be hardly associated with an acceptable meaning. In SDL, these principles
lead to several counter-intuitive conclusions, often presented in the form of de-
ontic paradoxes. For instance, if it is obligatory to perform an action, and if this
action always implies a negative consequence, then we are forced to conclude
that also the latter is obligatory. Problematic arguments like this one represent
a strong limitation to the applicability of SDL to normative reasoning [16].
To overcome these problems, a different semantics, based on neighbourhood
(or minimal ) models, has been proposed [9]. Instead of using a set of worlds en-
dowed with an accessibility relation, this approach associates to each situation w
a family of sets of worlds. These sets intuitively represent the propositions that
are obligatory (or believed, brought about, etc.) in w. MLs based on this seman-
tics can satisfy weaker principles, without validating those axioms and rules that
are common to all normal MLs. For this reason, they are called non-normal MLs.
At the propositional level, non-normal MLs based on neighbourhood semantics
have received considerable attention [20, 10], with results reducing validity in
propositional non-normal MLs to validity in normal ones [17, 15]. To increase
the expressive power of these formalisms, first-order non-normal MLs based on
neighbourhood semantics have been considered as well [27, 3, 7].
Not much has been done yet in applications of non-normal MLs to knowl-
edge representation, in particular, to normative automated reasoning. Most of
the modal description logics (MDLs) considered in the literature are based on
the standard relational semantics [14]. Modal extensions of ALC with neigh-
bourhood semantics have been introduced as a basis of coalition logic [22, 24]
and agent communication [12] languages for reasoning over structured domains.
However, in normative settings, these MDLs still share several problems of propo-
sitional normal MLs. Failing to address this issue can lead to serious drawbacks
to normative reasoning in knowledge-based systems. In this paper we study non-
normal MDLs, interpreted over neighbourhood models, satisfying only minimal
requirements on the modal operators. With these formalisms, counter-intuitive
inferences in normative scenarios can be blocked, while still retaining the expres-
sive power needed in knowledge representation.
In Section 2 we present MDLs, both recalling the standard relational seman-
tics, and introducing the neighbourhood models used for non-normal MDLs. In
Section 3 we model with MDLs a scenario involving normative notions, discussing
deontic paradoxes due to relational semantics, and how they can be blocked using
neighbourhood models. Then, in Section 4, we study the complexity of the for-
mula satisfiability problem for non-normal MDLs. We prove NExpTime-upper
bounds for the complexity of the satisfiability problem, showing that reasoning is
not harder than in basic (normal) modal DLs with the relational semantics [14].
Directions for future work are discussed in Section 5.
2 Preliminaries
We start by introducing the required notation for normal and non-normal MDLs.
On Non-normal Modal Description Logics 3
Syntax. Let NC , NR and NI be countably infinite and pairwise disjoint sets
of concept names, role names, and individual names, respectively. An MLnALC
concept is an expression of the form C, D ::= A | ¬C | C u D | ∃r.C | 2i C,
where A ∈ NC , r ∈ NR , and 2i , with 1 ≤ i ≤ n, are modal operators called
boxes. An MLnALC atom is either a concept inclusion (CI ) of the form C v D,
or an assertion of the form A(a) or r(a, b), where C, D are MLALC concepts,
A ∈ NC , r ∈ NR , and a, b ∈ NI . An MLnALC formula is an expression of the
form ϕ, ψ ::= π | ¬ϕ | ϕ ∧ ψ | 2i ϕ, where π is an MLnALC atom, and 1 ≤ i ≤
n. We will use the following standard definitions for concepts: ⊥ ≡ A u ¬A,
> ≡ ¬⊥; ∀r.C ≡ ¬∃r.¬C; (C t D) ≡ ¬(¬C u ¬D); 3i C ≡ ¬2i ¬C (3i are
called diamonds). Concepts of the form 2i C, 3i C are called modalised concepts.
Analogous conventions also hold for formulas. In particular, we write C =˙ D for
C v D ∧ D v C.
Relational Semantics. A relational frame (or R-frame) is a structure F =
(W, {Ri }i∈[1,n] ), where W is a non-empty set and each Ri is a binary relation
on W . An MLnALC relational model (or R-model ) based on an R-frame F is a
structure M = (F, ∆, I), where ∆ is a non-empty set, called the domain of M ,
and I is a function associating with every w ∈ W an ALC interpretation (or
model ) I(w) = (∆, ·I(w) ) having domain ∆, and where ·I(w) is a function such
that: for all A ∈ NC , AI(w) ⊆ ∆; for all r ∈ NR , rI(w) ⊆ ∆×∆; for all a ∈ NI ,
aI(w) ∈ ∆, and for all u, v ∈ W , aI(u) = aI(v) (denoted by aI ). Given an R-model
M = (F, ∆, I) and a world w in F , the interpretation of a concept C in w,
written C I(w) , is defined by taking:
(¬C)I(w) = ∆ \ C I(w) , (C u D)I(w) = C I(w) ∩ DI(w) ,
(∃r.C)I(w) = {d ∈ ∆ | ∃e ∈ C I(w) : (d, e) ∈ rI(w) },
(2i C)I(w) = {d ∈ ∆ | ∀v ∈ W : wRi v ⇒ d ∈ C I(v) },
A concept C is satisfied in M if there is w in F s.t. C I(w) 6= ∅, and that C
is satisfiable (over R-models) if there is an R-model in which it is satisfied. The
satisfaction of a MLALC formula ϕ in w of M , written M, w |= ϕ, is defined as:
M, w |= C v D iff C I(w) ⊆ DI(w) ,
M, w |= A(a) iff aI ∈ AI(w) , M, w |= r(a, b) iff (aI , bI ) ∈ rI(w) ,
M, w |= ¬ϕ iff M, w 6|= ϕ, M, w |= ϕ ∧ ψ iff M, w |= ϕ and M, w |= ψ,
M, w |= 2i ϕ iff for all v ∈ W : if wRi v, then M, v |= ϕ.
Given an R-frame F = (W, {Ri }i∈[1,n] ) and an R-model M = (F, ∆, I), we say
that ϕ is satisfied in M if there is w ∈ W s.t. M, w |= ϕ, and that ϕ is satisfiable
(over R-models) if it is satisfied in some R-model. Also, ϕ is said to be valid in
M , M |= ϕ, if it is satisfied in all w of M , and it is valid on F if, for all M based
on F , ϕ is valid in M , writing F |= ϕ. Moreover, ϕ logically implies a formula
ψ, writing ϕ |= ψ, if M, w |= ϕ implies M, w |= ψ, for every M and every w in
M . Recall that the concept satisfiability problem can be reduced to the formula
satisfiability problem, since C is satisfiable iff ¬(C v ⊥) is satisfiable.
4 T. Dalmonte et al.
Neighbourhood Semantics. A neighbourhood frame (or N-frame) is a pair
F = (W, {Ni }i∈[1,n] ), where W is a non-empty set and, for each 1 ≤ i ≤ n,
Ni : W → P(P(W)) is called a neighbourhood function. A frame is supplemented
if for all α, β ⊆ W, α ∈ Ni (w) and α ⊆ β implies β ∈ Ni (w); it is closed
under intersection if α ∈ Ni (w) and β ∈ Ni (w) implies α ∩ β ∈ Ni (w); and
it contains the unit if for all w ∈ W, W ∈ Ni (w). An MLnALC neighbourhood
model (or N-model ) based on an N-frame F is a triple M = (F, ∆, I), where
F = (W, {Ni }i∈[1,n] ) is a neighbourhood frame, ∆ is a non-empty set called
the domain of M, and I is a function associating with every w ∈ W an ALC
interpretation I(w) = (∆, ·I(w) ), defined as above. Given a model M = (F, ∆, I)
and a world w in F, the interpretation of a concept C in w, written C I(w) , is
defined as for the relational semantics, except from:
(2i C)I(w) = {d ∈ ∆ | [C]M
d ∈ Ni (w)},
where, for all d ∈ ∆, the set [C]Md = {v ∈ W | d ∈ C
I(v)
} is called the truth
set of C with respect to d. We say that a concept C is satisfied in M if there is
w in F s.t. C I(w) 6= ∅, and that C is satisfiable (over N-models) if there is an
N-model in which it is satisfied. The satisfaction of an MLALC formula ϕ in w
of M, written M, w |= ϕ, is defined analogously to relational semantics, and as
follows for modalised formulas:
M, w |= 2i ϕ iff [ϕ]M ∈ Ni (w),
where [ψ]M denotes the set {v ∈ W | M, v |= ψ} of the worlds v that satisfy ψ,
also called the truth set of ψ. As a consequence of the above definition, we obtain
the following condition for diamond formulas: M, w |= 3i ϕ iff [¬ϕ]M ∈ / Ni (w).
Given an N-frame F = (W, {Ni }i∈[1,n] ) and an N-model M = (F, ∆, I), we say
that ϕ is satisfied in M if there is w ∈ W s.t. M, w |= ϕ, and that ϕ is satisfiable
(over N-models) if it is satisfied in some N-model. Other semantical definitions
can be easily adapted from the relational semantics case.
Frames and Satisfiability Problems. In the following, we use F to stand
either for an N- or R-frame, and M for a N- or R-model. To define the MLnALC
formula satisfiability problems studied in this paper, we consider the principles
listed in Table 1 (where C, D and ϕ, ψ are MLnALC concepts and formulas, re-
spectively). Here, S is either a frame F, or a model M. For a principle P , if
S = F (respectively, S = M), we say that P holds on F (respectively, in M). On
the correspondence between the principles in Table 1 and conditions over frames
and models, we have the following result (see e.g. [20] for the propositional case).
Theorem 1. Given an N-frame F, we have that: (i) congruence holds on F;
(ii) monotonicity holds on F iff F is supplemented; (iii) agglomeration holds on
F iff F is closed under intersection; (iv) necessitation holds on F iff F contains
the unit. Given an R-frame F , congruence, monotonicity, agglomeration, and
necessitation hold on F ; moreover, for every R-model M , they hold in M .
On Non-normal Modal Description Logics 5
(Congruence) S |= C =˙ D implies S |= 2i C =˙ 2i D.
S |= ϕ ↔ ψ implies S |= 2i ϕ ↔ 2i ψ.
(Monotonicity) S |= C v D implies S |= 2i C v 2i D.
S |= ϕ → ψ implies S |= 2i ϕ → 2i ψ.
(Agglomeration) S |= 2i C u 2i D v 2i (C u D).
S |= 2i ϕ ∧ 2i ψ → 2i (φ ∧ ψ).
(Necessitation) S |= > v C implies S |= > v 2i C.
S |= ϕ implies S |= 2i ϕ.
Table 1. Principles over frames and models.
By the MLnALC formula satisfiability problem in a class of (respectively, N-
or R-) frames C we mean the problem of deciding whether an MLnALC formula is
satisfied in a (respectively, N- or R-) model based on a frame in C. The formula
satisfiability problem for EnALC , MnALC , and KnALC is the MLnALC formula satisfi-
ability problem in the class of N-frames, supplemented N-frames, and R-frames,
respectively.
3 Modelling
In this section we model well-known paradoxes that normal MLs with relational
semantics have to face in normative applications [16]. Firstly, the MDLs language
introduced in Section 2 is used to provide a running example, that also illustrates
more expressive (with respect to the propositional case) features of the language.
Then, we show how principles validated by all normal MLs, and thus also by
the standard MDLs based on relational models, can affect reasoning in deontic
settings. We focus on the problems associated with necessitation, agglomeration,
and monotonicity in normal MDLs, claiming that the flexibility of neighbourhood
semantics represents an advantage in blocking problematic inferences.
Modelling Scenario. Consider the following variant of the classical trolley
problem scenario [25]. A tram is moving towards a toddler lying on the tracks.
Although it is not possible to stop the trolley, an agent (called signaller ), possibly
an autonomous control system, can activate a switch that would divert it on a
side track, saving the toddler’s life. However, on the side track lies an elderly
that would be killed with the activation of the switch. Therefore, the switching
system has to decide among two (horrible) alternatives: (1) do not activate the
switch, allowing the tram to kill the toddler; (2) activate the switch, saving the
toddler’s life and allowing an elderly to be killed instead.
For modelling purposes, it is crucial to have a formalism that allows to specify
both the factual features of the setting, and the ethical or legal aspects involved.
We assume that the domain consists of objects (e.g. a switch, a signaller, a
toddler, etc.), performing some actions (e.g. activating a switch) and bringing
about some consequences (e.g. to save, to kill) on each other. We represent classes
6 T. Dalmonte et al.
of objects with (unary) concepts, such as Switch, Signaller and Toddler, while
actions and consequences are formalised using (binary) roles, e.g., activates, saves
and kills. Obligations and permissions are indicated using 2 and 3, respectively.
For instance, the concept ∃activates.Switch intuitively denotes the set of objects
that activate some switch, whereas 2∃activates.Switch is the set of entities that
are obliged to do so. The following example shows a simple N-model interpreting
these latter concepts according to the definitions given in Section 2.
Example 1. Let M = (F, ∆, I) be a MLALC N-model, where F = (W, N ) is such
that W = {w, v} and N (w) = {{v}}, N (v) = {{w}}. Moreover, ∆ = {d1 , d2 , d3 },
and let SwitchI(w) = SwitchI(v) = {d2 }, activatesI(w) = ∅, and activatesI(v) =
{(d1 , d2 )}. We have (∃activates.Switch)I(w) = ∅, (∃activates.Switch)I(v) = {d1 }.
Moreover, [∃activates.Switch]M M
d1 = {v} and [∃activates.Switch]di = ∅, for i ∈
I(w)
{2, 3}. Thus, (2∃activates.Switch) = {d1 } and (2∃activates.Switch)I(v) = ∅.
Non-normal MDLs allow also for a meaningful distinction between de re
(applied to concepts) and de dicto (applied to formulas) modalities. For instance,
a signaller can be defined as an agent with the permission to activate a switch,
and a guard as an agent having the duty to check the rails, i.e.,
˙ Agent u 3∃activates.Switch,
Signaller = ˙ Agent u 2∃checks.Rail.
Guard =
Using modal operators over formulas, it is possible to express additional norma-
tive specifications. For example, stating that it is obligatory that a guard who
detects some dangerous situation must alert a station agent, which in turn has
the duty to alert an emergency service:
2 Guard u ∃detects.DangerousSituation v
2∃alerts.(StationAgent u 2∃alerts.EmergencyService) .
This flexibility in the application of modal operators allows us to assign different
sets of duties to the agents involved, while still enforcing these statements as
obligatory. To see this, compare the above definition of Guard with the case of a
bystander that happens to detect a situation of danger while checking the rails.
We could expect that it is obligatory for them to alert an emergency service,
without requiring that they ought to alert a station manager to do so. Namely,
2(∃checks.Rail u ∃detects.DangerousSituation v 2∃alerts.EmergencyService).
Problems for Necessitation. Consider the CI, valid on every frame, that
signallers either save a toddler, or they do not, i.e.,
Signaller v ∃saves.Toddler t ¬∃saves.Toddler.
By Theorem 1, we have that on R-frames this formula is also obligatory:
2(Signaller v ∃saves.Toddler t ¬∃saves.Toddler).
On Non-normal Modal Description Logics 7
This conclusion violates what is known in the literature as the principle of de-
ontic contingency [16], according to which what ought to be the case cannot be
enforced within a deontic system by virtue of logical validity alone.
More in general, given a formula ϕ that is valid in a R-model, we always have
that some logically implied formula ψ is obligatory, even when ϕ contains only
factual statements describing the domain of interest. For instance, suppose that
the following formula χ, stating that a toddler is a person, and that no person
is a trolley, is valid in a R-model M :
Toddler v Person ∧ Person v ¬Trolley.
The formula χ specifies only some of the factual features of the trolley problem
scenario, without any reference to normative notions, and it logically implies
Toddler v ¬Trolley. However, since χ is assumed to be valid in M , we are forced
to conclude that also the latter is valid in M , and thus, due to Theorem 1,
we have that 2(Toddler v ¬Trolley) is valid in M . Although true as a factual
statement, it is not clear why it should be inferred that this ought to be the case.
Problems for Agglomeration. Given the following concept D describing a
moral dilemma,
2∃activates.Switch u 2¬∃activates.Switch,
(that is, the obligation to activate a switch and the obligation not to do it), by
Theorem 1 we have that the following CI is valid on all R-frames:
D v 2(∃activates.Switch u ¬∃activates.Switch).
In other words, all objects incurring in a moral dilemma are also objects that are
obligated to do something inconsistent. This issue is sometimes presented in the
literature as the problem of self-inconsistent obligations for deontic agents [16].
Problems for Monotonicity. Since ⊥ v C, for any MLnALC concept C, is valid
on R-frames, by Theorem 1 we have for instance that on R-frames it is valid
2(∃activates.Switch u ¬∃activates.Switch) v 2∃kills.Toddler
Together with the CI discussed in the previous paragraph, we obtain that an
object in the extension of a moral dilemma (such as the one described by D) is
an object for which anything is obligatory, hence the names of universal obliga-
toriness problem [16], or deontic explosion [7].
Another problematic inference is known in the literature as the Ross’s para-
dox. We have for instance that the following CI is valid on all R-frames:
∃saves.Toddler v ∃saves.Toddler t ∃kills.Toddler.
If the concept 2∃saves.Toddler, denoting the set of objects for which it is obliga-
tory to save a toddler, is satisfiable, by Theorem 1 we obtain that the following
concept is satisfiable as well:
2(∃saves.Toddler t ∃kills.Toddler).
8 T. Dalmonte et al.
In other words, there can be individuals for which it is obligatory to save some
toddlers or to kill them. However, it is not easy to explain why the obligation to
save some toddlers should imply another obligation that can be fulfilled by killing
some of them. Indeed, if it is not possible for an agent to fulfil the obligation
to save some toddlers, it is still possible that they could partially attend to
their duties by respecting other normative constraints. An obligation that can
be fulfilled by killing some toddlers is a highly undesirable consequence that
could not be used as a partial justification in case the former goal (to save a
toddler) is not reachable. Therefore, it should not be derived in the normative
system [16].
Another similar difficulty related to monotonicity is known as the Good
Samaritan paradox [16]. Suppose that the deontic concept 2∃activates.Switch,
denoting the set of entities for which it is obligatory to activate the switch, is
satisfied in a R-model M , and that ∃activates.Switch v ∃kills.Elderly, (meaning
that if someone activates the switch, then they kill some elderly) is valid in that
model. By Theorem 1, we have that also the following is valid in M :
2∃activates.Switch v 2∃kills.Elderly
Thus, the concept 2∃kills.Elderly is satisfied in M , i.e., there is an object for
which it is obligatory to kill an elderly. Although the killing of an elderly is a
consequence implied by the activation of the switch, the obligation to do so is a
consequence that a trustworthy moral agent should not be able to draw.
Example 2. In the N-model of Example 1, let killsI(w) = killsI(v) = {(d1 , d3 )}
and ElderlyI(w) = ElderlyI(v) = {d3 }. For all u of M, M, u |= ∃activates.Switch v
∃kills.Elderly. For the concept 2∃kills.Elderly, we have [∃kills.Elderly]Md1 = {w, v},
M I(w)
and [∃kills.Elderly]d3 = ∅. Since {w, v} ∈ / N (w), (2∃kills.Elderly) = ∅. Sim-
/ N (v), and so (2∃kills.Elderly)I(v) = ∅. Therefore, in particular, the
ilarly, ∅ ∈
concept 2∃activates.Switch is satisfied in M, and the formula ∃activates.Switch v
∃kills.Elderly is satisfied in all worlds of M. However, the concept 2∃kills.Elderly
is not satisfied in M. Hence, the Good Samaritan paradox does not apply.
4 Satisfiability in Non-normal Modal Description Logics
At the propositional level, logics En and Mn have both been used as a ba-
sis for weak deontic systems [1, 9] (although Mn suffers from several problems
discussed in Section 3), as well as to interpret praxeological operators, such as
‘agent i has the ability to bring about ϕ’ [6, 20]. Moreover, Mn has been com-
bined with ALC, as a basis for further coalition logic extensions of description
logic languages [24, 23], and En modal operators have been applied over ALC
axioms to formalise reasoning about agents’ intentions [12] (however, without
establishing tight complexity results). In this section we study the complexity of
the formula satisfiability problem in EnALC and MnALC . This result is then low-
n|g n|g
ered for fragments, denoted by EALC and MALC , in which the modal operators
are applied globally, i.e., over ALC axioms only.
On Non-normal Modal Description Logics 9
Satisfiability in EnALC and MnALC . We provide a NExpTime upper bound by
using a reduction, lifted from the propositional case, to multi-modal Km
ALC . The
translation ·† from MLnALC to ML3n ALC is defined as follows [17, 15]:
A† = A, (∃r.C)† = ∃r.C † , (C v D)† = C † v D† , (ϑ)† = ϑ,
(¬γ)† = ¬γ † , (γ ◦ δ)† = γ † ◦ δ † , (2i γ)† = 3i1 (2i2 γ † ◦ 2i3 ¬γ † )
where A ∈ NC , r ∈ NR , ϑ is an assertion, γ and δ are both either MLnALC concepts
or formulas, and ◦ ∈ {u, ∧}. Using this translation, one can show that the
satisfiability problem in N-frames is reducible to the formula satisfiability in the
relational case [17, 15]. Since satisfiability in K3n
ALC is known to be NExpTime-
complete [14, Theorem 15.15], we obtain the following complexity result.
Theorem 2. Satisfiability in EnALC is in NExpTime.
Proof (Sketch). Let ϕ be an MLnALC formula s.t. M, w |= ϕ, for some N-model
M = (F, ∆, I) and some w in F = (W, {Ni }i∈[1,n] ). We define an R-frame
F = (W, {Rij }i∈[1,n],j∈[1,3] ) and an ML3n
ALC R-model M = (F, ∆, I) s.t.:
S
– W = {(w, 0) | w ∈ W} ∪ {(α, 1) | α ∈ v∈W Ni (v)}
– Ri1 = {((w, 0), (α, 1)) | α ∈ Ni (w)};
– Ri2 = {((α, 1), (w, 0)) | w ∈ α}
– Ri3 = {((α, 1), (w, 0)) | w 6∈ α}
– for every (w, 0) ∈ W , I(w, 0) = I(w); for every (α, 1) ∈ W , X I(α,1) = ∅, for
all X ∈ NC ∪ NR , and aI(α,1) = aI , for all a ∈ NI .
The pairs (w, 0), (α, 1) are used to ensure that W is the disjoint union of the
sets of worlds w and subsets α of W. By induction on concept and formulas
occurring in ϕ, one can show that M, (w, 0) |= ϕ† . Conversely, given a ML3n
ALC
formula ϕ† s.t. M, w |= ϕ† , for some ML3n ALC R-model M = (F, ∆, I) based on
F = (W, {Rij }i∈[1,n],j∈[1,3] ), and some w ∈ W , we define a MLnALC N-model
M = (F, ∆, I) based on F = (W, {Ni }i∈[1,n] ) s.t. W = W , and for all w ∈ W :
– α ∈ Ni (w) iff there is v ∈ W s.t. wRi1 v and: (i) for all u ∈ W , vRi2 u ⇒ u ∈
α, and (ii) for all u ∈ W , vRi3 u ⇒ u 6∈ α;
– I(w) = I(w).
Again, by induction, we obtain that M, w |= ϕ. t
u
The translation ·‡ from MLnALC to ML2n †
ALC is defined as · on all concepts and
formulas, except from the modalised concepts or formulas γ [17, 15]:
(2i γ)‡ = 3i1 2i2 γ ‡ .
We obtain an upper bound analogous to the one for EnALC by a reduction of the
formula satisfiability problem for MnALC to the same problem for K2n
ALC [17, 15,
14].
Theorem 3. Satisfiability in MnALC is in NExpTime.
10 T. Dalmonte et al.
Proof (Sketch). The proof is similar to the one of Theorem 2. Given an N-model
based on a supplemented N-frame satisfying an MLnALC formula ϕ, we define an
‡
ML2nALC R-model satisfying ϕ as above, by using relations Ri1 and Ri2 only. To
prove the inductive step for modalised formulas 2i ψ occurring in ϕ, we use the
fact that, in N-models M based on supplemented N-frames F = (W, {Ni }i∈[1,n] ),
M, w |= 2i ψ is equivalent to: there is α ∈ Ni (w) s.t. α ⊆ [ψ]M . Conversely,
given a ML2n ALC R-model M = (F, ∆, I) based on F = (W, {Rij }i∈[1,n],j∈[1,2] )
and satisfying ϕ‡ , we define a MLnALC N-model M = (F, ∆, I) based on F =
(W, {Ni }i∈[1,n] ) s.t. W = W and, for all w ∈ W : I(w) = I(w); α ∈ Ni (w) iff
there is v ∈ W s.t. wRi1 v and for all u ∈ W , vRi2 u ⇒ u ∈ α. The N-frame F
so defined is supplemented: for all w ∈ W , if α ∈ Ni (w) and α ⊆ β ⊆ W , then
there is v ∈ W s.t. wRi1 v and for all u ∈ W , vRi2 u ⇒ u ∈ β, i.e., β ∈ Ni (w).
Moreover, by induction, we have that M satisfies ϕ. t
u
n|g n|g
Satisfiability in EALC and MALC . We now show tight complexity results for
n|g n|g
EALC and MALC using the notion of a propositional abstraction of a formula (as
in, e.g., [4]). Here, one can separate the satisfiability test into two parts, one for
the description logic dimension and one for the dimension of the neighbourhood
n|g
frame. The propositional abstraction ϕprop of an EALC formula ϕ is the result
of replacing each ALC atom in ϕ by a propositional variable, so that there is a
1 : 1 relationship between the ALC atoms π occurring in ϕ and the propositional
letters pπ used for the abstraction. The semantics of ϕprop is given in terms of
propositional N-models (W, {Ni }i∈[1,n] , V) for En , where (W, {Ni }i∈[1,n] ) is a
N-frame and V : NP → P(W) is a function mapping propositional variables
in NP to sets of worlds (see [9, 26]). We denote by NP (ϕ) the set {pπ ∈ NP |
n|g
π is an ALC atom in ϕ}. Given an EALC formula ϕ, we say that a propositional
P
N-model M = (W, {Ni }i∈[1,n] , V) of ϕprop is ϕ-consistent if, for all w ∈ W, the
following ALC formula is satisfiable
V V
pπ ∈NP (w) π ∧ pπ ∈NP (w)
¬π
where NP (w) = {pπ ∈ NP (ϕ) | w ∈ V(pπ )} and NP (w) = NP (ϕ) \ NP (w). We
n|g
now formalise the connection between EALC formulas and their propositional
abstractions with the following lemma.
n|g
Lemma 1. A formula ϕ is EALC satisfiable iff ϕprop is satisfied in a ϕ-consistent
En model.
We assume that the primitive connectives used to build propositional formu-
las 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 ML 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
N-model of the form ({w}, {Ni }i∈[1,n] , V) satisfying w ∈ V(pπ ) iff ν(pπ ) = 1, for
On Non-normal Modal Description Logics 11
all pπ ∈ NP (ϕ), is ϕ-consistent. We now establish that satisfiability of ϕprop in a
ϕ-consistent model is characterized by the existence of a ϕ-consistent valuation
satisfying the property described in Lemma 2.
Lemma 2. A formula ϕprop is satisfied in a ϕ-consistent En model iff there is a
ϕ-consistent valuation ν for ϕprop such that 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 En model.
To determine satisfiability of ϕprop in a ϕ-consistent model, we use Lemma 2
and the fact that there are only quadratically many formulas of the form ψ1 ∧
¬ψ2 , where ψ1 and ψ2 are subformulas of ϕprop . We observe that satisfiability in
ALC is ExpTime-complete [14] 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 ψ1 ∧ ¬ψ2 and
decide satisfiability of ϕprop by a ϕ-consistent model using a bottom-up strategy
(as in [26]). As satisfiability in ALC is ExpTime-hard our upper bound is tight.
n|g
Theorem 4. Satisfiability in EALC is ExpTime-complete.
n|g
Regarding the proof for MALC , we first point out that Lemma 1 can be easily
n|g n|g
adapted to MALC . The proof for our ExpTime result for MALC is analogous to
n|g
the one given for EALC , except that here we use a variant of Lemma 2 tailored
for Mn (see Proposition 3.8 in [26]). Thus, we obtain also the following result.
n|g
Theorem 5. Satisfiability in MALC is ExpTime-complete.
5 Conclusion
We have studied non-normal MDLs based on neighbourhood models, showing
how to express normative specifications in a deontic scenario, and highlighting
the differences with relational semantics. We have established complexity results
for the satisfiability problem in the non-normal MDLs EnALC and MnALC , and
n|g n|g
their respective fragments EALC and MALC , with modal operators applied only
over the description logic axioms. These logics represent the basis for further
extensions in deontic, epistemic, and dynamic contexts. As future work, we plan
to study logics interpreted over suitably constrained neighbourhood frames, so to
provide additional reasoning capabilities in multi-agent systems. MDLs extended
with non-normal dyadic modal operators, to express conditional obligations or
beliefs, such as ‘it is obligatory/believed that ϕ, given ψ’, represent another
direction for further research.
12 T. Dalmonte et al.
References
1. Anglberger, A.J., Gratzl, N., Roy, O.: Obligation, free choice, and the logic of
weakest permissions. Rev. Symb. Logic 8(4), 807–827 (2015)
2. Arkoudas, K., Bringsjord, S., Bello, P.: Toward ethical robots via mechanized de-
ontic logic. In: AAAI fall symposium on machine ethics. pp. 17–23 (2005)
3. Arló-Costa, H.L., Pacuit, E.: First-order classical modal logic. Stud. Logica 84(2),
171–210 (2006)
4. Baader, F., Ghilardi, S., Lutz, C.: LTL over description logic axioms. ACM T.
Comput. Logic 13(3), 21:1–21:32 (2012)
5. Boer, A., Winkels, R., Vitali, F.: Metalex XML and the legal knowledge interchange
format. In: Computable Models of the Law, pp. 21–41 (2008)
6. Brown, M.A.: On the logic of ability. J. Philos. Logic 17(1), 1–26 (1988)
7. Calardo, E., Rotolo, A.: Quantification in some non-normal modal logics. J. Philos.
Logic 46(5), 541–576 (2017)
8. Casellas, N.: Legal Ontology Engineering. Springer (2011)
9. Chellas, B.F.: Modal logic: an introduction. Cambridge University Press (1980)
10. Dalmonte, T., Olivetti, N., Negri, S.: Non-normal modal logics: Bi-neighbourhood
semantics and its labelled calculi. In: AiML. pp. 159–178 (2018)
11. Dennis, L.A., Fisher, M., Slavkovik, M., Webster, M.: Formal verification of ethical
choices in autonomous systems. Robot. Auton. Syst. 77, 1–14 (2016)
12. Erdur, R.C., Seylan, I.: The design of a semantic web compatible content language
for agent communication. Expert Syst. 25(3), 268–294 (2008)
13. Francesconi, E.: A description logic framework for advanced accessing and reason-
ing over normative provisions. Artif. Intell. Law 22(3), 291–311 (2014)
14. Gabbay, D.M., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional
Modal Logics: Theory and Applications. Elsevier (2003)
15. Gasquet, O., Herzig, A.: From classical to normal modal logics. In: Proof theory
of modal logic, pp. 293–311. Springer (1996)
16. Hansson, S.O.: Alternative semantics for deontic logic. In: Handbook of Deontic
Logic and Normative Systems, pp. 445–497. College Publication (2013)
17. Kracht, M., Wolter, F.: Normal monomodal logics can simulate all others. J. Sym-
bolic Logic 64(1), 99–138 (1999)
18. Lam, H., Hashmi, M.: Enabling reasoning with LegalRuleML. TPLP 19(1), 1–26
(2019)
19. Meyer, J.C., Wieringa, R.J., Dignum, F.: The role of deontic logic in the specifi-
cation of information systems. In: Logics for Databases and Information Systems.
pp. 71–115. Kluwer (1998)
20. Pacuit, E.: Neighborhood Semantics for Modal Logic. Springer (2017)
21. Pigozzi, G., van der Torre, L.W.N.: Multiagent deontic logic and its challenges
from a normative systems perspective. FLAP 4(9), 2929–2993 (2017)
22. Seylan, I., Erdur, R.C.: A tableau decision procedure for ALC with monotonic
modal operators and constant domains. ENTCS 231, 113–130 (2009)
23. Seylan, I., Jamroga, W.: Coalition description logic with individuals. ENTCS 262,
231–248 (2010)
24. Seylan, I., Jamroga, W.: Description logic for coalitions. In: AAMAS. pp. 425–432
(2009)
25. Thomson, J.J.: The Trolley Problem. Yale LJ 94(6), 1395–1415 (1985)
26. Vardi, M.Y.: On the complexity of epistemic reasoning. In: LICS. pp. 243–252 (1989)
27. Waagbø, G.: Quantified modal logic with neighborhood semantics. Math. Logic
Quart. 38(1), 491–499 (1992)