=Paper=
{{Paper
|id=Vol-1645/paper_15
|storemode=property
|title=ASP for Reasoning about Actions with an EL^bot Knowledge Base
|pdfUrl=https://ceur-ws.org/Vol-1645/paper_15.pdf
|volume=Vol-1645
|authors=Laura Giordano,Alberto Martelli,Matteo Spiotta,Daniele Theseider Dupré
|dblpUrl=https://dblp.org/rec/conf/cilc/0001MSD16
}}
==ASP for Reasoning about Actions with an EL^bot Knowledge Base==
https://ceur-ws.org/Vol-1645/paper_15.pdf
ASP for reasoning about actions with
an EL⊥ knowledge base
Laura Giordano1 , Alberto Martelli2 , Matteo Spiotta2 , and Daniele Theseider Dupré1
1
DISIT - Università del Piemonte Orientale, Alessandria, Italy
laura.giordano@uniupo.it, dtd@di.unipmn.it
2
Dip. di Informatica - Università di Torino, Italy
mrt@di.unito.it , matteo.spiotta@gmail.com
Abstract. In this paper we propose an approach based on Answer Set Program-
ming (ASP) for reasoning about actions in a domain description including knowl-
edge expressed in the low complexity description logic EL⊥ . We consider an
action theory in which the state is a set of positive and negative assertions, that
we represent through explicit negation. The action language allows for non-deter-
ministic actions, and causal rules are introduced to deal with ramifications. We
provide sufficient conditions under which action consistency can be guaranteed
and we define a polynomial encoding of the action theory in ASP.
1 Introduction
The integration of description logics and action formalisms has recently gained a lot
of interest [5, 4, 11, 1]. In this paper we explore the combination of an action language
based on Answer Set Programming (ASP) [16] with the low complexity description
logic EL⊥ [2, 3]. The temporal extension of ASP proposed in [20] is used as the basis
for integrating an EL⊥ knowledge base over the action theory. The aim is reasoning
about action execution with an EL⊥ knowledge base.
As usual in the formalisms integrating description logics and action languages [5,
6, 11, 1], we regard inclusions in the KB as state constraints of the action theory, which
we expect to be satisfied in the state resulting after an action. In the literature of rea-
soning about actions it is well known that causal laws and their interplay with domain
constraints are crucial for solving the ramification problem [27, 25, 28, 12, 18, 21].
In case knowledge on a domain is expressed in a description logic, the issue has
been considered, e.g., in [4] where causal laws are used to ensure the consistency with
the TBox (i.e., the set of terminological axioms) of a state resulting from an action. For
instance, given a TBox containing ∃Teaches.Course v Teacher , and an ABox (i.e.,
a set of assertions on individuals) containing the assertion Course(math), an action
which adds the assertion Teaches(john, math), without also adding Teacher (john),
will not give rise to a next state consistent with the knowledge base. The addition of the
causal law caused Teacher (john) if Teaches(john, math) ∧ Course(math) would
allow for instance the above TBox inclusion to be satisfied in the resulting state.
In this paper we define an action theory for reasoning about actions with an EL⊥
knowledge base. The semantics aims at extending to the treatment of non-deterministic
actions (as well as to the treatment of frame/non-frame fluents) the approach proposed
by Baader et al. [4] which uses causal relationships to deal with the ramification prob-
lem in an action formalism based on description logics. In [4] a semantics of actions
and causal laws is defined in the style of Winslett’s [29] and McCain and Turner’s [27]
fixpoint semantics. To deal with non-deterministic effects of actions (not allowed in
[4]), as well as with ramifications, through static and dynamic causal laws [21, 19, 12,
13, 20], we provide a semantics based on Answer Sets [16], which appears to be well
suited to provide a simple definition of temporal projection for EL⊥ action theories,
along the lines of previous work on reasoning about actions in ASP [17, 9, 13, 7].
In particular, as in EL⊥ negated concepts are not included, we allow ASP-like ex-
plicit negation to occur in assertions within states as well as in direct or indirect effects
of actions so to allow for the addition and deletion of assertions by action execution. In
this paper, we consider reasoning about states which correspond to DL interpretations;
a state transition transforms an interpretation into a new one, in agreement with the se-
mantics of other DL-based approaches to reasoning about actions [5, 4, 11, 1]. We also
provide sufficient conditions under which an action specification can be guaranteed to
be consistent with the TBox.
The projection problem is reduced to the problem of computing the answer sets
of the action theory, given an underlying EL⊥ knowledge base. In this respect, two
approaches are feasible: either to encode the action theory into a formalism which al-
ready combines ASP and DLs, as in [14], or to provide a direct encoding of the action
language in ASP. As inference in EL⊥ can be polynomially encoded into ASP by the
materialization calculus proposed by Krötzsch [23], the second approach appears to be
a natural choice, which also allows to exploit well known encodings of reasoning about
actions into ASP [17, 9, 13, 7]. We define an encoding in ASP of the action theory so
that temporal projection and other reasoning problems can be reduced to computing the
answer sets of a program, whose size is polynomial in the size of the action theory and
of the EL⊥ knowledge base. The complexity of the temporal projection problem is in
co-NP so that, as expected, the presence of an EL⊥ TBox does not increase the worst
case complexity for the temporal projection problem.
Our approach also relates to the approach to action reasoning proposed in [20], and
can be extended by exploiting the approach therein for the verification of LTL temporal
properties of an action theory, through bounded model checking.
2 The description logic EL⊥
We consider a fragment of the logic EL++ [2] that, for simplicity of presentation, does
not include role inclusions and concrete domains. The fragment, let us call it EL⊥ ,
includes the concept ⊥ as well as nominals.
We let NC be a set of concept names, NR a set of role names and NI a set of
individual names. A concept in EL⊥ is defined as follows:
C := A | > | ⊥ | C u C | ∃r.C | {a}
where A ∈ NC and r ∈ NR . Observe that complement, disjunction and universal
restriction are not allowed in EL⊥ .
A KB is a pair (T , A), where T is a TBox containing a finite set of concept inclu-
sions C1 v C2 and A is an ABox containing assertions of the form C(a) and r(a, b),
with C, C1 , C2 concepts, r ∈ NR and a, b ∈ NI .
We will assume that the TBox is in normal form [3]. Let BCKB be the smallest set
of concepts containing >, all the concept names occurring in KB and all nominals {a},
for any individual name a occurring in KB . An inclusion is in normal form if it has one
of the following forms: C1 v D, C1 u C2 v D, C1 v ∃r.C2 , ∃r.C2 v D, where
C1 , C2 ∈ BCKB , and D ∈ BCKB ∪ {⊥}. In [3] it is shown that any TBox can be
normalized in linear time, by introducing new concept and role names.
The following is the usual definition for interpretations and models.
Definition 1 (Interpretations and models). An interpretation in EL⊥ is any structure
(∆I , ·I ) where: ∆I is a domain; ·I is an interpretation function that maps each concept
name A to set AI ⊆ ∆I , each role name r to a binary relation rI ⊆ ∆I × ∆I , and
each individual name a to an element aI ∈ ∆I . Furthermore:
– >I = ∆I , ⊥I = ∅;
– {a}I = {aI };
– (C u D)I = C I ∩ DI ;
– (∃r.C)I = {x ∈ ∆ | ∃y ∈ C I : (x, y) ∈ rI }.
An interpretation (∆I , ·I ) satisfies an inclusion C v D if C I ⊆ DI ; it satisfies an
assertion C(a) if aI ∈ C I ; it satisfies an assertion r(a, b) if (aI , bI ) ∈ rI .
Given a KB = (T , A), an interpretation (∆I , ·I ) is a model of T if (∆I , ·I ) satis-
fies all inclusions in T ; (∆I , ·I ) is a model of KB if (∆I , ·I ) satisfies all inclusions in
T and all assertions in A. A is consistent with T if there is a model of T satisfying all
the assertions in A.
In the following we will denote with NC,KB , NR,KB and NI,KB the (finite) sets of
concept names, role names and individual names occurring in KB .
3 The action theory
Reasoning about actions in a description logic, given a knowledge base KB = (T , A),
consists in reasoning about the evolution of the world, starting from an initial state com-
patible with the ABox A and satisfying the TBox T , and updating the state according to
actions specifications. In our proposal, as well as in most other proposals for reasoning
about actions in DLs [5, 6, 11, 4, 1] the TBox is regarded as a set of state constraints, i.e.
conditions that must be satisfied by any state of the world.
This section defines the language of the action theory, and the notion of state. Let
P red be a set of predicate symbols and C be a finite set of constants. We define a set
of fluents F as a set of ground atomic propositions p(a1 , . . . , ak ) where p ∈ P red is a
n-ary predicate symbol and a1 , . . . , an ∈ C. A fluent literal l is a fluent f or its explicit
negation −f . We denote by Lit the set of fluent literals. We assume that distinguished
0-ary predicates ⊥ and > (representing inconsistency and truth) belong to Lit.
We want to regard DL assertions as fluents that occur in our action laws as well as
in the states of the action theory. Given a (normalized) EL⊥ knowledge base KB =
(T , A), we require P red to include:
– a unary predicate C, for each (possibly complex) concept C occurring in KB (we
let P redC be the set of such predicates);
– a binary predicate r, for each role name r ∈ NR,KB (we let P redR be the set of
such predicates);
Also, we require C to include the individual names occurring in the KB , i.e. NI,KB ⊆
C.
Observe that if a complex concept such as ∃r.C occurs in the KB , there is a pred-
icate name ∃r.C in P red and for each a ∈ NI,KB , the fluent literals (∃r.C)(a) and
−(∃r.C)(a) belong to the set Lit (sometimes we will still call such literals assertions).
Although classical negation is not allowed in EL⊥ (as well as in ASP), we use explicit
negation [16] to allow negative literals of the form −C(a) in the action language.
A literal in Lit is said to be a simple literal (or a simple assertion) if it has the form
B(a) or r(a, b) or −B(a) or −r(a, b), where B ∈ BCKB is a base concept in KB ,
r ∈ NR,KB and a, b ∈ NI,KB . Observe that {a}(c) and −{a}(c) are simple literals,
while (∃r.C)(a) and −(∃r.C)(a) are non-simple litterals.
In order to deal with existential restrictions, in addition to the individual names
NI,KB occurring in the KB we introduce a finite set Aux of auxiliary individual names,
as proposed in [23] to encode EL⊥ inference in Datalog, where Aux contains a new
individual name auxAv∃r.B , for each inclusion A v ∃r.B occurring in the KB . We
require that the names in Aux are contained in C. Let ∆ = NI,KB ∪ Aux be the
enlarged set of named individuals.
A state S is a set of literals in Lit. A state S is consistent if it is not the case that
both a literal and its complement belong to S, nor that ⊥ ∈ S. A state S is complete
if the following conditions hold: for all assertions C(a) ∈ Lit, either C(a) ∈ S or
−C(a) ∈ S; and for all assertions r(a, b) ∈ Lit, either r(a, b) ∈ S or −r(a, b) ∈ S.
Definition 2 (Action theory). Given a set of actions Σ, a set P red of predicate sym-
bols and an EL⊥ knowledge base KB = (T , A) an action theory is a tuple (KB , Π,
Frame), where:
– KB = (T , A) is an EL⊥ knowledge base;
– Π is a set of laws: action, causal, executability and initial state laws (see below);
– Frame is a set of positive literals, the set of fluents to which inertia applies1 .
The notion of frame fluents was first introduced in [24].
We introduce action theory laws adopting a notation similar to those used in [9, 22,
21, 13]. Action laws describe the direct effects of actions. They have the form:
α causes φ if ψ1 after ψ2
meaning that the execution of action α in a state in which ψ2 holds causes φ to hold
in the new state as a direct effect, if ψ1 holds in the new state as well, where: α is an
action name2 , φ is a literal in Lit and ψi = L1 ∧ . . . ∧ Lm , not Lm+1 ∧ . . . ∧ not Ln
is a conjunction of literals Li ∈ Lit or their default negations.
1
For simplicity of exposition, here we consider a single set of frame fluents, but different sets
of frame fluents, for distinct actions, could be introduced as done in [26] for occluded fluents.
2
In the C+ action description language [21] this kind of action laws would be written as caused
φ if ψ1 after α ∧ ψ2 . In practice, an action name can have parameters also occurring in φ, ψ1
and ψ2 , and a parametric action law is a shorthand for all the instances with individual names.
Non-deterministic effects of actions can be defined using default negation in the
body of action laws. For instance, after flipping a coin, it may be head or not:
f lip causes head if not − head
f lip causes −head if not head
Causal laws describe indirect effects of actions. They have the form:
caused φ if ψ1 after ψ2
meaning that ψ1 causes φ to hold whenever ψ2 holds in the previous state; φ is a literal
in Lit and ψ1 and ψ2 are conjunctions of literals or default negations of literals, as
above. Both static and dynamic causal laws are allowed. In particular, a causal law is
said static, when the condition ψ2 is >. In such a case, we will write the causal law
as caused φ if ψ1 . Observe that, differently from [5, 4], we do not restrict direct and
indirect effects of actions to be simple literals.
Precondition laws describe the executability conditions of actions. They have the
form: α executable if ψ, meaning that the execution of action α is possible in a state
where the precondition ψ holds; α is an action name and ψ is a conjunction of literals
or default negations of literals.
The constraints define conditions that must be satisfied by all states. They have the
form: ⊥ if ψ, meaning that any state in which ψ holds is inconsistent.
Initial state laws are needed to introduce conditions that have to hold in the initial
state. They have the form: Init φ if ψ. When φ = ⊥, we get the a constraint on the
initial state Init ⊥ if ψ.
Persistency of frame fluents from a state to the next one can be captured by intro-
ducing in Π a set of causal laws, said persistency laws for all fluents p ∈ Frame:
caused p if not − p after p
caused −p if not p after −p
meaning that, if p holds in a state, then p will hold in the next state, unless its negation
−p is caused to hold (and similarly for −p). Persistency of a fluent is blocked by the
execution of an action which causes the value of the fluent to change, or by a nondeter-
ministic action which may cause it to change. The persistency laws above play the role
of inertia rules in C [22], C+ [21] and K [13].
If p is a non-frame fluent, p is not expected to persist and may change its value when
an action α is executed. We can introduce non-frame laws to guarantee, for some fluent
p, that in the new state obtained by executing an action, either p or −p holds:
caused p if not − p
caused −p if not p
In the following we assume that persistency laws and non-frame laws can be ap-
plied to simple literals but not to non-simple ones, whose value in a state is determined
from the value of simple fluents. For simple literals, one has to choose whether the cor-
responding concept is frame or non-frame (so that either persistency laws or non-frame
laws are introduced). In particular, we assume that all the nominals are always (implic-
itly) in Frame: if {a}(b) (respectively −{a}(b)) belongs to a state, it will persist to the
next state unless it is cancelled by the direct or indirect effects of an action.
ABox assertions may incompletely specify the initial state. As we want to reason
about states corresponding to EL⊥ interpretations, we assume that the laws:
Init p if not − p
Init −p if not p
for completing the initial state are introduced in Π for all simple literals p (including
assertions with nominals). As shown in [20], the assumption of complete initial states,
together with suitable conditions on the laws in Π, gives rise to semantic interpretations
(extensions) of the domain description in which all states are complete. In particular, to
guarantee that each state is complete for simple literals we assume that, either a simple
literal is frame, and persistency laws are introduced for it, or it is non-frame, and non-
frame laws are introduced. The other fluents are not subject to this requirement but, as
we will see below, the value of existential literals in a state will be determined from the
value of simple ones.
Any action theory (KB , Π, Frame), where KB = (T , A), has to contain a set
of domain constraints and causal laws, to guarantee that any consistent state S of the
action theory respects the semantics of DL concepts in the KB . Observe that, if a state
is consistent, then C(x) and −C(x) (nor r(x, y) and −r(x, y)) cannot both occur in it.
Let ΠKB be the following set of laws:
(1) ⊥ if ⊥(a)
(2) caused >(x) if >
(3) caused {a}(a) if >
(4) caused exists r B(x) if r(x, y) ∧ B(y)
(5) caused (∃r.B)(x) if exists r B(x)
(6) caused −(∃r.B)(x) if not exists r B(x)
(7) ⊥ if {a}(x) ∧ B(x) ∧ not B(a), for x 6= a
(8) ⊥ if {a}(x) ∧ B(a) ∧ not B(x), for x 6= a
(9) ⊥ if {a}(x) ∧ r(z, x) ∧ not r(z, a), for x 6= a
for all x, y ∈ ∆, a ∈ NI,KB , B ∈ BCKB (the base concepts occurring in KB ) and
r ∈ NR,KB (the roles occurring in KB ). Observe that the first constraint has the effect
that a state S, in which the concept ⊥ has an instance, is made inconsistent. Law (4)
makes exists r B(x) hold (where exists r B is an additional auxiliary predicate for
any B ∈ BCKB ) in any state in which there is a domain element y such that r(x, y)
and B(y) hold. Then, laws (5) and (6) guarantee that, for all x ∈ ∆, either (∃r.B)(x) or
−(∃r.B)(x) is contained in the state. State constraints (7-9) are needed for the treatment
of nominals and are related to the materialization calculus rules (27-29) [23]. As we
will see in Section 4, the laws in ΠKB guarantee that any state corresponds to an EL⊥
interpretation.
In general, we are interested in the states which are consistent with the TBox T . We
say that a state S is consistent with the TBox T if there is an interpretation (∆I , ·I ) such
that (∆I , ·I ) is a model of T and (∆I , ·I ) satisfies the state S.
Consistency of a state S with the TBox T can be checked in EL⊥ by defining a
knowledge base (T 0 , A0 ) such that the ABox A0 contains all the assertions in S + , and
T 0 contains all the inclusions in T as well as, for each assertion C(a) ∈ S − , an inclu-
sion {a} u C v ⊥ and, for each assertion r(a, b) ∈ S − , an inclusion {a} u ∃r.{b} v ⊥.
Hence, verifying that a state S satisfies the TBox T amounts to verifying the consis-
tency of the EL⊥ knowledge base (A0 , T 0 ), which can be polynomially reduced to a
subsumption problem and decided in polynomial time [2].
Let us consider the example from the introduction.
Example 1. Let KB = (T , A) be a knowledge base such that T = {∃Teaches.Course v
Teacher } and A= { Person(john), Course(cs1 )}. We assume that all simple asser-
tions are frame, i.e., Frame= {Person(x ), Teacher (x ), Course(x ), Teaches(x , y):
for all x, y ∈ ∆},
Let us consider a state S0 where John does not teach any course. If an action
Assign(cs1 , john) is executed in S0 and Π contains:
caused Teaches(john, cs1 ) if Assign(cs1 , john)
the resulting state would contain Teaches(john,cs1) and ∃Teaches. Course(john), but
not Teacher(john), thus violating the inclusion in T . If the causal law:
caused Teacher (x ) if Teaches(x , y) ∧ Course(y)
were present in Π, Teacher(john) would be caused to hold in the resulting state (let
us call it S1 ) which would then be consistent with the TBox. In S1 Person(john),
Course(cs1), Teaches(john,cs1) and Teacher(john) hold.
Suppose now that the action Change to seminar(cs1) is executed in S1 with the
effect that cs1 becomes a seminar and it is not a course any more, i.e., in state S2 ,
−Course(cs1) holds. By law (6) in ΠKB , −(∃Teaches.Course)(john) also holds.
Should we conclude that John is not a teacher any more? As we have included the
concept Teacher among frame fluents, once John has been recognized to be a teacher,
he would remain such until some action (e.g., retiring) causes him not to be a theacher
any more. Indeed, Teacher(john) still holds in S2 by persistence.
Consider, now, the case when action retire(john) is executed in S1 , and suppose that
the action law: caused −Teacher (john) if retire(john) is in Π. Then, −Teacher (john)
will belong to the new state (let us call it S20 ), but S20 will still contain the literals:
Course(cs1), Teaches(john,cs1). Hence, S20 would violate the TBox. To avoid this Π
should contain some causal law which allows to avoid inconsistency, for instance,
caused −Teaches(x , y) if −Teacher (x ) ∧ Course(y) after Teaches(x , y)
By this causal law, when John retires he stops teaching all the courses he was teaching
before. In particular, he stops teaching cs1.
As we will see in Section 5, the causal laws that are needed to restore consistency when
an action is executed can in essence be obtained from the inclusions in the TBox and
from their contrapositives, even though not all the contrapositives are always wanted.
4 Semantics of actions
In the previous section, we have defined a state of an action theory as a set of literals.
Two options can be considered: either the state provides a complete description of the
world and is intended to represent an interpretation of the knowledge base; or the state
represents an incomplete specification of the world, which essentially is intended to
describe what is known to hold in the knowledge base.
As already mentioned, in the paper we consider the first option, in agreement with
the approaches in [5, 6, 11, 4, 1] where, in essence, actions have the effect of updating
interpretations. In particular, in this section, we define a semantics of the action theory
introduced in the previous section based on the answer set semantics.
Given an action theory (KB , Π, Frame), we want to determine the sequences of
actions executable according to the action theory by determining: (1) the initial states
and (2) the transition relation among states. Concerning the first point, we have the
following definition:
Definition 3. A state S0 is an initial state of an action theory (KB , Π, Frame) if
(1)S0 is an answer set of the program Pinit defined as follows:
Pinit = {φ ← ψ : Init φ if ψ ∈ Π} ∪ {φ ← ψ : caused φ if ψ ∈ Π} ∪
{⊥ ← ψ : ⊥ if ψ ∈ Π}
(2) S0 satisfies the TBox T
Observe that Pinit is defined as a set of rules, an ASP program obtained from the initial
state laws, as well as from the static causal laws and the state constraints (which hold
for all the states). Given an ABox A, initial state laws are introduced to constrain the
initial state of the action theory to satisfy ABox assertions. Let us call this set of laws
ΠA . In particular, for each assertion C(a) (resp., r(a, b)) in the ABox A, we introduce
in ΠA a law Init C(a) if > (resp., Init r(a, b) if >). Remember that, to make the
initial state complete for simple literals, for all the fluents f of the form B(a) or r(a, b),
with B ∈ BCKB , r ∈ P redR and a, b ∈ ∆, the laws Init f if not − f and Init −f
if not f are assumed to be in Π. We also assume that ΠA ⊆ Π.
Similarly to the initial state, any state of the action theory is required to satisfy all
state constraints and static causal laws in Π. And we define a state S to be admissible
for Π if it is an answer set of the program: Padmissible = {φ ← ψ : caused φ if ψ
∈ Π} ∪ {⊥ ← ψ : ⊥ if ψ ∈ Π}
The following proposition shows that, for any consistent state S satisfying the laws
in ΠKB , there is an EL⊥ interpretation satisfying the positive assertions in S and fal-
sifying the negative ones. Given a consistent state S, we let S + be the set of EL⊥
assertions C(a) (resp., r(a, b)), such that C(a) ∈ S (resp., r(a, b) ∈ S), and S − be the
set of EL⊥ assertions C(a) (resp., r(a, b)), such that −C(a) ∈ S (resp., −r(a, b) ∈ S).
Proposition 1. Let ΠKB ⊆ Π and let S be a consistent state admissible for Π. Then
there is an interpretation (∆I , ·I ) that satisfies all the assertions in S + and does not
safisfy any of the assertions in S − (and we say that (∆I , ·I ) satisfies the state S).
Proof. (Sketch) Let ∼ be a relation on ∆ defined as follows: a ∼ b if and only if
{b}(a) ∈ S. It can be shown by laws (3), (7), (8) that ∼ is an equivalence relation. We
define the interpretation (∆I , ·I ) as follows: ∆I = ∆/ ∼ is the quotient set of ∆ by
∼; for all a ∈ ∆, we let aI = [a]∼ ; for all concept names B ∈ BCKB and a ∈ ∆,
we let aI ∈ B I iff B(a) ∈ S; for all role names r ∈ NR,KB and a, b ∈ ∆, we let
(aI , bI ) ∈ rI iff r(a, b) ∈ S. It is easy to prove that the interpretation (∆I , ·I ) is well
defined and that it satisfies S. 2
Observe that, in general, if a state S is admissible for Π and ΠKB ⊆ Π, S is not
guaranteed to be complete for all assertions, i.e. that for all assertions C(a) (or r(a, b))
either C(a) ∈ S or −C(a) ∈ S. However, the initial state is guaranteed to be complete
for all assertions, due to the presence of initial state laws and to laws (4-6) in ΠKB .
Given a state S, which is consistent and complete for assertions, we want to define
a next-state relation to determine the set of possible resulting states when a given action
is executed in S. Given Π, we define the set of direct effects of action α, when executed
in the state S, as follows:
Dir Eff (α, S, Π) = {φ ← ψ1 : α causes φ if ψ1 after ψ2 ∈ Π and S |= ψ2 }
where the satisfiability of a condition ψ in a state S is defined as follows: S |= L1 ∧
. . . ∧ Lm , not Lm+1 ∧ . . . ∧ not Ln iff S |= Li , for all i = 1, . . . , m, and S 6|= Lj , for
all j = m + 1, . . . , n, where, for a literal L, S |= L iff L ∈ S.
Observe that this is the usual definition of satisfiability of a clause body in ASP, as
the precondition ψ of an action law is a conjunction of literals or their default negation.
Similarly, we define the set of indirect effects rules in a state S, i.e., the set of causal
rules that are available in the resulting state, when an action is executed in state S:
Indir Eff (S, Π) = {φ ← ψ1 : caused φ if ψ1 after ψ2 ∈ Π and S |= ψ2 }
Note that both Dir Eff (α, S, Π) and Indir Eff (S, Π) are sets of ASP rules.
Let us now consider the execution of an action α in a state S. We define the condi-
tions that a state S 0 has to satisfy to be a resulting state of the execution of α in S. Let
α
PS,Π be the set containing the direct effects of action α in S and the indirect effects
rules introduced from the causal laws whose after precondition is satisfied in S:
α
PS,Π = Dir Eff (α, S, Π)∪ Indir Eff (S, Π)
α
PS,Π is a set of ASP facts and rules, i.e., an ASP program. Remember that Π con-
tains the persistency laws for all frame fluents which, in particular, allow to deal with
persistency of the positive and negative assertions from the state S to the new state S 0 .
In the following definition, we introduce a transition relation from states to states.
A first requirement for the new state S 0 is that it is an answer set of PS,Π
α
. A further
requirement is that the action α is executable in the state S. An action α is executable
in the state S if there is an executability law ”α executable if ψ” in Π and S |= ψ.
Definition 4 (Transition relation). Let S be a state consistent and complete for asser-
tions. S 0 is a possible result of the execution of action α in S wrt Π, if S 0 is an answer
α
set of PS,Π and α is executable in S. The set of possible results of the execution of α in
S wrt Π is Res(α, S, Π).
It is possible to show that any state S 0 ∈ Res(α, S, Π) is consistent and complete
for assertions (if S is so) given our assumptions that frame/non-frame laws are intro-
duced for all simple literals. However, as we have seen from the examples, according to
the actions specification, S 0 might not satisfy the TBox T . The requirement that S 0 sat-
isfies the TBox T can nevertheless be incorporated in the transition relation. In fact, for
a state S which is complete for assertions, the verification that S satisfies a TBox T (in
normal form) can be reduced to the verification that S satisfies a set of state constraints.
We associate with T a set ΠT containing the state constraints:
– ⊥ if A(x) ∧ not D(x), for each A v D in T ;
– ⊥ if A(x) ∧ B(x) ∧ not D(x), for each A u B v D in T ;
– ⊥ if A(x) ∧ not (∃r.B)(x), for each A v ∃r.B in T ;
– ⊥ if (∃r.B)(x) ∧ not D(x), for each ∃r.B v D in T ;
where A, B ∈ BCKB , D ∈ BCKB ∪ {⊥} and x ∈ ∆. For D = ⊥, the condition
not D(x) is omitted. It is easy to see that:
Proposition 2. Given a state S which is consistent and complete for assertions, S sat-
isfies T if and only if S satisfies the state constraints in ΠT .
This result motivates the following definition of the transition relation.
Definition 5 (Transition relation satisfying T ). Let S be a state consistent and com-
plete for assertions satisfying T . S 0 is a possible result of the execution of action α in
0 0
S satisfying T , written S ⇒α T S , if S ∈ Res(α, S, Π ∪ ΠT ).
Definition 6. Let S be a state consistent and complete for assertions satisfying T . A
state S 0 is reachable from S through the action sequence α1 , . . . , αk , written S ⇒Tα1 ,...,αk
S 0 , if there is a sequence of states S = S0 , S1 , . . . , Sk = S 0 such that Si−1 ⇒α T Si ,
i
for i = 1, . . . , k. In this case, we say that α1 , . . . , αk is executable in S wrt. T .
Besides determining for a given initial state S0 of an action theory (KB , Π, Frame)
whether an action sequence α1 , . . . , αk is executable in S0 wrt. T (executability prob-
lem), we want to determine, for a given assertion φ, if φ holds in all the states resulting
from the execution of α1 , . . . , αk in any initial state (temporal projection problem).
Definition 7 (Projection). Given an action theory (KB , Π, Frame), an assertion φ,
and a sequence α1 , . . . , αk of actions, φ is a consequence of applying α1 , . . . , αk in A
wrt. T if, for all states S and S 0 such that S is an initial state of (KB , Π, Frame) and
S ⇒α T
1 ,...,αk
S 0 , it holds that S 0 |= φ.
5 TBox axioms and causal laws to repair inconsistencies
A further problem is that of determining, for an action theory, whether an action spec-
ification is consistent with a TBox [4]. Given an action theory (KB , Π, Frame), the
action specification (Π, Frame) is consistent with the TBox T if for all pairs of states
S, S 0 and all actions α, if S is consistent, complete for assertions, and it satisfies T , α
is executable and S 0 ∈ Res(α, S, Π), then S 0 satisfies T .
Given S and α, it may be the case that even though there is some S 0 ∈ Res(α, S, Π),
there is no resulting state that satisfies the TBox (i.e., Res(α, S, Π ∪ ΠT ) = ∅). As ob-
served in [4], when this happens, the action specification can be regarded to be under-
specified as it is not able to capture the dependencies among fluents which are specified
in the TBox. To guarantee that the TBox is satisfied in the new state, causal laws are
needed which allow the state to be repaired.
In general, while defining a domain description, one has to choose which causal
relationships are intended by the inclusions and which are not. The choice depends on
the domain and should not be done automatically, although sufficient conditions that
guarantee the consistency of action specifications and TBoxs can be defined.
The case of a (normalized) inclusion A v B, with A, B ∈ NC , is relatively simple;
the execution of an action α with effect A(c) (but not B(c)), in a state in which none
of A(c) and B(c) holds, would lead to a state which violates the constraints in the KB .
Similarly for an action β with effect −B(c). Deleting B(c) should cause A(c) to be
deleted as well, if we want the inclusion A v B to be satisfied. Hence, to guarantee
that the TBox is satisfied in the new state, for each inclusion A v B, two causal laws
are needed:
caused B(x) if A(x) and caused −A(x) if −B(x).
For an axiom A u B v ⊥, consider the concrete case pending u approved v
⊥, representing mutually exclusive states of a claim in a process of dealing with an
insurance claim, we expect the following causal laws to be included:
caused −pending(x) if approved(x) after −approved(x)
caused −approved(x) if pending(x) after −pending(x)
even though the second one is only useful if a claim can become pending again after
having become (temporarily) approved.
In the same domain, an axiom ∃approved by.clerk v approved could have the
associated causal law:
caused approved(x) if (∃approved by.clerk)(x)
If we admit that the claim, after being approved by a clerk, can be made −approved by
a supervisor, we could also add:
caused −approved by(x, y) if −approved(x)∧clerk(y) after approved by(x, y)
while we do not expect clerk to possibly change as a side effect.
Proposition 3. Given an action theory (KB , Π, Frame), a sufficient condition to guar-
antee the consistency of an action specification Π with a TBox T , is that, for each
inclusion in normal form occurring in T , Π contains a set of causal laws, as follows:
– For A v B in T , the laws: 1) caused B(x) if A(x); 2) caused −A(x) if −B(x).
– For A u B v D, the laws: (3) caused D(x) if A(x) ∧ B(x); and at least one of (4)
caused −A(x) if −D(x) ∧ B(x) and (5) caused −B(x) if −D(x) ∧ A(x)
– For A v ∃r.B, the laws: (6) caused r(x, auxAv∃r.B ) if A(x);
(7) caused B(auxAv∃r.B ) if A(x) ; (8) caused −A(x) if −(∃r.B)(x);
– For ∃r.B v A, the laws: (9) caused A(x) if (∃r.B)(x);
(10) caused −(∃r.B)(x) if −A(x);
at least one of: (11) caused −r(x, y) if −A(x) ∧ B(y)
(12) caused −B(y) if −A(x) ∧ r(x, y)
Observe that for A v ∃r.B, causal laws (6-7) here, together with (4-5) in ΠKB , are
such that (∃r.B)(x) is also caused.
6 Encoding the action theory in ASP
In this section, we show how to translate a domain description to standard ASP.
States are represented in ASP as integers, starting with the initial state 0. We will use
the predicates occurs(Action, State), next(State, State) and holds(Fluent, State).
Predicate next(S, SN ) means that SN is the next state of S:
next(S , SN ) ← state(S ), SN = S + 1 .
Occurrence of exactly one action in each state must be encoded:
−occurs(A, S ) ← occurs(A1 , S ), action(A), action(A1 ), A 6= A1 , state(S ).
occurs(A, S) ← not − occurs(A, S), action(A), state(S).
To represent the fact that a literal holds in a state, we use different predicates for
the fluents that correspond to EL⊥ assertions and for other fluents. In particular, we
introduce the predicates holds inst(Concept, Name, State) and holds triple(Role,
Name, Name, State) to represent the fact that an assertions of the form C(a) (resp.,
r(a, b)) hods in a state. Instead, we use the predicate holds(Fluent, State) for the flu-
ents p(a1 , . . . , an ) which are not assertions.
The laws Π can be translated as follows: An action law α causes L0 if ψ1 after
ψ2 , where ψ1 = L1 ∧ . . . ∧ Lm , not Lm+1 ∧ . . . ∧ not Ln and ψ2 = L01 ∧ . . . ∧
L0m , not L0m+1 ∧ . . . ∧ not L0n is translated to:
h0 ← state(S), S 0 = S + 1, occurs(a, S), h1 . . . hm , not hm+1 . . . not hn ,
h01 . . . h0m , not h0m+1 . . . not h0n
where h0 = (−)holds inst(C0 , a0 , S 0 ) if L0 = (−)C0 (a0 ), h0 = (−)holds triple(r0 ,
a0 , b0 , S 0 ), if L0 = (−)r0 (a0 , b0 ), and h0 = (−)holds(p(a1 , .., an ), S 0 ) if L0 = (−)
p(a1 , .., an ) and similarly for the hi ’s and h0j ’s, using S 0 for the hi ’s and S for the h0j ’s
(where C0 in holds inst stands for the ground term representing C0 , and similarly
p(a1 , .., an ) within holds stands for the corresponding ground term).
A dynamic causal law caused L0 if ψ1 after ψ2 , where ψ1 = L1 ∧. . .∧Lm , not Lm+1 ∧
. . . ∧ not Ln and ψ2 = L01 ∧ . . . ∧ L0m , not L0m+1 ∧ . . . ∧ not L0n is translated to:
h0 ← state(S ), S 0 = S + 1 , h1 . . . hm , not hm+1 . . . not hn ,
h10 . . . hm0 0
, not hm+1 . . . not hn0
where the hi ’s and hj ’s are defined as before, using S 0 for the hi ’s and S for the h0j ’s.
0
A precondition law α executable if L1 ∧ . . . ∧ Lm , not Lm+1 ∧ . . . ∧ not Ln is
translated to the following two ASP rules, where the hi ’s are defined as before using S
and the predicate executable(Action, State):
← state(S ), occurs(A, S ), not executable(A, S )
executable(A, S ) ← h1 . . . hm , not hm+1 . . . not hn
A constraint ⊥ if L1 ∧ . . . ∧ Lm , not Lm+1 ∧ . . . ∧ not Ln is translated to the following
ASP constraint, where the hi ’s are defined as before using S:
← state(S), occurs(a, S), h1 . . . hm , not hm+1 . . . not hn
Initial state laws are translated in a similar way but they are evaluated in state 0.
Given a domain description (KB , Π, Frame), we denote by tr(Π) the set of rules
containing the translation of each law in Π, including those in ΠKB , ΠA and in ΠT ,
as well as the definitions of occurs and next introduced above.
Proposition 4. Given an action theory (KB , Π, Frame), let tr(Π) be the encoding of
Π as defined above. The following holds:
– To check for the executability of an action sequence act1, act2, . . . , actn, the facts:
occurs(act1, 0), occurs(act2, 1), . . . , occurs(actn, n − 1) should be included in
tr(Π). The sequence is executable when tr(Π) has an answer set.
– To check whether a given literal L = (−)C(a) (or (−)r(a, b)) holds in some of the
resulting states after executing the action sequence act1, act2, . . . , actn from an
initial state, one has to look for an answer set of tr(Π) enriched with the following:
• occurs(act1, 0), occurs(act2, 1), . . . , occurs(actn, n − 1),
• the constraint ← not (−)holds inst(C, a, n) if L = (−)C(a)
• the constraint ← not (−)holds triple(R, a, b, n) ) if L = (−)r(a, b)
– For the temporal projection problem, checking whether a literal L = (−)C(a)
(or (-)r(a, b)) holds in all the possible resulting states after executing the action
sequence act1, act2, . . . , actn from an initial state, amounts to checking the non-
existence of answer sets when the following rules are added to tr(Π):
• occurs(act1, 0), occurs(act2, 1), . . . , occurs(actn, n − 1)
• the constraint ← (−)holds inst(C, a, n) if L = (−)C(a)
• the constraint ← (−)holds triple(R, a, b, n) ) if L = (−)r(a, b)
Notice that size of the ASP encoding is polynomial in the size of the action theory.
7 Conclusions and Related Work
In this paper we have proposed an approach for reasoning about actions in an action
language that includes a knowledge base in EL⊥ and allows for causal laws and non-
deterministic actions. We have provided a semantics for the action language based on
Answer Sets as well as a polynomial ASP encoding of a domain description. It follows
that the temporal projection problem in our action logic is a co-NP problem and that it
can be solved by using standard ASP solvers.
Many of the proposals in the literature for combining DLs with action theories fo-
cus on expressive DLs. In their seminal work [5], Baader et al. study the integration of
action formalisms with expressive DLs, from ALC to ALCOIQ, under Winslett’s pos-
sible models approach (PMA) [29], based on the assumption that TBox is acyclic and
on the distinction between defined and primitive concepts (i.e., concept names that are
not defined in the TBox), where only primitive concepts are allowed in action effects.
They determine the complexity of the executability and projection problems and show
that they get decidable fragments of the situation calculus. Our semantics departs from
PMA as causal laws are considered. As [26] and [4] we do not require acyclic TBoxes
and primitive concepts in postconditions.
The requirement of acyclic TBoxes is lifted in the paper by Liu et al. [26], where an
approach to the ramification problem is proposed which does not use causal relation-
ships, but exploits occlusion to provide a specification of the predicates that can change
through the execution of actions. The idea is to leave to the designer of an action de-
scription the control of the ramification of the actions.
Similar considerations are at the basis of the approach by Baader et al. [4] that, in-
stead, exploit causal relationships for modeling ramifications. They define an action lan-
guage for ALCO, which deals with the ramification problem using causal relationships
and provide a semantics for it in the style of McCain and Turner fixpoint semantics.
They show that temporal projection is decidable and E XP T IME-complete. Their action
theory does not deal with non-deterministic effects of actions. In this paper, following
[4], we exploit causal laws for modeling ramifications in the context of an action lan-
guage for EL⊥ . We allow for non-deterministic effects of actions and for the distinction
between frame and non-frame fluents [24] (which is strongly related to occlusion used
in [26]) based on the answer set semantics. We also provide sufficient conditions for an
action specification to be consistent with a normalized EL⊥ KB .
Ahmetai et al. [1] study the evolution of Graph Structured Data as a result of updates
expressed in an action language. They provide decidability and complexity results for
expressive DLs such as ALCHOIQbr (under finite satisfiability) as well as for vari-
ants of DL-lite. Complex actions including action sequence and conditional actions are
considered. Complex actions are considered as well in [11], where an action formalism
is introduced for a family DLs, from ALCO to ALCHOIQ, exploiting PDL program
constructors to define complex actions. As in [5], the TBox is assumed to be acyclic.
In [8] Description Logic and Action Bases are introduced, where an initial Abox
evolves over time due to actions which have conditional effects. In the basic approach,
if the resulting state it inconsistent, is not considered; in [10] the approach is extended
to allow for different notions of repairing the resulting state: either a maximal subset
that is consistent with the Tbox, or the intersection of all such subsets. In this paper,
we rely on causal laws for repairing states; selecting the appropriate causal laws means
acquiring more knowledge, and it allows for a finer control of the resulting state.
In [14] a language, dl-programs, is proposed which combines logic programming,
under the answer set semantics, and the expressive description logics SHIF(D) and
SHOIN (D). In this paper, instead, we do not propose a general language paradigm,
but we provide a semantics of EL⊥ action theories based on answer sets, that can be
easily encoded in ASP borrowing some ideas from the materialization calculus in [23].
The system DReW [15] provides an implementation of dl-programs for two DLs, in-
cluding SROEL(u, ×), also using the materialization calculus in [23]. However, as in
our approach states are complete for EL⊥ assertions, and correspond to EL⊥ interpre-
tations, we do not need to perform inference in EL⊥ , but just model checking.
Our semantics for actions requires, as in many proposals in the literature, that the
state provides a complete description of the world and is intended to represent an in-
terpretation of the knowledge base. Alternatively, as in [8], a state could represent an
incomplete specification of the world, which describes what is known about the world.
In this way, one can avoid, for a given ABox, to consider as initial states all the complete
states consistent with it and with the TBox. Rather, one can consider a single initial state
as an epistemic state representing what is known and what is unknown. We leave the
study of this alternative approach for future work.
Our proposal is related to the approach to action reasoning in ASP proposed in [20],
where verification of LTL temporal properties of an action theory is encoded in ASP
through bounded model checking. As future work, we aim at incorporating verification
of temporal properties also in the approach proposed in this paper.
Acknowledgements. This research is partially supported by INDAM - GNCS Project
2016 Ragionamento Defeasible nelle Logiche Descrittive.
References
1. Ahmetaj, S., Calvanese, D., Ortiz, M., Simkus, M.: Managing change in graph-structured
data using description logics. In: Proceedings of the Twenty-Eighth AAAI Conference on
Artificial Intelligence. pp. 966–973 (2014)
2. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: Kaelbling, L., Saffiotti, A.
(eds.) Proc. IJCAI 2005. pp. 364–369. Edinburgh, Scotland, UK (August 2005)
3. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: LTCS-Report LTCS-05-01.
Inst. for Theoretical Computer Science, TU Dresden (2005)
4. Baader, F., Lippmann, M., Liu, H.: Using causal relationships to deal with the ramification
problem in action formalisms based on description logics. In: LPAR-17. pp. 82–96 (2010)
5. Baader, F., Lutz, C., Milicic, M., Sattler, U., Wolter, F.: Integrating description logics and
action formalisms: First results. In: Proc. AAAI 2005. pp. 572–577 (2005)
6. Baader, F., Liu, H., ul Mehdi, A.: Verifying properties of infinite sequences of description
logic actions. In: ECAI. pp. 53–58 (2010)
7. Babb, J., Lee, J.: Cplus2asp: Computing action language C+ in Answer Set Programming.
In: Proc. Logic Programming and Nonmonotonic Reasoning, LPNMR 2013. pp. 122–134
(2013)
8. Bagheri Hariri, B., Calvanese, D., Montali, M., De Giacomo, G., De Masellis, R., Felli, P.:
Description logic knowledge and action bases. J. Artif. Intell. Res. 46, 651–686 (2013)
9. Baral, C., Gelfond, M.: Reasoning agents in dynamic domains. In: Logic-Based Artificial
Intelligence, pp. 257–279 (2000)
10. Calvanese, D., Kharlamov, E., Montali, M., Santoso, A., Zheleznyakov, D.: Verification of
inconsistency-aware knowledge and action bases. In: Proc. IJCAI 2013
11. Chang, L., Shi, Z., Gu, T., Zhao, L.: A family of dynamic description logics for representing
and reasoning about actions. J. Autom. Reasoning 49(1), 1–52 (2012)
12. Denecker, M., Theseider Dupré, D., Van Belleghem, K.: An inductive definitions approach
to ramifications. Electronic Transactions on Artificial Intelligence 2, 25–97 (1998)
13. Eiter, T., Faber, W., Leone, N., Pfeifer, G., Polleres, A.: A logic programming approach to
knowledge-state planning: Semantics and complexity. ACM Transactions on Computational
Logic 5(2), 206–263 (2004)
14. Eiter, T., Ianni, G., Lukasiewicz, T., Schindlauer, R., Tompits, H.: Combining answer set
programming with description logics for the semantic web. Artificial Intellgence 172(12-13)
(2008)
15. Eiter, T., Krennwallner, T., Schneider, P., Xiao, G.: Uniform evaluation of nonmonotonic
dl-programs. In: Foundations of Information and Knowledge Systems - 7th International
Symposium, FoIKS 2012, Kiel, Germany, March 5-9, 2012. Proceedings. pp. 1–22 (2012)
16. Gelfond, M.: Handbook of Knowledge Representation, chapter 7, Answer Sets. Elsevier
(2007)
17. Gelfond, M., Lifschitz, V.: Action languages. Electron. Trans. Artif. Intell. 2, 193–210 (1998)
18. Giordano, L., Martelli, A., Schwind, C.: Ramification and causality in a modal action logic.
J. Log. Comput. 10(5), 625–662 (2000)
19. Giordano, L., Martelli, A., Schwind, C.: Reasoning about actions in dynamic linear time
temporal logic. The Logic Journal of the IGPL 9(2), 289–303 (2001)
20. Giordano, L., Martelli, A., Theseider Dupré, D.: Reasoning about actions with temporal
answer sets. Theory and Practice of Logic Programming 13, 201–225 (2013)
21. Giunchiglia, E., Lee, J., Lifschitz, V., McCain, N., , Turner, H.: Nonmonotonic causal theo-
ries. Artificial Intelligence 153(1-2), 49–104 (2004)
22. Giunchiglia, E., Lifschitz, V.: An action language based on causal explanation: Preliminary
report. In: Proc. AAAI/IAAI 1998. pp. 623–630 (1998)
23. Krötzsch, M.: Efficient inferencing for OWL EL. In: Proc. JELIA 2010. pp. 234–246 (2010)
24. Lifschitz, V.: Frames in the space of situations. Artificial Intelligence 46, 365–376 (1990)
25. Lin, F.: Embracing causality in specifying the indirect effects of actions. In: IJCAI 95,
Montréal Québec, Canada, August 20-25 1995, 2 Volumes. pp. 1985–1993 (1995)
26. Liu, H., Lutz, C., Milicic, M., Wolter, F.: Reasoning about actions using description logics
with general tboxes. In: Proc. JELIA 2006, Liverpool, UK. pp. 266–279 (2006)
27. McCain, N., Turner, H.: A causal theory of ramifications and qualifications. In: Proc. IJCAI
95. pp. 1978–1984 (1995)
28. Thielscher, M.: Ramification and causality. Artif. Intell. 89(1-2), 317–364 (1997)
29. Winslett, M.: Reasoning about action using a possible models approach. In: Proc. AAAI, St.
Paul, MN, August 21-26, 1988. pp. 89–93 (1988)