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 principles 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 modelling of obligations, beliefs, abilities and strategies. On the computational 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.
Several approaches to the formal study of normative, epistemic and action-based
notions are based on modal logic (ML) operators [
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 [
To overcome these problems, a different semantics, based on neighbourhood
(or minimal ) models, has been proposed [
Not much has been done yet in applications of non-normal MLs to
knowledge 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 [
In Section 2 we present MDLs, both recalling the standard relational
semantics, 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
formula 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 [
We start by introducing the required notation for normal and non-normal MDLs. 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 j :C j C u D j 9r:C j 2iC; where A 2 NC, r 2 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, oAr 2anNaCs,serrt2ionNRo,f athned fao;rbm2A(NaI). AornrM(aL;bnA)L,CwhfoerrmeuCl a;Dis aarne MexLpAreLsCsiocnonocfeptthse, form '; ::= j :' j ' ^ j 2i'; where is an MLnALC atom, and 1 i n. We will use the following standard definitions for concepts: ? A u :A, > :?; 8r:C :9r::C; (C t D) :(:C u :D); 3iC :2i:C (3i are called diamonds). Concepts of the form 2iC, 3iC 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; fRigi2[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 2 W an ALC interpretation (or model ) I(w) = ( ; I(w)) having domain , and where I(w) is a function such that: for all A 2 NC, AI(w) ; for all r 2 NR, rI(w) ; for all a 2 NI, aI(w) 2 , and for all u; v 2 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 CI(w), is defined by taking: (:C)I(w) =
n CI(w); (9r:C)I(w) = fd 2
A concept C is satisfied in M if there is w in F s.t. CI(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 j= ', is defined as: M; w j= C v D iff CI(w)
DI(w); M; w j= A(a) iff aI 2 AI(w);
M; w j= r(a; b) iff (aI ; bI ) 2 rI(w); M; w j= :' iff
M; w 6j= '; M; w j= ' ^ iff M; w j= ' and M; w j= ;
M; w j= 2i' iff for all v 2 W : if wRiv, then M; v j= ': Given an R-frame F = (W; fRigi2[1;n]) and an R-model M = (F; ; I), we say that ' is satisfied in M if there is w 2 W s.t. M; w j= ', and that ' is satisfiable (over R-models) if it is satisfied in some R-model. Also, ' is said to be valid in M , M j= ', 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 j= '. Moreover, ' logically implies a formula , writing ' j= , if M; w j= ' implies M; w j= , 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.
Neighbourhood Semantics. A neighbourhood frame (or N-frame) is a pair F = (W; fNigi2[1;n]), where W is a non-empty set and, for each 1 i n,
if for all ; W, 2 Ni(w) and implies 2 Ni(w); it is closed under intersection if 2 Ni(w) and 2 Ni(w) implies \ 2 Ni(w); and it contains the unit if for all w 2 W; W 2 Ni(w). An MLnALC neighbourhood model (or N-model ) based on an N-frame F is a triple M = (F ; ; I), where F = (W; fNigi2[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 2 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 CI(w), is defined as for the relational semantics, except from: where, for all d 2 , the set [C]dM = fv 2 W j d 2 CI(v)g 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. CI(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 j= ', is defined analogously to relational semantics, and as follows for modalised formulas:
M; w j= 2i' iff [']M 2 Ni(w); where [ ]M denotes the set fv 2 W j M; v j= g 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 j= 3i' iff [:']M 2= Ni(w). Given an N-frame F = (W; fNigi2[1;n]) and an N-model M = (F ; ; I), we say that ' is satisfied in M if there is w 2 W s.t. M; w j= ', 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,
respectively). 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. [
(ii) monotonicity holds on F iff F is supplemented; (iii) agglomeration holds on
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 . (Monotonicity) (Agglomeration) (Necessitation)
S j= C =_ D implies S j= 2iC =_ 2iD.
S j= ' $ implies S j= 2i' $ 2i .
S j= C v D implies S j= 2iC v 2iD.
S j= ' ! implies S j= 2i' ! 2i .
S j= 2iC u 2iD v 2i(C u D).
S j= 2i' ^ 2i ! 2i( ^ ).
S j= > v C implies S j= > v 2iC.
S j= ' implies S j= 2i'. or RB-y) ftrhaemMesLCnALwCe fmoremanultahesaptriosfibalebmilitoyf dperocibdleinmg iwnhaethclearsasnoMf(LrenAsLpCecftoivrmelyu,laNissatisfied 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 satisfiability problem in the class of N-frames, supplemented N-frames, and R-frames, respectively. 3
In this section we model well-known paradoxes that normal MLs with relational
semantics have to face in normative applications [
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 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 9activates:Switch intuitively denotes the set of objects that activate some switch, whereas 29activates: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 = fw; vg and N (w) = ffvgg, N (v) = ffwgg. Moreover, = fd1; d2; d3g, and let SwitchI(w) = SwitchI(v) = fd2g, activatesI(w) = ;, and activatesI(v) = f(d1; d2)g. We have (9activates:Switch)I(w) = ;, (9activates:Switch)I(v) = fd1g. Moreover, [9activates:Switch]dM1 = fvg and [9activates:Switch]dMi = ;, for i 2 f2; 3g. Thus, (29activates:Switch)I(w) = fd1g and (29activates: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., Signaller =_ Agent u 39activates:Switch; Guard =_ Agent u 29checks:Rail: Using modal operators over formulas, it is possible to express additional normative 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:
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,
Problems for Necessitation. Consider the CI, valid on every frame, that signallers either save a toddler, or they do not, i.e.,
Signaller v 9saves:Toddler t :9saves:Toddler: By Theorem 1, we have that on R-frames this formula is also obligatory:
This conclusion violates what is known in the literature as the principle of
deontic contingency [
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,
29activates:Switch u 2:9activates: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:
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 [
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
obligatoriness problem [
Another problematic inference is known in the literature as the Ross’s paradox. We have for instance that the following CI is valid on all R-frames: 9saves:Toddler v 9saves:Toddler t 9kills:Toddler: If the concept 29saves:Toddler, denoting the set of objects for which it is obligatory to save a toddler, is satisfiable, by Theorem 1 we obtain that the following concept is satisfiable as well:
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 [
Another similar difficulty related to monotonicity is known as the Good
Samaritan paradox [
At the propositional level, logics En and Mn have both been used as a
basis for weak deontic systems [
ALC ALC are applied globally, i.e., over ALC axioms only. Satisfiability in EnALC and MnALC . We provide a NExpTime upper bound by tursainngslaatrioenducytfiroonm,liMfteLdnAfLrComtotMheLp3ArnLoCpoissitdieofinnaeldcaasse,fotlolomwusl[t1i-7m,1o5d]a:l KAmLC . The Ay = A; (: )y = : y; (9r:C)y = 9r:Cy;
(C v D)y = Cy v Dy;
(
)y = y
y;
(2i )y = 3i1 (2i2 y
(#)y = #;
2i3 : y)
owrheforermAu2lasN, Ca, nrd2 NR2, #f uis; a^ng.asUsesritnigont,hisantrdansalaretibonot,hoeniethcearnMsLhnAoLwC tchoantcetphtes
satisfiability problem in N-frames is reducible to the formula satisfiability in the
relational case [
Proof (Sketch). Let ' be an MLnALC formula s.t. M; w j= ', for some N-model M = (F ; ; I) and some w in F = (W; fNigi2[1;n]). We define an R-frame F = (W; fRij gi2[1;n];j2[1;3]) and an ML3n
ALC R-model M = (F; ; I) s.t.: – W = f(w; 0) j w 2 Wg [ f( ; 1) j 2 Sv2W Ni(v)g – Ri1 = f((w; 0); ( ; 1)) j 2 Ni(w)g; – Ri2 = f(( ; 1); (w; 0)) j w 2 g – Ri3 = f(( ; 1); (w; 0)) j w 62 g – for every (w; 0) 2 W , I(w; 0) = I(w); for every ( ; 1) 2 W , XI( ;1) = ;, for all X 2 NC [ NR, and aI( ;1) = aI , for all a 2 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) j= 'y. Conversely, given a ML3n formula 'y s.t. M; w j= 'y, for some ML3AnLC R-model M = (F; ; I) basedALonC F = (W; fRij gi2[1;n];j2[1;3]), and some w 2 W , we define a MLnALC N-model M = (F ; ; I) based on F = (W; fNigi2[1;n]) s.t. W = W , and for all w 2 W : – 2 Ni(w) iff there is v 2 W s.t. wRi1 v and: (i) for all u 2 W , vRi2 u ) u 2 , and (ii) for all u 2 W , vRi3 u ) u 62 ; – I(w) = I(w).
Again, by induction, we obtain that M; w j= '.
The translation z from MLnALC to ML2AnLC is defined as y on all concepts and
formulas, except from the modalised concepts or formulas [
Proof (Sketch). The proof is similar to the one of Theorem 2. Given an N-model bMaLse2dn on a supplemented N-frame satisfying an MLnALC formula ', we define an
ALC R-model satisfying 'z 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; fNigi2[1;n]),
M; w j= 2i is equivalent to: there is 2 Ni(w) s.t. [ ]M. Conversely,
given a ML2AnLC R-model M = (F; ; I) based on F = (W; fRij gi2[1;n];j2[1;2])
and satisfying 'z, we define a MLnALC N-model M = (F ; ; I) based on F =
(W; fNigi2[1;n]) s.t. W = W and, for all w 2 W : I(w) = I(w); 2 Ni(w) iff
there is v 2 W s.t. wRi1 v and for all u 2 W , vRi2 u ) u 2 . The N-frame F
so defined is supplemented: for all w 2 W , if 2 Ni(w) and W , then
there is v 2 W s.t. wRi1 v and for all u 2 W , vRi2 u ) u 2 , i.e., 2 Ni(w).
Moreover, by induction, we have that M satisfies '. tu
SEanAtjLgiCsfiaanbdilMitynAjLgiCn uEsinAnjLggCthaenndotMionAnjLgoCf.a Wpreopnooswitsiohnoawl atibgshttraccotmiopnleoxf iatyforremsuulltas (faosr
in, e.g., [
ALC N-model MP = (W; fNigi2[1;n]; V) of 'prop is '-consistent if, for all w 2 W, the following ALC formula is satisfiable
V p 2NP(w) ^ V p 2NP(w) : where NP(w) = fp 2 NP(') j w 2 V(p )g and NP(w) = NP(') n NP(w). We anbowstrfaocrtmioanlsisweitthhethcoenfnoellcotwioinngbleetmwmeean. EnAjLgC formulas and their propositional LEenmmmodael1.. A formula ' is EnAjLgC satisfiable iff 'prop is satisfied in a '-consistent
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 ML formula 'prop is a function : sub('prop) ! f0; 1g that satisfies the following conditions: (1) for all : 2 sub('prop), ( ) = 1 iff (: ) = 0; (2) for all 1 ^ 2 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 (fwg; fNigi2[1;n]; V) satisfying w 2 V(p ) iff (p ) = 1, for all p 2 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.
'-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 [
ALC
is ExpTime-complete.
Regarding the proof for Mnjg , we first point out that Lemma 1 can be easily
ALC adapted to MnAjLgC . The proof for our ExpTime result for MnAjLgC is analogous to the one given for Enjg , except that here we use a variant of Lemma 2 tailored
ALC
for Mn (see Proposition 3.8 in [
ALC is ExpTime-complete. 5
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 ftohreitrhreesspaetcistfiivaebiflriatygmpernotbsleEmnAjLignC tahned nMonnA-jLngCo,rmwaitlhMmDoLdsalEonApeLrCataonrds aMppnAliLeCd, oannldy 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.