=Paper=
{{Paper
|id=Vol-2970/causalpaper3
|storemode=property
|title=Reasoning About Actions with EL(bot) Ontologies and Temporal Answer Sets
|pdfUrl=https://ceur-ws.org/Vol-2970/causalpaper3.pdf
|volume=Vol-2970
|authors=Laura Giordano,Alberto Martelli,Daniele Theseider Dupré
|dblpUrl=https://dblp.org/rec/conf/iclp/0001MD21
}}
==Reasoning About Actions with EL(bot) Ontologies and Temporal Answer Sets==
https://ceur-ws.org/Vol-2970/causalpaper3.pdf
Reasoning about actions with ℰℒ⊥ ontologies
and temporal answer sets
Laura Giordano1 , Alberto Martelli2 and Daniele Theseider Dupré 1
1
DISIT - Università del Piemonte Orientale, Alessandria, Italy
2
Dip. di Informatica - Università di Torino, Italy
Abstract
We propose an approach based on Answer Set Programming for reasoning about actions with domain
descriptions including ontological knowledge, expressed in the lightweight description logic ℰℒ⊥ . We
consider a temporal action theory, which allows for non-deterministic actions and causal rules to deal with
ramifications, and whose extensions are defined by temporal answer sets. We provide conditions under
which action consistency can be guaranteed with respect to an ontology, by a polynomial encoding of an
action theory extended with an ℰℒ⊥ knowledge base (in normal form) into a temporal action theory.
1. Introduction
The integration of description logics and action formalisms has gained a lot of interest in the
past years [5, 4, 12, 1]. In this paper we explore the combination of a temporal action logic [23]
and an ℰℒ⊥ knowledge bases, with the aim of allowing reasoning about action execution in the
presence of the constraints given by an ℰℒ⊥ ontology.
As usual in many formalisms integrating description logics and action languages [5, 6, 12, 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 action execution. In the literature of reasoning about
actions it is well known that causal laws and their interplay with domain constraints are crucial
for solving the ramification problem [33, 31, 34, 13, 18, 25]. In case knowledge about the
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 of the resulting state, after action
execution. For instance, given a TBox containing ∃Teaches.Course ⊑ Teacher , and an ABox
(i.e., a set of assertions on individuals) containing the assertion Course(𝑚𝑎𝑡ℎ), an action which
adds the assertion Teaches(john, math), without also adding Teacher (john), will not give rise
to a consistent next state with respect to the knowledge base. The addition of the causal law
□(Teacher (john) ← Teaches(john, math) ∧ Course(math)) would enforce, for instance, the
above TBox inclusion to be satisfied in the resulting state.
The approach proposed by Baader et al. [4] uses causal relationships to deal with the ramifi-
cation problem in an action formalism based on description logics, and it exploits a semantics
of actions and causal laws in the style of Winslett’s [35] and McCain and Turner’s [33] fixpoint
" laura.giordano@uniupo.it (L. Giordano); mrt@di.uniuto.it (A. Martelli); dtd@uniupo.it (D. T. )
© 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR Workshop Proceedings (CEUR-WS.org)
semantics. In this paper, we aim at extending this approach to reason about actions with an ℰℒ⊥
ontology with temporal answer sets. Reasoning about actions with temporal answer sets has been
proposed in [21, 23] by defining a temporal logic programming language for reasoning about
complex actions and infinite computations. This action language, besides the usual LTL operators,
allows for general Dynamic Linear Time Temporal Logic (DLTL) formulas to be included in
domain descriptions to constrain the space of possible extensions. In [23] a notion of Temporal
Answer Set for domain descriptions is introduced, as a generalization of the usual notion of
Answer Set, and a translation of domain descriptions into standard Answer Set Programming
(ASP) is provided, by exploiting bounded model checking techniques for the verification of DLTL
constraints, extending the approach developed by Helianko and Niemela [27] for bounded LTL
model checking with Stable Models. An alternative ASP translation of this temporal action
language has been investigated in [22, 24], by proposing an approach to bounded model checking
which exploits the Büchi automaton construction while searching for a counterexample, with the
aim of achieving completeness. Our temporal action logic has been shown to be strongly related
to extensions of the 𝒜 language [17, 9, 14, 7, 25]. The temporal formalism is also related to the
recent temporal extension of Clingo, telingo dealing with finite computations [10].
The paper studies extended temporal action theories, combining the temporal action logic
mentioned above with an ℰℒ⊥ knowledge base. It is shown that, for ℰℒ⊥ knowledge bases in
normal form, the consistency of the action theory extensions with the ontology can be verified by
adding to the action theory a set of causal laws and state constraints, by exploiting a fragment
of the materialization calculus by Krötzsch [29]. Furthermore, sufficient conditions on the
action theory can be defined to repair the states resulting from action execution and guarantee
consistency with TBox. To this purpose, for each inclusion axiom in TBox, a suitable set of
causal laws can be added to the action theory. Our approach provides a polynomial encoding of
an extended action theory, with an ℰℒ⊥ knowledge base in normal form, into the language of
the (DLTL) temporal action logic studied in [23]. The proof methods for this temporal action
logic, based on bounded model checking, can then be exploited for reasoning about actions in the
extended action theory.
A preliminary version of this work, which does not exploit a temporal action language, has
been presented in CILC 2016 [20].
2. The description logic ℰℒ⊥
We consider a fragment of the logic ℰℒ++ [2] that, for simplicity of presentation, does not
include role inclusions and concrete domains. The fragment, let us call it ℰℒ⊥ , includes the
concept ⊥ as well as nominals.
We let 𝑁𝐶 be a set of concept names, 𝑁𝑅 a set of role names and 𝑁𝐼 a set of individual names.
A concept in ℰℒ⊥ is defined as follows:
𝐶 := 𝐴 | ⊤ | ⊥ | 𝐶 ⊓ 𝐶 | ∃𝑟.𝐶 | {𝑎}
where 𝐴 ∈ 𝑁𝐶 and 𝑟 ∈ 𝑁𝑅 . Observe that complement, disjunction and universal restriction are
not allowed in ℰℒ⊥ .
A knowledge base K is a pair (𝒯 , 𝒜), where 𝒯 is a TBox containing a finite set of concept
inclusions 𝐶1 ⊑ 𝐶2 and 𝒜 is an ABox containing assertions of the form 𝐶(𝑎) and 𝑟(𝑎, 𝑏), with
𝐶, 𝐶1 , 𝐶2 concepts, 𝑟 ∈ 𝑁𝑅 and 𝑎, 𝑏 ∈ 𝑁𝐼 .
We will assume that the TBox is in normal form [3]. Let 𝐵𝐶K be the smallest set of concepts
containing ⊤, all the concept names occurring in K and all nominals {𝑎}, for any individual name
𝑎 occurring in K . An inclusion is in normal form if it has one of the following forms: 𝐶1 ⊑ 𝐷,
𝐶1 ⊓ 𝐶2 ⊑ 𝐷, 𝐶1 ⊑ ∃𝑟.𝐶2 , ∃𝑟.𝐶2 ⊑ 𝐷, where 𝐶1 , 𝐶2 ∈ 𝐵𝐶K , and 𝐷 ∈ 𝐵𝐶K ∪ {⊥}. In
[3] it is shown that any TBox can be normalized in linear time, by introducing new concept and
role names.
In the following we will denote with 𝑁𝐶,K , 𝑁𝑅,K and 𝑁𝐼,K the (finite) sets of concept names,
role names and individual names occurring in K .
Definition 1 (Interpretations and models). An interpretation in ℰℒ⊥ is any structure (∆𝐼 , ·𝐼 )
where: ∆𝐼 is a domain; ·𝐼 is an interpretation function that maps each concept name 𝐴 to set
𝐴𝐼 ⊆ ∆𝐼 , each role name 𝑟 to a binary relation 𝑟𝐼 ⊆ ∆𝐼 × ∆𝐼 , and each individual name 𝑎 to
an element 𝑎𝐼 ∈ ∆𝐼 . Furthermore: ⊤𝐼 = ∆𝐼 , ⊥𝐼 = ∅; {𝑎}𝐼 = {𝑎𝐼 }; (𝐶 ⊓ 𝐷)𝐼 = 𝐶 𝐼 ∩ 𝐷𝐼 ;
(∃𝑟.𝐶)𝐼 = {𝑥 ∈ ∆ | ∃𝑦 ∈ 𝐶 𝐼 : (𝑥, 𝑦) ∈ 𝑟𝐼 }. An interpretation (∆𝐼 , ·𝐼 ) satisfies an inclusion
𝐶 ⊑ 𝐷 if 𝐶 𝐼 ⊆ 𝐷𝐼 ; it satisfies an assertion 𝐶(𝑎) if 𝑎𝐼 ∈ 𝐶 𝐼 ; it satisfies an assertion 𝑟(𝑎, 𝑏) if
(𝑎𝐼 , 𝑏𝐼 ) ∈ 𝑟𝐼 .
Given a knowledge base K = (𝒯 , 𝒜), an interpretation (∆𝐼 , ·𝐼 ) is a model of 𝒯 if (∆𝐼 , ·𝐼 )
satisfies all inclusions in 𝒯 ; (∆𝐼 , ·𝐼 ) is a model of K if (∆𝐼 , ·𝐼 ) satisfies all inclusions in 𝒯 and
all assertions in 𝒜. 𝒜 is consistent with 𝒯 if there is a model of 𝒯 satisfying all the assertions in
𝒜.
3. Temporal Action Theories
In this paper we refer to the notion of the temporal action theory in [19], a rule based fragment of
which has been studied in [23, 24], which exploits the dynamic extension of LTL introduced by
Henriksen and Thiagarajan, called Dynamic Linear Time Temporal Logic (DLTL) [28]. In DLTL
the next state modality is indexed by actions and the until operator 𝒰 𝜋 is indexed by a program 𝜋
which, as in PDL, can be any regular expression built from atomic actions using sequence (;),
nondeterministic choice (+) and finite iteration (*). The derived modalities ⟨𝜋⟩ and [𝜋] can be
defined as: ⟨𝜋⟩𝛼 ≡ ⊤𝒰 𝜋 𝛼 and [𝜋]𝛼 ≡ ¬⟨𝜋⟩¬𝛼. Similarly, ○ (next), ◇ and □ operators of LTL
can be defined. We let Σ be a finite non-empty set of (atomic) actions and we refer to [19, 23] for
the details concerning complex actions.
A domain description Π is a set of laws describing the effects of actions and their executability
preconditions. Atomic propositions describing the state of the domain are called fluents. Actions
may have direct effects, described by action laws, and indirect effects, described by causal laws
capturing the causal dependencies among fluents.
Let ℒ be a first order language which includes a finite number of constants and variables, but
no function symbol. Let 𝒫 be the set of predicate symbols, 𝑉 𝑎𝑟 the set of variables and 𝐶𝑜𝑛𝑠 the
set of constant symbols. We call fluents atomic literals of the form 𝑝(𝑡1 , . . . , 𝑡𝑛 ), where, for each
𝑖, 𝑡𝑖 ∈ 𝑉 𝑎𝑟 ∪ 𝐶𝑜𝑛𝑠. A simple fluent literal (or s-literal) 𝑙 is an atomic literals 𝑝(𝑡1 , . . . , 𝑡𝑛 ) or its
negation ¬𝑝(𝑡1 , . . . , 𝑡𝑛 ). We denote by 𝐿𝑖𝑡𝑆 the set of all simple fluent literals. 𝐿𝑖𝑡𝑇 is the set of
temporal fluent literals: if 𝑙 ∈ 𝐿𝑖𝑡𝑆 , then [𝑎]𝑙, ○𝑙 ∈ 𝐿𝑖𝑡𝑇 , where 𝑎 is an action name (an atomic
proposition, possibly containing variables), and [𝑎] and ○ are the temporal operators introduced
in the previous section. Let 𝐿𝑖𝑡 = 𝐿𝑖𝑡𝑆 ∪ 𝐿𝑖𝑡𝑇 ∪ {⊥, ⊤}, where ⊥ represents the inconsistency
and ⊤ truth. Given a (simple or temporal) fluent literal 𝑙, 𝑛𝑜𝑡 𝑙 represents the default negation of
𝑙. A (simple or temporal) fluent literal possibly preceded by a default negation, will be called an
extended fluent literal.
The laws are formulated as rules of a temporally extended logic programming language. Rules
have the form
□(𝑙0 ← 𝑙1 , . . . , 𝑙𝑚 , 𝑛𝑜𝑡 𝑙𝑚+1 , . . . , 𝑛𝑜𝑡 𝑙𝑛 ) (1)
where the 𝑙𝑖 ’s are either simple fluent literals or temporal fluent literals, with the following
constraints: (i) If 𝑙0 is a simple literal, then the body cannot contain temporal literals; (ii) If
𝑙0 = [𝑎]𝑙, then the temporal literals in the body must have the form [𝑎]𝑙′ ; (iii) If 𝑙0 = ○𝑙, then the
temporal literals in the body must have the form ○𝑙′ . As usual in ASP, the rules with variables
will be used as a shorthand for the set of their ground instances.
In the following we use of a notion of state: a set of ground fluent literals. A state is said to
be consistent if it is not the case that both 𝑓 and ¬𝑓 belong to the state, or that ⊥ belongs to the
state. A state is said to be complete if, for each fluent 𝑓 , either 𝑓 or ¬𝑓 belong to the state. The
execution of an action in a state may possibly change the values of fluents in the state through its
direct and indirect effects, thus giving rise to a new state.
While a law as (1) can be applied in all states, a law
𝑙0 ← 𝑙1 , . . . , 𝑙𝑚 , 𝑛𝑜𝑡 𝑙𝑚+1 , . . . , 𝑛𝑜𝑡 𝑙𝑛 (2)
which is not prefixed by □, only applies to the initial state.
A domain description can be defined as a pair (Π, 𝒞), consisting of a set of laws Π and a set of
temporal constraints 𝒞. The following action laws describe the deterministic effect of the actions
shoot and load for the Russian Turkey problem, as well as the nondeterministic effect of action
spin, after which the gun may be loaded or not:
□([𝑠ℎ𝑜𝑜𝑡]¬𝑎𝑙𝑖𝑣𝑒 ← 𝑙𝑜𝑎𝑑𝑒𝑑) □[𝑙𝑜𝑎𝑑]𝑙𝑜𝑎𝑑𝑒𝑑
□([𝑠𝑝𝑖𝑛]𝑙𝑜𝑎𝑑𝑒𝑑 ← 𝑛𝑜𝑡 [𝑠𝑝𝑖𝑛]¬𝑙𝑜𝑎𝑑𝑒𝑑) □([𝑠𝑝𝑖𝑛]¬𝑙𝑜𝑎𝑑𝑒𝑑 ← 𝑛𝑜𝑡 [𝑠𝑝𝑖𝑛]𝑙𝑜𝑎𝑑𝑒𝑑)
The following precondition laws: □([𝑙𝑜𝑎𝑑]⊥ ← 𝑙𝑜𝑎𝑑𝑒𝑑) specifies that, if the gun is loaded,
𝑙𝑜𝑎𝑑 is not executable. The program (¬𝑖𝑛_𝑠𝑖𝑔ℎ𝑡?; 𝑤𝑎𝑖𝑡)* ; 𝑖𝑛_𝑠𝑖𝑔ℎ𝑡?; 𝑙𝑜𝑎𝑑; 𝑠ℎ𝑜𝑜𝑡 describes the
behavior of the hunter who waits for a turkey until it appears and, when it is in sight, loads the
gun and shoots. Actions 𝑖𝑛_𝑠𝑖𝑔ℎ𝑡? and ¬𝑖𝑛_𝑠𝑖𝑔ℎ𝑡? are test actions (we refer to [23]). If the
constraint ⟨(¬𝑖𝑛_𝑠𝑖𝑔ℎ𝑡?; 𝑤𝑎𝑖𝑡)* ; 𝑖𝑛_𝑠𝑖𝑔ℎ𝑡?; 𝑙𝑜𝑎𝑑; 𝑠ℎ𝑜𝑜𝑡⟩⊤ is included in 𝒞 then all the runs of
the domain description which do not start with an execution of the given program will be filtered
out. For instance, an extension in which in the initial state the turkey is not in sight and the hunter
loads the gun and shoots is not allowed.
As we will see later, this temporal language is also well suited to describe causal dependencies
among fluents as static and dynamic causal laws similar to the ones in the action languages 𝒦
[14] and 𝒞 + [25].
The semantics of a domain description has been defined based on temporal answer sets [23],
which extend the notion of answer set [15] to capture the linear structure of temporal models. Let
us shortly recall the main notions. In the following, we consider the ground instantiations of the
domain description Π, and we denote by Σ the set of all the ground instances of the action names
in Π.
3.1. Temporal answer sets
A temporal interpretation is defined as a pair (𝜎, 𝑆), where 𝜎 ∈ Σ𝜔 is a sequence of actions and
𝑆 is a consistent set of ground literals of the form [𝑎1 ; . . . ; 𝑎𝑘 ]𝑙, where 𝑎1 . . . 𝑎𝑘 is a prefix of 𝜎
and 𝑙 is a ground simple fluent literal, meaning that 𝑙 holds in the state obtained by executing
𝑎1 . . . 𝑎𝑘 . 𝑆 is consistent iff it is not the case that both [𝑎1 ; . . . ; 𝑎𝑘 ]𝑙 ∈ 𝑆 and [𝑎1 ; . . . ; 𝑎𝑘 ]¬𝑙 ∈ 𝑆,
for some 𝑙, or [𝑎1 ; . . . ; 𝑎𝑘 ]⊥ ∈ 𝑆. A temporal interpretation (𝜎, 𝑆) is said to be total if either
[𝑎1 ; . . . ; 𝑎𝑘 ]𝑝 ∈ 𝑆 or [𝑎1 ; . . . ; 𝑎𝑘 ]¬𝑝 ∈ 𝑆, for each 𝑎1 . . . 𝑎𝑘 prefix of 𝜎 and for each fluent name
𝑝.
We define the satisfiability of a simple, temporal or extended literal 𝑡 in a partial temporal
interpretation (𝜎, 𝑆) in the state 𝑎1 . . . 𝑎𝑘 , (written (𝜎, 𝑆), 𝑎1 . . . 𝑎𝑘 |= 𝑡) as:
(𝜎, 𝑆), 𝑎1 . . . 𝑎𝑘 |= ⊤, (𝜎, 𝑆), 𝑎1 . . . 𝑎𝑘 ̸|= ⊥
(𝜎, 𝑆), 𝑎1 . . . 𝑎𝑘 |= 𝑙 iff [𝑎1 ; . . . ; 𝑎𝑘 ]𝑙 ∈ 𝑆, for 𝑙 s-literal
(𝜎, 𝑆), 𝑎1 . . . 𝑎𝑘 |= [𝑎]𝑙 iff [𝑎1 ; . . . ; 𝑎𝑘 ; 𝑎]𝑙 ∈ 𝑆 or
𝑎1 . . . 𝑎𝑘 , 𝑎 is not a prefix of 𝜎
(𝜎, 𝑆), 𝑎1 . . . 𝑎𝑘 |= ○𝑙 iff [𝑎1 ; . . . ; 𝑎𝑘 ; 𝑏]𝑙 ∈ 𝑆,
where 𝑎1 . . . 𝑎𝑘 𝑏 is a prefix of 𝜎
(𝜎, 𝑆), 𝑎1 . . . 𝑎𝑘 |= 𝑛𝑜𝑡 𝑙 iff (𝜎, 𝑆), 𝑎1 . . . 𝑎𝑘 ̸|= 𝑙
The satisfiability of rule bodies in a temporal interpretation is defined as usual. A rule □(𝐻 ←
𝐵𝑜𝑑𝑦) is satisfied in a temporal interpretation (𝜎, 𝑆) if, for all action sequences 𝑎1 . . . 𝑎𝑘 (in-
cluding the empty action sequence 𝜀), (𝜎, 𝑆), 𝑎1 . . . 𝑎𝑘 |= 𝐵𝑜𝑑𝑦 implies (𝜎, 𝑆), 𝑎1 . . . 𝑎𝑘 |= 𝐻.
A rule 𝐻 ← 𝐵𝑜𝑑𝑦 is satisfied in a partial temporal interpretation (𝜎, 𝑆) if, (𝜎, 𝑆), 𝜀 |= 𝐵𝑜𝑑𝑦
implies (𝜎, 𝑆), 𝜀 |= 𝐻.
Let Π be a set of rules over an action alphabet Σ, not containing default negation, and let
𝜎 ∈ Σ𝜔 .
Definition 2. A temporal interpretation (𝜎, 𝑆) is a temporal answer set of Π if 𝑆 is minimal
(with respect to set inclusion) among the 𝑆 ′ such that (𝜎, 𝑆 ′ ) is a partial interpretation satisfying
the rules in Π.
To define answer sets of a program Π containing negation, given a temporal interpretation
(𝜎, 𝑆) over 𝜎 ∈ Σ𝜔 , the reduct, Π(𝜎,𝑆) , of Π relative to (𝜎, 𝑆) is defined, by extending Gelfond
and Lifschitz’ transform [16], roughly speaking, to compute a different reduct of Π for each
prefix 𝑎1 , . . . , 𝑎ℎ of 𝜎.
(𝜎,𝑆)
Definition 3. The reduct, Π𝑎1 ,...,𝑎ℎ , of Π relative to (𝜎, 𝑆) and to the prefix 𝑎1 , . . . , 𝑎ℎ of 𝜎 , is the
set of all the rules [𝑎1 ; . . . ; 𝑎ℎ ](𝐻 ← 𝑙1 , . . . , 𝑙𝑚 ) such that 𝐻 ← 𝑙1 , . . . , 𝑙𝑚 , 𝑛𝑜𝑡 𝑙𝑚+1 , . . . , 𝑛𝑜𝑡 𝑙𝑛
is in Π and (𝜎, 𝑆), 𝑎1 , . . . , 𝑎ℎ ̸|= 𝑙𝑖 , for all 𝑖 = 𝑚 + 1, . . . , 𝑛.
(𝜎,𝑆)
The reduct Π(𝜎,𝑆) of Π relative to (𝜎, 𝑆) is the union of all reducts Π𝑎1 ,...,𝑎ℎ for all prefixes
𝑎1 , . . . , 𝑎ℎ of 𝜎.
In definition above, we say that rule [𝑎1 ; . . . ; 𝑎ℎ ](𝐻 ← 𝐵𝑜𝑑𝑦) is satisfied in a temporal interpre-
tation (𝜎, 𝑆) if (𝜎, 𝑆), 𝑎1 . . . 𝑎𝑘 |= 𝐵𝑜𝑑𝑦 implies (𝜎, 𝑆), 𝑎1 . . . 𝑎𝑘 |= 𝐻.
Definition 4 ([23]). A temporal interpretation (𝜎, 𝑆) is an answer set of Π if (𝜎, 𝑆) is an answer
set of the reduct Π(𝜎,𝑆) .
Observe that a partial interpretation (𝜎, 𝑆) provides, for each prefix 𝑎1 . . . 𝑎𝑘 , a partial eval-
(𝜎,𝑆)
uation of fluents in the state corresponding to that prefix. The (partial) state 𝑤𝑎1 ...𝑎𝑘 obtained
(𝜎,𝑆)
by the execution of the actions 𝑎1 . . . 𝑎𝑘 in the sequence can be defined as: 𝑤𝑎1 ...𝑎𝑘 = {𝑙 :
[𝑎1 ; . . . ; 𝑎𝑘 ]𝑙 ∈ 𝑆}.
Although the answer sets of a domain description Π are partial interpretations, in some cases,
e.g., when the initial state is complete and all fluents are inertial, it is possible to guarantee that
the temporal answer sets of Π are total. The case of total temporal answer sets is of special
interest as a total temporal answer set (𝜎, 𝑆) can be regarded as a temporal model.
4. Combining Temporal Action Theories with ℰℒ⊥ KBs
In this section we define a notion of extended temporal action theory, consisting of a temporal
action theory plus an ℰℒ⊥ knowledge base. Our approach, following most of the proposals for
reasoning about actions in DLs [5, 6, 12, 4, 1] is to regard the TBox as a set of state constraints,
i.e. conditions that must be satisfied by any state of the world (in all possible extensions of the
action theory), and the ABox as a set of constraints on all possible initial states.
We want to regard DL assertions as fluents that may occur in our action laws as well as in the
states of the action theory. Given a (normalized) ℰℒ⊥ knowledge base K = (𝒯 , 𝒜), we require
that: (a) for each (possibly complex) concept 𝐶 occurring in K there is a unary predicate 𝐶 ∈ 𝒫;
(b) for each role name 𝑟 ∈ 𝑁𝑅,K there is a binary predicate 𝑟 ∈ 𝒫; (c) the set of constants 𝐶𝑜𝑛𝑠
includes all the individual names occurring in the K , i.e. 𝑁𝐼,K ⊆ 𝐶𝑜𝑛𝑠.
Observe that if a complex concept such as ∃𝑟.𝐶 occurs in K , there exists a predicate name
∃𝑟.𝐶 ∈ 𝒫 and, for each 𝑎 ∈ 𝑁𝐼,KB , the fluent literals (∃𝑟.𝐶)(𝑎) and ¬(∃𝑟.𝐶)(𝑎) belong to the
set 𝐿𝑖𝑡 (we will still call such literals assertions). Although classical negation is not allowed in
ℰℒ⊥ , we use explicit negation [15] to allow negative literals of the form ¬𝐶(𝑎) in the action
language (to allow for deleting an assertion from a state).
A simple literal in 𝐿𝑖𝑡 is said to be a simple assertion if it has the form 𝐵(𝑎) or 𝑟(𝑎, 𝑏) or
¬𝐵(𝑎) or ¬𝑟(𝑎, 𝑏), where 𝐵 ∈ 𝐵𝐶K is a base concept in K , 𝑟 ∈ 𝑁𝑅,K and 𝑎, 𝑏 ∈ 𝑁𝐼,K .
Observe that {𝑎}(𝑐) and ¬{𝑎}(𝑐) are simple assertions, while (∃𝑟.𝐶)(𝑎) and ¬(∃𝑟.𝐶)(𝑎) are
non-simple assertions.
In order to deal with existential restrictions, in addition to the individual names 𝑁𝐼,KB occurring
in the KB we introduce a finite set 𝐴𝑢𝑥 of auxiliary individual names, as proposed in [29] to
encode ℰℒ⊥ inference in Datalog, where 𝐴𝑢𝑥 contains a new individual name 𝑎𝑢𝑥𝐴⊑∃𝑟.𝐵 , for
each inclusion 𝐴 ⊑ ∃𝑟.𝐵 occurring in the KB . We further require that 𝐴𝑢𝑥 ⊆ 𝐶𝑜𝑛𝑠.
Definition 5 (Extended action theory). An extended action theory is a tuple (K , Π, 𝒞), where:
K = (𝒯 , 𝒜) is an ℰℒ⊥ knowledge base; Π is a set of laws: action, causal, executability and
initial state laws (see below); 𝒞 is a set of temporal constraints.
Action laws describe the immediate effects of actions. They have the form:
□([𝑎]𝑙0 ← 𝑡1 , . . . , 𝑡𝑚 , 𝑛𝑜𝑡 𝑡𝑚+1 , . . . , 𝑛𝑜𝑡 𝑡𝑛 ) (3)
where 𝑙0 is a simple fluent literal and the 𝑡𝑖 ’s are either simple fluent literals or temporal fluent
literals of the form [𝑎]𝑙. Its meaning is that executing action 𝑎 in a state in which the conditions
𝑡1 , . . . , 𝑡𝑚 hold and conditions 𝑡𝑚+1 , . . . , 𝑡𝑛 do not hold causes the effect 𝑙0 to hold. As an exam-
ple, [Assign(c, x )]Teaches(x , c) ← 𝐶𝑜𝑢𝑟𝑠𝑒(𝑐) means that executing the action of assigning a
course 𝑐 to 𝑥 has the effect that 𝑥 teaches 𝑐. Non-deterministic effects of actions can be defined
using default negation in the body of action laws, as for the action spin in Section 3.
Causal laws describe indirect effects of actions. They have the form: In Π we allow two kinds
of causal laws. Static causal laws have the form:
□(𝑙0 ← 𝑙1 , . . . , 𝑙𝑚 , 𝑛𝑜𝑡 𝑙𝑚+1 , . . . , 𝑛𝑜𝑡 𝑙𝑛 ) (4)
where the 𝑙𝑖 ’s are simple fluent literals. Their meaning is: if 𝑙1 , . . . , 𝑙𝑚 hold in a state and
𝑙𝑚+1 , . . . , 𝑙𝑛 do not hold in that state, than 𝑙0 is caused to hold in that state. Dynamic causal laws
have the form:
□(○𝑙0 ← 𝑡1 , . . . , 𝑡𝑚 , 𝑛𝑜𝑡 𝑡𝑚+1 , . . . , 𝑛𝑜𝑡 𝑡𝑛 ) (5)
where 𝑙0 is a simple fluent literal and the 𝑡𝑖 ’s are either simple fluent literals or temporal fluent
literals of the form ○𝑙𝑖 . For instance, ○Teacher (x ) ← ○Teaches(x , y) ∧Course(y). Observe
that, differently from [5, 4], we do not restrict direct and indirect effects of actions to be simple
assertions. State constraints that apply to the initial state or to all states can be obtained when ⊥
occurs in the head of initial state laws (6) or static causal laws (4).
Precondition laws describe the executability conditions of actions. They have the form:
□([𝑎]⊥ ← 𝑙1 , . . . , 𝑙𝑚 , 𝑛𝑜𝑡 𝑙𝑚+1 , . . . , 𝑛𝑜𝑡 𝑙𝑛 ) where 𝑎 ∈ Σ and the 𝑙𝑖 ’s are simple fluent literals.
The meaning is that the execution of an action 𝑎 is not possible in a state in which 𝑙1 , . . . , 𝑙𝑚 hold
and 𝑙𝑚+1 , . . . , 𝑙𝑛 do not hold
Initial state laws are needed to introduce conditions that have to hold in the initial state. They
have the form:
𝑙0 ← 𝑙1 , . . . , 𝑙𝑚 , 𝑛𝑜𝑡 𝑙𝑚+1 , . . . , 𝑛𝑜𝑡 𝑙𝑛 (6)
where the 𝑙𝑖 ’s are simple fluent literals. Observe that initial state laws, unlike static causal
laws, only apply to the initial state as they are not prefixed by the □ modality. As a special
case, the initial state can be defined as a set of simple fluent literals. For instance, the initial
state {𝑎𝑙𝑖𝑣𝑒, ¬𝑖𝑛_𝑠𝑖𝑔ℎ𝑡, ¬𝑓 𝑟𝑖𝑔ℎ𝑡𝑒𝑛𝑒𝑑} is defined by the initial state laws: 𝑎𝑙𝑖𝑣𝑒, ¬𝑖𝑛_𝑠𝑖𝑔ℎ𝑡,
¬𝑓 𝑟𝑖𝑔ℎ𝑡𝑒𝑛𝑒𝑑.
Following Lifschitz [30] we call frame fluents the fluents to which the law of inertia applies.
Persistence of frame fluents from a state to the next one can be captured by introducing in Π a set
of causal laws, said persistence laws for all frame fluents 𝑓 .
□(○𝑓 ← 𝑓, 𝑛𝑜𝑡 ○ ¬𝑓 ) □(○¬𝑓 ← ¬𝑓, 𝑛𝑜𝑡 ○ 𝑓 )
meaning that, if 𝑓 holds in a state, then 𝑓 will hold in the next state, unless its negation ¬𝑓 is
caused to hold (and similarly for ¬𝑓 ). Persistence 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 persistence laws above play the role of inertia rules in 𝒞 [26], 𝒞+ [25]
and 𝒦 [14].
If 𝑓 is non-frame with respect to an action 𝑎, 𝑓 is not expected to persist and may change its
value when an action 𝛼 is executed, either non-deterministically:
□(○𝑓 ← 𝑛𝑜𝑡 ○ ¬𝑓 ) □(○¬𝑓 ← 𝑛𝑜𝑡 ○ 𝑓 )
or by taking some default value (see [23] for some examples).
In the following we assume that persistence laws and non-frame laws can be applied to simple
assertions but not to non-simple ones (such as (∃𝑟.𝐵)(𝑥)), whose value in a state (as we will
see) is determined from the value of simple assertions. For simple assertions 𝐴(𝑐) in a domain
description, one has to choose whether the concept 𝐴 is frame or non-frame (so that either
persistence laws or non-frame laws can be introduced). In particular, we assume that all the
nominals always correspond to frame fluents: if {𝑎}(𝑏) (respectively ¬{𝑎}(𝑏)) 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 ℰℒ⊥ interpretations, we assume that the laws: 𝑓 ← 𝑛𝑜𝑡¬𝑓 and ¬𝑓 ← 𝑛𝑜𝑡𝑓 for
completing the initial state are introduced in Π for all simple literals 𝑓 (including assertions with
nominals). As shown in [23], 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 reachable state in
each extension of a domain description is complete for simple fluents, we assume that, either the
fluent is frame, and persistence laws are introduced for it, or it is non-frame, and non-frame laws
are introduced. Other literals, such as existential assertions, are not subject to this requirement
but, as we will see below, the value of existential assertions in a state will be determined from
the value of simple assertions. Under the condition above, starting from an initial state which is
complete for simple fluents, all the reachable states are also complete for simple fluents. We call
well-defined the domain descriptions satisfying this condition (and sometimes we will simply say
that Π is well-defined).
The third component 𝒞 of a domain description (𝐾, Π, 𝒞) is the set of temporal constraints in
DLTL, which allow general temporal conditions to be imposed on the executions of the domain
description. Their effect is that of restricting the space of the possible executions (or extensions).
For a domain description 𝐷 = (Π, 𝒞), as introduced in [23], extensions are defined as follows.
Definition 6. An extension of a well-defined domain domain description 𝐷 = (Π, 𝒞) over Σ is a
(total) answer set (𝜎, 𝑆) of Π which satisfies the constraints in 𝒞.
In the next section we extend the notion of extension to a domain description (𝐾, Π, 𝒞) with 𝐾
an ontology.
5. Ontology axioms as state constraints
Given an action theory (K , Π, 𝒞), where K = (𝒯 , 𝒜), we define an extension of (K , Π, 𝒞) as an
extension (𝜎, 𝑆) of the action theory (Π, 𝒞) satisfying all axioms of the ontology 𝐾. Informally,
each state 𝑤 in the extension is required to correspond to an ℰℒ⊥ interpretation and to satisfy all
inclusion axioms in TBox 𝒯 . Additionally, the initial state must satisfy all assertions in the ABox
𝒜.
To define the extensions of an action theory (K , Π, 𝒞), we restrict to well-defined domain
descriptions (K , Π, 𝒞), so that all states in an extension are complete for simple fluents (and for
simple assertions). We prove that such states represent ℰℒ⊥ interpretations on the language of
𝐾, provided an additional set of laws Πℒ(𝐾) is included in the action theory. Next, we add to
Π another set Π𝒯 of constraints, to guarantee that each state satisfies the inclusion axioms in 𝒯 .
Finally, we add to Π the set of laws Π𝒜 , to guarantee that all assertions in 𝒜 are satisfied in the
initial state.
Overall, this provides a transformation of the action theory (K , Π, 𝒞) into a new action theory
(Π ∪ Π𝐾 , 𝒞), by eliminating the ontology while introducing a set of static causal laws and
constraints Π𝐾 = Πℒ(𝐾) ∪ Π𝒯 ∪ Π𝒜 , intended to exclude those extensions which do not satisfy
the axioms in 𝐾.
The set of domain constraints and causal laws in Πℒ(𝐾) is intended to guarantee that any
state 𝑤 of an extension respects the semantics of DL concepts occurring in K . The definition of
Πℒ(𝐾) is based on a fragment of the materialization calculus for ℰℒ⊥ , which provides a Datalog
encoding of an ℰℒ⊥ ontology. Here, the idea is that of regarding an assertion 𝐶(𝑎) in a state 𝑤
as the evidence that 𝑎𝐼 ∈ 𝐶 𝐼 in the corresponding interpretation. Let Πℒ(𝐾) be the following set
of causal laws:
(1) □(⊥ ← ⊥(𝑥)) (2) □(⊤(𝑥) ←) (3) □({𝑎}(𝑎) ←)
(4) □(𝑒𝑥𝑖𝑠𝑡𝑠_𝑟_𝐵(𝑥) ← 𝑟(𝑥, 𝑦) ∧ 𝐵(𝑦))
(5) □((∃𝑟.𝐵)(𝑥) ← 𝑒𝑥𝑖𝑠𝑡𝑠_𝑟_𝐵(𝑥))
(6) □(¬(∃𝑟.𝐵)(𝑥) ← 𝑛𝑜𝑡 𝑒𝑥𝑖𝑠𝑡𝑠_𝑟_𝐵(𝑥))
(7) □(⊥ ← {𝑎}(𝑥) ∧ 𝐵(𝑥) ∧ 𝑛𝑜𝑡 𝐵(𝑎)), for 𝑥 ̸= 𝑎
(8) □(⊥ ← {𝑎}(𝑥) ∧ 𝐵(𝑎) ∧ 𝑛𝑜𝑡 𝐵(𝑥)), for 𝑥 ̸= 𝑎
(9) □(⊥ ← {𝑎}(𝑥) ∧ 𝑟(𝑧, 𝑥) ∧ 𝑛𝑜𝑡 𝑟(𝑧, 𝑎)), for 𝑥 ̸= 𝑎
for all 𝑥, 𝑦 ∈ ∆, 𝑎 ∈ 𝑁𝐼,K , 𝐵 ∈ 𝐵𝐶K (the base concepts occurring in K ) and 𝑟 ∈ 𝑁𝑅,K (the
roles occurring in K ). Observe that the first constraint has the effect that a state 𝑆, in which the
concept ⊥ has an instance, is made inconsistent. Law (4) makes 𝑒𝑥𝑖𝑠𝑡𝑠_𝑟_𝐵(𝑥) hold in any state
in which there is a domain element 𝑦 such that 𝑟(𝑥, 𝑦) and 𝐵(𝑦) hold (where 𝑒𝑥𝑖𝑠𝑡𝑠_𝑟_𝐵 is an
additional auxiliary predicate for 𝐵 ∈ 𝐵𝐶K and 𝑟 ∈ 𝑁𝑅,K ). Laws (5) and (6) guarantee that,
for all 𝑥 ∈ ∆, either (∃𝑟.𝐵)(𝑥) or ¬(∃𝑟.𝐵)(𝑥) is contained in the state. State constraints (7-9)
are needed for the treatment of nominals and are related to materialization calculus rules (27-29)
[29].
Let (𝜎, 𝑆) be an extension of the action theory (Π ∪ Πℒ(𝐾) , 𝒞). It can be proven that any
state 𝑤 of (𝜎, 𝑆) represents an ℰℒ⊥ interpretation. Given a state 𝑤, let 𝑤+ be the set of ℰℒ⊥
assertions 𝐶(𝑎) (𝑟(𝑎, 𝑏)), such that 𝐶(𝑎) ∈ 𝑤 (resp., 𝑟(𝑎, 𝑏) ∈ 𝑤). Let 𝑤− be the set of ℰℒ⊥
assertions 𝐶(𝑎) (𝑟(𝑎, 𝑏)), such that ¬𝐶(𝑎) ∈ 𝑤 (resp., ¬𝑟(𝑎, 𝑏) ∈ 𝑤).
Proposition 1. Let (𝜎, 𝑆) be an extension of the action theory (Π ∪ Πℒ(𝐾) , 𝒞) and let 𝑤 be a
state of (𝜎, 𝑆). Then there is an interpretation (∆𝐼 , ·𝐼 ) that satisfies all the assertions in 𝑤+ and
falsifies all assertions in 𝑤− (and we say that (∆𝐼 , ·𝐼 ) agrees with state 𝑤).
As mentioned, we are interested in the states satisfying the TBox 𝒯 of 𝐾. Provided Π is well-
defined, for each extension (𝜎, 𝑆) of the action theory (Π ∪ Πℒ(𝐾) , 𝒞), any state 𝑤 is consistent
and complete for all simple literals (and hence, by (5) and (6), for all assertions). We say that
𝑤 satisfies the TBox 𝒯 if for all interpretations (∆𝐼 , ·𝐼 ) such that (∆𝐼 , ·𝐼 ) agrees with state 𝑤,
(∆𝐼 , ·𝐼 ) is a model of 𝒯 .
The requirement that each 𝑤 should satisfy the TBox 𝒯 can be incorporated in the action
theory through a set of constraints, that we call Π𝒯 , by exploiting the fact that the TBox 𝒯 is in
normal form. Π𝒯 contains the following state constraints:
□(⊥ ← 𝐴(𝑥) ∧ 𝑛𝑜𝑡 𝐷(𝑥)), for each 𝐴 ⊑ 𝐷 in 𝒯 ;
□(⊥ ← 𝐴(𝑥) ∧ 𝐵(𝑥) ∧ 𝑛𝑜𝑡 𝐷(𝑥)), for each 𝐴 ⊓ 𝐵 ⊑ 𝐷 in 𝒯 ;
□(⊥ ← 𝐴(𝑥) ∧ 𝑛𝑜𝑡 (∃𝑟.𝐵)(𝑥)), for each 𝐴 ⊑ ∃𝑟.𝐵 in 𝒯 ;
□(⊥ ← (∃𝑟.𝐵)(𝑥) ∧ 𝑛𝑜𝑡 𝐷(𝑥)), for each ∃𝑟.𝐵 ⊑ 𝐷 in 𝒯 ;
where 𝐴, 𝐵 ∈ 𝐵𝐶K , 𝐷 ∈ 𝐵𝐶K ∪ {⊥} and 𝑥 ∈ 𝑁𝐼,K ∪ 𝐴𝑢𝑥. For 𝐷 = ⊥, the condition
𝑛𝑜𝑡 𝐷(𝑥) is omitted. The following proposition can be proved for a well-defined Π.
Proposition 2. Let (𝜎, 𝑆) be an extension of the action theory (Π ∪ Πℒ(𝐾) , 𝒞) and let 𝑤 be a
state of (𝜎, 𝑆); 𝑤 satisfies 𝒯 iff 𝑤 satisfies all constraints in Π𝒯 .
We can then add the constraints in Π𝒯 to an action theory (Π ∪ Πℒ(𝐾) , 𝒞) to single out the
extensions (𝜎, 𝑆) whose states all satisfy the TBox 𝒯 . In a similar way, we can restrict to answer
(𝜎,𝑆)
sets (𝜎, 𝑆) whose initial state 𝑤𝜀 satisfies all assertions in 𝒜, by defining a set of initial state
constraints as:
Π𝒜 = {⊥ ← 𝑛𝑜𝑡 𝐴(𝑐)) | 𝐴(𝑐) ∈ 𝒜} ∪ {⊥ ← 𝑛𝑜𝑡 𝑟(𝑐, 𝑑)) | 𝑟(𝑐, 𝑑) ∈ 𝒜}
We define the extensions of the extended action theory (K , Π, 𝒞) as the extensions of the action
theory (Π ∪ Π𝐾 , 𝒞), where Π𝐾 = Πℒ(𝐾) ∪ Π𝒯 ∪ Π𝒜 .
Given this notion of extension of an action theory (K , Π, 𝒞), we can verify, in the temporal
action logic, whether a sequence of actions is executable from the initial state (executability
problem) or whether any execution of an action sequence makes some property (e.g., assertion)
hold in all reachable states (temporal projection problem).
Let us consider the example from the introduction.
Example 1. Let K = (𝒯 , 𝒜) be a knowledge base such that 𝒯 = {∃Teaches.Course ⊑
Teacher } and 𝒜= { Person(john), Course(cs1 )}. We assume that all simple assertions, i.e.,
Person(x ), Teacher (x ), Course(x ), Teaches(x , y), are frame for all 𝑥, 𝑦 ∈ 𝑁𝐼,K ∪ 𝐴𝑢𝑥.
Let us consider a state 𝑤0 where John does not teach any course and is not a teacher.
If an action Assign(cs1 , john) were executed in 𝑤0 , given a Π containing the action law
[Assign(cs1 , john)]Teaches(john, cs1 ), the resulting state would contain
∃Teaches.Course)(john), but would not contain Teacher (john), thus violating the state con-
straint
□(⊥ ← (∃Teaches.Course)(𝑥) ∧ 𝑛𝑜𝑡 Teacher (𝑥)),
in Π𝒯 . In this case, there is no extension of the action theory in which action Assign(cs1 , john)
can be executed in the initial state.
As observed in [4], when this happens, the action specification can be regarded as being
underspecified, as it is not able to capture the dependencies among fluents which occur in the
TBox. To guarantee that TBox is satisfied in the new state, causal laws are needed which allow the
state to be repaired. In the specific case, adding causal law □(Teacher (x ) ← Teaches(x , y) ∧
Course(y)) to Π would suffice to cause Teacher (x ) in the resulting state, as an indirect effect of
action Assign(cs1 , john).
6. Causal laws for repairing inconsistencies: sufficient
conditions
Can we identify which and how many conditions are needed to guarantee that an action theory is
able to repair the state, after executing an action, so to satisfy all inclusions of a (normalized)
ℰℒ⊥ TBox, when possible? Let us continue Example 1.
Example 2. Consider the case when action retire(john) is executed in a state 𝑤1 where
Person(john), Course(cs1 ), Teaches(john, cs1 ) and Teacher (john) hold. Suppose that the
action law: [retire(john)]¬Teacher (john) is in Π. Then, ¬Teacher (john) will belong to the
new state (let us call it 𝑤2 ), but 𝑤2 will still contain the literals: Course(cs1 ), Teaches(john, cs1 ),
which persist from the previous state (as Course and Teaches are frame fluents). Hence, 𝑤2
would violate the TBox 𝒯 . To avoid this, Π should contain some causal law to repair the incon-
sistency, for instance, □(¬Teaches(x , y) ← ¬Teacher (x ) ∧ Course(y)). By this causal law,
when John retires he stops teaching all the courses he was teaching before. In particular, he
stops teaching 𝑐𝑠1. On the contrary, □(¬Course(y) ← ¬Teacher (x ) ∧ Teaches(x , y)) would
be unintended.
As we can see, the causal laws 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 contrapositives are always wanted.
In general, while defining a domain description, one has to choose which causal relationships
are intended and which are not. The choice depends on the domain and should not be done
automatically, but some sufficient conditions to restore the consistency of the resulting state (if
any) with a TBox (in normal form) can be defined.
The case of a (normalized) inclusion 𝐴 ⊑ 𝐵, with 𝐴, 𝐵 ∈ 𝑁𝐶 , is relatively simple; the
execution of an action 𝛼 with effect 𝐴(𝑐) (but not 𝐵(𝑐)), in a state in which none of 𝐴(𝑐)
and 𝐵(𝑐) holds, would lead to a state which violates the constraints in the KB . Similarly for
an action 𝛽 with effect ¬𝐵(𝑐). Deleting 𝐵(𝑐) should cause 𝐴(𝑐) to be deleted as well, if we
want the inclusion 𝐴 ⊑ 𝐵 to be satisfied. Hence, to guarantee that the TBox is satisfied in
the new state, for each inclusion 𝐴 ⊑ 𝐵, two causal laws are needed: □(𝐵(𝑥) ← 𝐴(𝑥)) and
□(¬𝐴(𝑥) ← ¬𝐵(𝑥)).
For an axiom 𝐴 ⊓ 𝐵 ⊑ ⊥, consider the concrete case 𝑝𝑒𝑛𝑑𝑖𝑛𝑔 ⊓ 𝑎𝑝𝑝𝑟𝑜𝑣𝑒𝑑 ⊑ ⊥, 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:
□(¬𝑝𝑒𝑛𝑑𝑖𝑛𝑔(𝑥) ← 𝑎𝑝𝑝𝑟𝑜𝑣𝑒𝑑(𝑥)) □(¬𝑎𝑝𝑝𝑟𝑜𝑣𝑒𝑑(𝑥) ← 𝑝𝑒𝑛𝑑𝑖𝑛𝑔(𝑥))
even though the second one is only useful if a claim can become pending again after having
become (temporarily) approved. For the general case, we have the following.
Let us define a set Π𝐶(𝒯 ) of causal laws associated with 𝒯 as follows:
• For 𝐴 ⊑ 𝐵 in 𝒯 : □(𝐵(𝑥) ← 𝐴(𝑥)) and □(¬𝐴(𝑥) ← ¬𝐵(𝑥));
• For 𝐴 ⊓ 𝐵 ⊑ 𝐷: □(𝐷(𝑥) ← 𝐴(𝑥) ∧ 𝐵(𝑥)) and at least one among
□(¬𝐴(𝑥) ← ¬𝐷(𝑥) ∧ 𝐵(𝑥)) and □(¬𝐵(𝑥) ← ¬𝐷(𝑥) ∧ 𝐴(𝑥));
• For 𝐴 ⊑ ∃𝑟.𝐵: □(𝑟(𝑥, 𝑎𝑢𝑥𝐴⊑∃𝑟.𝐵 ) ← 𝐴(𝑥)), □(𝐵(𝑎𝑢𝑥𝐴⊑∃𝑟.𝐵 ) ← 𝐴(𝑥)) and
□(¬𝐴(𝑥) ← ¬(∃𝑟.𝐵)(𝑥));
• For ∃𝑟.𝐵 ⊑ 𝐴 in 𝒯 : □(𝐴(𝑥) ← (∃𝑟.𝐵)(𝑥), □(¬(∃𝑟.𝐵)(𝑥) ← ¬𝐴(𝑥)) and at least one
of: □(¬𝑟(𝑥, 𝑦) ← ¬𝐴(𝑥) ∧ 𝐵(𝑥)) and □(¬𝐵(𝑥) ← ¬𝐴(𝑥) ∧ 𝑟(𝑥, 𝑦)).
Proposition 3. Given a well-defined action theory (Π, 𝒞) and a TBox 𝒯 , any state 𝑤 of an
extension (𝜎, 𝑆) of (Π ∪ Πℒ(𝐾) ∪ Π𝐶(𝒯 ) ∪ Π𝒜 , 𝒞) satisfies 𝒯 .
Observe that, for the case for 𝐴 ⊑ ∃𝑟.𝐵, from 𝑟(𝑥, 𝑎𝑢𝑥𝐴⊑∃𝑟.𝐵 ) and 𝐵(𝑎𝑢𝑥𝐴⊑∃𝑟.𝐵 ) (∃𝑟.𝐵)(𝑥)
is caused by laws (4-5) in Πℒ(𝐾) . While the causal laws in Π𝐶(𝒯 ) are sufficient to guarantee the
consistency of a resulting state with TBox 𝒯 , one cannot exclude that some action effects are
inconsistent with TBox and cannot be repaired (e.g., an action with direct effects 𝐴(𝑐) and ¬𝐵(𝑐),
conflicting with an axiom 𝐴 ⊑ 𝐵 in 𝒯 ). In such a case, the action would not be executable.
Notice that the encoding above of ℰℒ⊥ TBox into a set of temporal laws only requires a
polynomial number of laws to be added to the action theory (in the size of 𝐾). Based on this
mapping, the proof methods for our temporal action logic, which are based on the ASP encodings
of bounded model checking [22, 23, 24], can be exploited for reasoning about actions in an action
theory extended with an ℰℒ⊥ knowledge base.
7. Conclusions and Related Work
In this paper we have proposed an approach for reasoning about actions by combining a temporal
action logic in [23], whose semantics is based on a notion of temporal answer sets, and an ℰℒ⊥
ontology. It is shown that, for ℰℒ⊥ knowledge bases in normal form, the consistency of the
action theory extensions with the ontology can be verified by adding to the action theory a set
of causal laws and state constraints, by exploiting a fragment of the materialization calculus
by Krötzsch [29]. Starting from the idea by Baader et al. [4] that causal rules can be used to
ensure the consistency of states with the TBox, we have defined sufficient conditions on the
action theory to repair the states resulting from action execution and guarantee consistency with
TBox. For each inclusion axiom, a suitable set of causal laws has to be added. Our approach
provides a polynomial encoding of an extended action theory, including an ℰℒ⊥ knowledge base
in normal form, into the language of the (DLTL based) temporal action logic studied in [23].
The proof methods for this temporal action logic, based on ASP encodings of bounded model
checking [22, 23, 24], can then be exploited for reasoning about actions in an extended action
theory. It would also be interesting, for action domains with finite executions, to investigate
whether the action theories in [23] can be encoded in in telingo [10], and whether the optimized
implementation of telingo can be exploited for reasoning about action in our extended action
theories.
Many of the proposals in the literature for combining DLs with action theories focus on
expressive DLs. In their seminal work [5], Baader et al. study the integration of action formalisms
with expressive DLs, from 𝒜ℒ𝒞 to 𝒜ℒ𝒞𝒪ℐ𝒬, under Winslett’s possible models approach (PMA)
[35], 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 [32] and [4] we do not require
the restriction to acyclic TBoxes and primitive concepts in postconditions.
The requirement of acyclic TBoxes is lifted in the work by Liu et al. [32], 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 domain the control of the ramifications.
Similar considerations are at the basis of the approach by Baader et al. [4] that, instead,
exploits causal relationships for modeling ramifications in an action language for 𝒜ℒ𝒞𝒪, and
defines its semantics in the style of McCain and Turner fixpoint semantics [33] (the action theory
does not deal with non-deterministic effects of actions). It is shown that temporal projection
is decidable and E XP T IME-complete. In this paper, following [4], we exploit causal laws for
modeling ramifications in the context of a temporal action language for ℰℒ⊥ . It allows for
non-deterministic effects of actions and for the distinction between frame and non-frame fluents
[30] (which is strongly related to occlusion used in [32]) based on the temporal logic. We have
also provided sufficient conditions for an action specification to be consistent with a normalized
ℰℒ⊥ 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 𝒜ℒ𝒞ℋ𝒪ℐ𝒬𝑏𝑟 (under finite satisfiability) as well as for variants of DL-lite. Complex
actions including action sequence and conditional actions are considered. Complex actions are
considered as well in [12], where an action formalism is introduced for a family DLs, from
𝒜ℒ𝒞𝒪 to 𝒜ℒ𝒞ℋ𝒪ℐ𝒬, 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 [11] the approach is extended to allow for
different notions of repairing of the resulting state, such as a maximal subset 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 allows for a
finer control on the resulting state.
Our semantics for actions, as many of the proposals in the literature, requires that a state
provides a complete description of the world and is intended to represent an interpretation of
the ℰℒ⊥ knowledge base. An alternative approach has been adopted in [8], where a state can
provide an incomplete specification of the world. In our approach, an incomplete state could
be represented as an epistemic state, which distinguish between what is known to be true (or to
be false) and what is unknown. An epistemic extension of our action logic, based on temporal
answer sets, has been developed in [24], and it can potentially be exploited for reasoning about
actions with incomplete states also in presence of ontological knowledge. We leave the study of
this case for future work.
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 ℰℒ 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 ℰℒ 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 𝒞+ 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] Cabalar, P., Kaminski, R., Morkisch, P., Schaub, T.: telingo = ASP + time. In: Logic
Programming and Nonmonotonic Reasoning - 15th International Conference, LPNMR
2019, Philadelphia, PA, USA, June 3-7, 2019, Proceedings. Lecture Notes in Computer
Science, vol. 11481, pp. 256–269. Springer (2019)
[11] Calvanese, D., Kharlamov, E., Montali, M., Santoso, A., Zheleznyakov, D.: Verification of
inconsistency-aware knowledge and action bases. In: Proc. IJCAI 2013 (2013)
[12] 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)
[13] Denecker, M., Theseider Dupré, D., Van Belleghem, K.: An inductive definitions approach
to ramifications. Electronic Transactions on Artificial Intelligence 2, 25–97 (1998)
[14] 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)
[15] Gelfond, M.: Handbook of Knowledge Representation, chapter 7, Answer Sets. Elsevier
(2007)
[16] Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Logic
Programming, Proc. of the 5th Int. Conf. and Symposium. pp. 1070–1080 (1988)
[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., Spiotta, M., Theseider Dupré, D.: ASP for reasoning about
actions with an EL⊥ knowledge base. In: Fiorentini, C., Momigliano, A. (eds.) Proceedings
of the 31st Italian Conference on Computational Logic, Milano, Italy, June 20-22, 2016.
CEUR Workshop Proceedings, vol. 1645, pp. 214–229. CEUR-WS.org (2016), http://
ceur-ws.org/Vol-1645/paper_15.pdf
[21] Giordano, L., Martelli, A., Theseider Dupré, D.: Reasoning about actions with temporal
answer sets. In: Faber, W., Leone, N. (eds.) Proceedings of the 25th Italian Conference on
Computational Logic, Rende, Italy, July 7-9, 2010. CEUR Workshop Proceedings, vol. 598.
CEUR-WS.org (2010)
[22] Giordano, L., Martelli, A., Theseider Dupré, D.: Achieving completeness in bounded
model checking of action theories in ASP. In: Brewka, G., Eiter, T., McIlraith, S.A. (eds.)
Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth
International Conference, KR 2012, Rome, Italy, June 10-14, 2012. AAAI Press (2012),
http://www.aaai.org/ocs/index.php/KR/KR12/paper/view/4532
[23] Giordano, L., Martelli, A., Theseider Dupré, D.: Reasoning about actions with temporal
answer sets. Theory and Practice of Logic Programming 13, 201–225 (2013)
[24] Giordano, L., Martelli, A., Theseider Dupré, D.: Achieving completeness in the verification
of action theories by bounded model checking in ASP. J. Log. Comput. 25(6), 1307–1330
(2015), https://doi.org/10.1093/logcom/ext067
[25] Giunchiglia, E., Lee, J., Lifschitz, V., McCain, N., , Turner, H.: Nonmonotonic causal
theories. Artificial Intelligence 153(1-2), 49–104 (2004)
[26] Giunchiglia, E., Lifschitz, V.: An action language based on causal explanation: Preliminary
report. In: Proc. AAAI/IAAI 1998. pp. 623–630 (1998)
[27] Heljanko, K., Niemelä, I.: Bounded LTL model checking with stable models. Theory and
Practice of Logic Programming 3(4-5), 519–550 (2003)
[28] Henriksen, J., Thiagarajan, P.: Dynamic linear time temporal logic. Annals of Pure and
Applied logic 96(1-3), 187–207 (1999)
[29] Krötzsch, M.: Efficient inferencing for OWL EL. In: Proc. JELIA 2010. pp. 234–246 (2010)
[30] Lifschitz, V.: Frames in the space of situations. Artificial Intelligence 46, 365–376 (1990)
[31] 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)
[32] 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)
[33] McCain, N., Turner, H.: A causal theory of ramifications and qualifications. In: Proc. IJCAI
95. pp. 1978–1984 (1995)
[34] Thielscher, M.: Ramification and causality. Artif. Intell. 89(1-2), 317–364 (1997)
[35] Winslett, M.: Reasoning about action using a possible models approach. In: Proc. AAAI, St.
Paul, MN, August 21-26, 1988. pp. 89–93 (1988)