In this paper we propose an approach based on Answer Set Programming (ASP) for reasoning about actions in a domain description including knowledge 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-deterministic 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.
The integration of description logics and action formalisms has recently gained a lot
of interest [
As usual in the formalisms integrating description logics and action languages [
In case knowledge on a domain is expressed in a description logic, the issue has
been considered, e.g., in [
In this paper we define an action theory for reasoning about actions with an E L?
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. [
In particular, as in E L? negated concepts are not included, we allow ASP-like
explicit 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
semantics of other DL-based approaches to reasoning about actions [
The projection problem is reduced to the problem of computing the answer sets
of the action theory, given an underlying E L? knowledge base. In this respect, two
approaches are feasible: either to encode the action theory into a formalism which
already combines ASP and DLs, as in [
Our approach also relates to the approach to action reasoning proposed in [
The description logic E L?
We consider a fragment of the logic E L++ [
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 E L? is defined as follows:
C := A j > j ? j C u C j 9r:C j fag where A 2 NC and r 2 NR. Observe that complement, disjunction and universal restriction are not allowed in E L?.
A KB is a pair (T ; A), where T is a TBox containing a finite set of concept inclusions 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 2 NR and a; b 2 NI .
We will assume that the TBox is in normal form [
The following is the usual definition for interpretations and models.
Definition 1 (Interpretations and models). An interpretation in E L? 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 2 I . Furthermore: – >I = I , ?I = ;; – fagI = faI g; – (C u D)I = CI \ DI ; – (9r:C)I = fx 2 j 9y 2 CI : (x; y) 2 rI g.
An interpretation ( I ; I ) satisfies an inclusion C v D if CI DI ; it satisfies an assertion C(a) if aI 2 CI ; it satisfies an assertion r(a; b) if (aI ; bI ) 2 rI .
Given a KB = (T ; A), an interpretation ( I ; I ) is a model of T if ( I ; I ) satisfies 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
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
compatible 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 [
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 2 P red is a n-ary predicate symbol and a1; : : : ; an 2 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) E L? 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 2 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 9r:C occurs in the KB , there is a
predicate name 9r:C in P red and for each a 2 NI;KB , the fluent literals (9r:C)(a) and
(9r:C)(a) belong to the set Lit (sometimes we will still call such literals assertions).
Although classical negation is not allowed in E L? (as well as in ASP), we use explicit
negation [
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 2 BCKB is a base concept in KB , r 2 NR;KB and a; b 2 NI;KB . Observe that fag(c) and fag(c) are simple literals, while (9r:C)(a) and (9r: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 E L? inference in Datalog, where Aux contains a new individual name auxAv9r:B , for each inclusion A v 9r: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 ? 2 S. A state S is complete if the following conditions hold: for all assertions C(a) 2 Lit, either C(a) 2 S or
C(a) 2 S; and for all assertions r(a; b) 2 Lit, either r(a; b) 2 S or r(a; b) 2 S. Definition 2 (Action theory). Given a set of actions , a set P red of predicate symbols and an E L? knowledge base KB = (T ; A) an action theory is a tuple (KB ; ; Frame ), where: – KB = (T ; A) is an E L? 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 [
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
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 [
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
introducing in a set of causal laws, said persistency laws for all fluents p 2 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
nondeterministic action which may cause it to change. The persistency laws above play the role
of inertia rules in C [
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 applied 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 corresponding 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 (implicitly) in Frame: if fag(b) (respectively fag(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 E L? 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 [
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 fag(a) if > (4) caused exists r B(x) if r(x; y) ^ B(y) (5) caused (9r:B)(x) if exists r B(x) (6) caused (9r:B)(x) if not exists r B(x) (7) ? if fag(x) ^ B(x) ^ not B(a), for x 6= a (8) ? if fag(x) ^ B(a) ^ not B(x), for x 6= a (9) ? if fag(x) ^ r(z; x) ^ not r(z; a), for x 6= a for all x; y 2 , a 2 NI;KB , B 2 BCKB (the base concepts occurring in KB ) and r 2 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 2 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 2 , either (9r:B)(x) or (9r: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 E L? 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 E L? 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) 2 S , an
inclusion fag u C v ? and, for each assertion r(a; b) 2 S , an inclusion fag u 9r:fbg v ?.
Hence, verifying that a state S satisfies the TBox T amounts to verifying the
consistency of the E L? knowledge base (A0; T 0), which can be polynomially reduced to a
subsumption problem and decided in polynomial time [
Let us consider the example from the introduction.
Example 1. Let KB = (T ; A) be a knowledge base such that T = f9Teaches:Course v Teacher g and A= f Person(john); Course(cs1 )g. We assume that all simple assertions are frame, i.e., Frame= fPerson(x ), Teacher (x ), Course(x ); Teaches(x ; y ): for all x; y 2 g,
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 9Teaches. 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 , (9Teaches: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
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 Pinit = f : Init f? : ? if 2 g (2) S0 satisfies the TBox T if 2 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 [
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: 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 2 BCKB , r 2 P redR and a; b 2 , 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 = f : caused if 2 g [ f? : ? if 2 g
The following proposition shows that, for any consistent state S satisfying the laws in KB , there is an E L? interpretation satisfying the positive assertions in S and falsifying the negative ones. Given a consistent state S, we let S+ be the set of E L? assertions C(a) (resp., r(a; b)), such that C(a) 2 S (resp., r(a; b) 2 S), and S be the set of E L? assertions C(a) (resp., r(a; b)), such that C(a) 2 S (resp., r(a; b) 2 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 fbg(a) 2 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 2 , we let aI = [a] ; for all concept names B 2 BCKB and a 2 , we let aI 2 BI iff B(a) 2 S; for all role names r 2 NR;KB and a; b 2 , we let (aI ; bI ) 2 rI iff r(a; b) 2 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) 2 S or C(a) 2 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; ) = f 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 conditions that a state S0 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 contains 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 S0.
In the following definition, we introduce a transition relation from states to states. A first requirement for the new state S0 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 j= . Definition 4 (Transition relation). Let S be a state consistent and complete for assertions. S0 is a possible result of the execution of action in S wrt , if S0 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 S0 2 Res( ; S; ) is consistent and complete for assertions (if S is so) given our assumptions that frame/non-frame laws are introduced for all simple literals. However, as we have seen from the examples, according to the actions specification, S0 might not satisfy the TBox T . The requirement that S0 satisfies 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 (9r:B)(x), for each A v 9r:B in T ; – ? if (9r:B)(x) ^ not D(x), for each 9r:B v D in T ; where A; B 2 BCKB , D 2 BCKB [ f?g and x 2 not D(x) is omitted. It is easy to see that: . For D = ?, the condition Proposition 2. Given a state S which is consistent and complete for assertions, S satisfies 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 complete for assertions satisfying T . S0 is a possible result of the execution of action in S satisfying T , written S )T S0, if S0 2 Res( ; S; [ T ).
Definition 6. Let S be a state consistent and complete for assertions satisfying T . A state S0 is reachable from S through the action sequence 1; : : : ; k, written S )T1;:::; k S0, if there is a sequence of states S = S0; S1; : : : ; Sk = S0 such that Si 1 )Ti Si, 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 problem), 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. T1;i:f:,:;fokr Sal0l, sittahtoelsdSs tahnadt SS00 j=such. that S is an initial state of (KB ; ; Frame) and S )T 5
A further problem is that of determining, for an action theory, whether an action
specification is consistent with a TBox [
Given S and , it may be the case that even though there is some S0 2 Res( ; S; ),
there is no resulting state that satisfies the TBox (i.e., Res( ; S; [ T ) = ;). As
observed in [
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 2 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 9approved by:clerk v approved could have the associated causal law:
caused approved(x) if (9approved 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 guarantee 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 9r:B, the laws: (6) caused r(x; auxAv9r:B) if A(x);
(7) caused B(auxAv9r:B) if A(x) ; (8) caused A(x) if (9r:B)(x); – For 9r:B v A, the laws: (9) caused A(x) if (9r:B)(x); (10) caused (9r: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 9r:B, causal laws (6-7) here, together with (4-5) in such that (9r:B)(x) is also caused.
KB , are 6
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 E L? 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 fluents 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); S0 = S + 1; occurs(a; S); h1 : : : hm; not hm+1 : : : not hn; h01 : : : h0m; not h0m+1 : : : not h0
n where h0 = ( )holds inst (C0; a0; S0) if L0 = ( )C0(a0), h0 = ( )holds triple(r0; a0; b0; S0), if L0 = ( )r0(a0; b0), and h0 = ( )holds(p(a1; ::; an); S0) if L0 = ( ) p(a1; ::; an) and similarly for the hi’s and h0j ’s, using S0 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 ; not hm0+1 : : : not h0
n where the hi’s and h0j ’s are defined as before, using S0 for the hi’s and S for the h0j ’s. 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 nonexistence 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
In this paper we have proposed an approach for reasoning about actions in an action language that includes a knowledge base in E L? and allows for causal laws and nondeterministic 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
focus on expressive DLs. In their seminal work [
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 relationships, 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 description the control of the ramification of the actions.
Similar considerations are at the basis of the approach by Baader et al. [
Ahmetai et al. [
In [
In [
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
interpretation of the knowledge base. Alternatively, as in [
Our proposal is related to the approach to action reasoning in ASP proposed in [
Acknowledgements. This research is partially supported by INDAM - GNCS Project 2016 Ragionamento Defeasible nelle Logiche Descrittive. 23. Kro¨ 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,
Montre´al Que´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)