Temporal Logic Programs with Temporal Description Logic Axioms

Abstract

In this paper we introduce a combination of Answer Set Programming (ASP) and Description Logics (DL) (in particular, $\mathcal{ALC}$) on top of a modal temporal basis using connectives from Linear-time Temporal Logic (LTL). On the one hand, for the temporal extension of $\mathcal{ALC}$, we depart from Baader et al.’s proposal $\mathcal{ALC}$-LTL that restricts the use of temporal operators to occur only in front of DL axioms. On the other hand, for the temporal extension of ASP we use its formalization in terms of Temporal (Quantified) Equilibrium Logic (TEL). This choice is convenient since (non-temporal) Equilibrium Logic has been already used to capture the semantics of hybrid theories, that is, combinations of ASP programs with DL axioms. Our proposal, called $\mathcal{ALC}$-TEL, actually interprets $\mathcal{ALC}$ axioms in terms of their translation into first order sentences, so that the semantics of TEL is eventually used in the background. The resulting formalism conservatively extends TEL, hybrid theories and $\mathcal{ALC}$-LTL as particular cases.

This work was partially supported by MINECO, Spain (grant TIC2017-84453-P), Xunta de Galicia, Spain (grant 2016-2019 ED431G/01, CITIC) and DFG, Germany, (grant SCHA 550/9).

1 Introduction

Due to its versatility, Answer Set Programming (ASP) [1, 2] is one of the paradigms for non-monotonic reasoning that has been more frequently extended in the literature (if not the most). Each extension has been motivated by a given type of reasoning problem or family of application domains. For instance, the treatment of dynamic scenarios and transition systems was present from the very beginning of ASP [3] and eventually led to a combination of ASP with modal operators from Linear-time Temporal Logic (LTL) [4, 5], giving birth to so-called Temporal Equilibrium Logic (TEL) [6]. As another example, the ASP extension of Hybrid Knowledge Bases [7] allows for combining non-monotonic logic programs with classical inference about ontologies, in terms of Description Logic (DL) [8]. Both extensions are based on the underlying formalism of Equilibrium Logic [9] but work in different directions: a natural question is what happens when we try to embrace both features, time and ontologies, in a common ASP extension. In the monotonic case, several approaches considered the introduction of LTL operators in DL at different levels, at the cost of a high complexity, or even undecidability for some reasoning tasks. A simple approach that avoids these inconveniences is $\mathcal{ALC}$-LTL [10], proposed by Baader, Ghilardi and Lutz, that extends $\mathcal{ALC}$ [11] with LTL constructs, but restricts the use of temporal operators to occur only in front of DL axioms.

In this paper, we consider the same temporal extension of DL in $\mathcal{ALC}$-LTL but under the answer set semantics for temporal logic programs provided by TEL, so that temporal $\mathcal{ALC}$ expressions can be combined with temporal logic programs. The resulting formalism, $\mathcal{ALC}$-TEL, conservatively extends TEL, hybrid theories and $\mathcal{ALC}$-LTL as particular cases. This work is a preliminary step to introduce the logic and informally explain its behavior using a simple example.

The rest of the paper is organized as follows. In the next section, we recall the basic definition of $\mathcal{ALC}$ and its translation to First Order Logic. In Sect. 3 we present the first order version of TEL as introduced in [12], but with a slight modification to allow open domains and capture $\mathcal{ALC}$ quantification. Section 4 defines the $\mathcal{ALC}$-LTL syntax whereas Sect. 5 incorporates those constructs into TEL using their first order translation together with some additional axiomatization. Finally, Sect. 6 concludes the paper.

2 Description Logic $\mathcal{ALC}$

The alphabet of an $\mathcal{ALC}$ theory [11, 13] is a triple $\langle N_C,N_R,N_I \rangle$ of mutually disjoint sets of names referring to concepts, roles and individuals, respectively. As an example, consider the alphabet $N_C=\{\mathtt{Disease},\mathtt{Treatment},\mathtt{Vaccine},\mathtt{Medication}\}$, $N_R=\{\mathtt{curedBy}\}$, $N_I=\{\mathtt{AIDS},\mathtt{Smallpox}\}$.

A concept (description) C is an expression that follows the grammar:

where $\mathtt{c}\in N_C$ is a concept name and $\mathtt{r}\in N_R$ a role name. We use the following abbreviations for concept descriptions:

for some concept name $\mathtt{c}\in N_C$. A general concept inclusion (GCI) axiom is an expression of the form $C \sqsubseteq D$ where C and D are concept descriptions. A T-Box is a set of GCI axioms. We sometimes write $C \equiv D$ as an element of a T-Box $\varTheta$ to mean that the two axioms $C \sqsubseteq D$ and $D \sqsubseteq C$ are elements of $\varTheta$. As an example, consider the T-Box:

$$\begin{aligned} \mathtt{Vaccine} \sqcup \mathtt{Medication} \sqsubseteq \mathtt{Treatment} \end{aligned}$$

(1)

$$\begin{aligned} \exists \mathtt{curedBy}.\mathtt{Treatment} \sqsubseteq \mathtt{Disease} \end{aligned}$$

(2)

meaning that vaccines and medications are treatments, and that anything cured by a treatment must be a disease. An assertion (axiom) is a construct of one of the forms:

$$ \mathtt{a}:C (\mathtt{a},\mathtt{b}):\mathtt{r}$$

where $\mathtt{a},\mathtt{b}\in N_I$ are individual names, $\mathtt{r}\in N_R$ is a role name and C is an arbitrary concept description. An A-Box is a set of assertions. For instance, the A-Box:

$$\begin{aligned}&\mathtt{Smallpox} \, : \, \exists \mathtt{curedBy}.\mathtt{Vaccine} \end{aligned}$$

(3)

$$\begin{aligned}&\qquad \mathtt{AIDS} \, : \, \mathtt{Disease} \sqcap \lnot \exists \mathtt{curedBy}.\mathtt{Treatment} \end{aligned}$$

(4)

tells us that smallpox is cured¹ by a vaccine whereas AIDS is a disease and has no treatment for its cure. The fact that $\mathtt{Smallpox}$ is a disease can be derived from the previous T-Box since it is cured by some vaccine, and the later is a treatment. A knowledge base $\langle \varTheta ,\varOmega \rangle$ consists of a T-Box $\varTheta$ and an A-Box $\varOmega$.

In the rest of the paper, we treat $\mathcal{ALC}$ through its standard First Order Logic translation (see for instance [13]). However, for the sake of completeness, we provide next the standard definition of the $\mathcal{ALC}$ semantics.

Definition 1

($\mathcal{ALC}$ interpretation). An $\mathcal{ALC}$ interpretation $\mathcal{I}$ is a pair $(\varDelta ^\mathcal{I},\cdot ^\mathcal{I})$ where $\varDelta ^\mathcal{I}$ is a non-empty set called the domain (containing individuals) and $\cdot ^\mathcal{I}$ is a mapping on $N_C \cup N_R \cup N_I$ that assigns: an individual $\mathtt{a}^\mathcal{I}\in \varDelta ^\mathcal{I}$ to each individual name $\mathtt{a}\in N_I$; a set of individuals $\mathtt{c}^\mathcal{I}\subseteq \varDelta ^\mathcal{I}$ to each concept name $\mathtt{c}\in N_C$; and a set of pairs of individuals $\mathtt{r}^\mathcal{I}\subseteq \varDelta ^\mathcal{I}\times \varDelta ^\mathcal{I}$ to each role name $\mathtt{r}\in N_R$.    $\square$

Definition 2

(Interpretation of concept descriptions). Given interpretation $\mathcal{I}=(\varDelta ^\mathcal{I},\cdot ^\mathcal{I})$ its extension to concept descriptions follows the recursive rules:

The interpretation of derived concepts can be easily deduced:

$$\begin{aligned} (C \sqcup D)^\mathcal{I}= & {} C^\mathcal{I}\cup D^\mathcal{I}\\ \top ^\mathcal{I}= & {} \varDelta ^\mathcal{I}\\ \bot ^\mathcal{I}= & {} \emptyset \\ (\forall \mathtt{r}.C)^\mathcal{I}= & {} \{d \in \varDelta ^\mathcal{I}\mid \text { all } d' \text { with }(d,d') \in \mathtt{r}^\mathcal{I}\text { satisfy } d' \in C^\mathcal{I}\} \end{aligned}$$

As expected, an interpretation $\mathcal{I}$ satisfies a GCI axiom $C \sqsubseteq D$, written $\mathcal{I}\models C \sqsubseteq D$, iff $C^\mathcal{I}\subseteq D^\mathcal{I}$. Similarly, we define satisfaction for assertions as: $\mathcal{I}\models \mathtt{a}:C$ iff $\mathtt{a}^\mathcal{I}\in C^\mathcal{I}$; and $\mathcal{I}\models (\mathtt{a},\mathtt{b}):r$ iff $(\mathtt{a}^\mathcal{I},\mathtt{b}^\mathcal{I}) \in r^\mathcal{I}$. Interpretation $\mathcal{I}$ is a model of a knowledge base $\langle \varTheta ,\varOmega \rangle$ iff it satisfies all GCIs in the T-Box $\varTheta$ and all assertions in the A-Box $\varOmega$.

As said before, we are interested in the translation of $\mathcal{ALC}$ into First Order Logic (FOL) [13]. Given an $\mathcal{ALC}$ alphabet $N_C \cup N_R \cup N_I$ we define the corresponding First Order signature with one unary predicate $\mathtt{c}(x)$ per each $\mathtt{c}\in N_C$, binary predicate $\mathtt{r}(x,y)$ per each $\mathtt{r}\in N_R$ and constant name $\mathtt{a}$ per each $\mathtt{a}\in N_I$. The FOL translation of a concept description C with respect to a free variable x is a formula denoted as $t_{x}(C)$ and recursively defined as follows:

Notice that y is a variable name² different from x and bound in $\exists y$. It is relatively easy to check that the translation of derived concepts can be captured by the following equivalent FOL formulas:

The translation of a GCI axiom $C \sqsubseteq D$ is defined as

$$t(C \sqsubseteq D) {\mathop {=}\limits ^\mathrm{def}}\forall x (t_{x}(C) \rightarrow t_{x}(D))$$

For instance, the translation of (2) corresponds to:

$$ \forall x (\exists y \ (\mathtt{curedBy}(x,y) \wedge \mathtt{Treatment}(y)) \rightarrow \mathtt{Disease}(x)) $$

We also define the translation of assertions as:

where $[x/\mathtt{a}]$ stands for the substitution of variable x by the individual name $\mathtt{a}$. As an example, the translation of (3) amounts to:

$$ \exists y \ (\mathtt{curedBy}(\mathtt{Smallpox},y) \wedge \mathtt{Vaccine}(y)) $$

Given a knowledge base $\langle \varTheta ,\varOmega \rangle$, we define its translation as the union $t(\varTheta ) \cup t(\varOmega )$ of the sets of translations of all GCIs in $\varTheta$ and assertions in $\varOmega$, respectively.

Proposition 1

There is a one-to-one correspondence between $\mathcal{ALC}$ models of $\langle \varTheta ,\varOmega \rangle$ and FOL models of $t(\varTheta ) \cup t(\varOmega )$.

3 Temporal Quantified Equilibrium Logic

The definition of Temporal Quantified Equilibrium logic we use in the current paper is an extension of a previous version defined in [12] to cope with open domains as in Quantified Equilibrium Logic from [7]. Syntactically, we consider function-free first-order languages $\mathcal {L} =\langle \mathcal{C},\mathcal{P}\rangle$ built over a set of constant symbols, $\mathcal{C}$, and a set of predicate symbols, $\mathcal{P}$. Additionally, each $p \in \mathcal{P}$ has an associated arity or number of arguments. An atom is any $p(t_1, \ldots , t_n)$ where $p \in \mathcal{P}$ is a predicate with arity $n\ge 0$ and each $t_i$ is a term, that is, a constant or a variable in its turn. We assume the existence of a binary equality predicate ‘$=$’ $\in \mathcal{P}$, written in infix notation. Using $\mathcal {L}$, connectors and variables, an $\mathcal {L}$-formula $\varphi$ is defined by following the grammar:

where $p(t_1,\dots ,t_n)$ is an atom, x is a variable and $\bigcirc$, $\text {U}$ and $\text {R}$ respectively stand for “next”, “until” and “release.” A theory is a finite set of formulas. We use the following derived operators:

$$ \begin{array}{rcl@{}rcl} \lnot \varphi &{} {\mathop {=}\limits ^\mathrm{def}}&{} \varphi \rightarrow \bot &{} \Diamond \varphi &{} {\mathop {=}\limits ^\mathrm{def}}&{} \top \ \text {U}\ \varphi \\ \top &{} {\mathop {=}\limits ^\mathrm{def}}&{} \lnot \bot &{} \Box \varphi &{} {\mathop {=}\limits ^\mathrm{def}}&{} \bot \ \text {R}\ \varphi \\ \varphi \leftrightarrow \psi &{} {\mathop {=}\limits ^\mathrm{def}}&{} (\varphi \rightarrow \psi ) \wedge (\psi \rightarrow \varphi ) \end{array} $$

for any formulas $\varphi ,\psi$. Note that $\lnot \varphi$ will be used to represent default negation. The application of i consecutive $\bigcirc$’s is denoted as follows: $\bigcirc ^i \varphi {\mathop {=}\limits ^\mathrm{def}}\bigcirc (\bigcirc ^{i-1} \varphi )$ for $i>0$ and $\bigcirc ^0 \varphi {\mathop {=}\limits ^\mathrm{def}}\varphi$. We say that a term, atom, formula or theory is ground if it does not contain variables. A sentence or closed-formula is a formula without free-variables (defined as usual). A theory $\varGamma$ is a set of sentences.

A universe is a pair $(\mathcal{D},\sigma )$ where $\mathcal{D}$ is a non-empty set called the domain and $\sigma$ is a mapping $\sigma :\mathcal{C}\cup \mathcal{D}\rightarrow \mathcal{D}$ satisfying $\sigma (d)=d$ for every $d\in \mathcal{D}$. We call d an unnamed individual if there is no constant $c \in \mathcal{C}$ with $\sigma (c)=d$. Throughout this paper, $\sigma$ is subject to the unique names assumption (UNA) stating that different individual names are mapped to different domain elements, that is, $\sigma (c) \ne \sigma (c')$ if $c \ne c'$ for any $c,c' \in \mathcal{C}$. This is a common assumption both in Description Logics and in Logic Programming. In fact, the latter usually makes a stronger assumption, taking the Herbrand Universe $(\mathcal{C},\sigma )$ where $\mathcal{D}=\mathcal{C}$, and so, $\sigma (c)=c$ for all $c \in \mathcal{C}$. In this paper, however, we adopt an open domain as in [7] to accommodate the use of quantification from Description Logic.

By $At_\mathcal{D}(\mathcal{C},\mathcal{P})$ we denote the set of ground atoms constructible from the language $\mathcal {L} '=\langle \mathcal{C}\cup \mathcal{D}, \mathcal{P}\rangle$. A first-order LTL-interpretation for language $\mathcal {L} =\langle \mathcal{C},\mathcal{P}\rangle$ is a structure $\langle (\mathcal{D},\sigma ),\mathbf {T} \rangle$ where $(\mathcal{D},\sigma )$ is a universe as above and $\mathbf {T}$ is an infinite sequence of sets, $\mathbf {T}=\{T_i\}_{i\ge 0}$ with $T_i \subseteq At_\mathcal{D}(\mathcal{C},\mathcal{P})$. Intuitively, $T_i$ contains those ground atoms that are true at situation i. For any $\mathbf {T}=\{T_i\}_{i\ge 0}$ and $k\ge 0$, by $\mathbf {T}[k]$ we denote the LTL-interpretation $\mathbf {T}=\{T_i\}_{i\ge k}$ that starts at the k-th position of $\mathbf {T}$. Given two sequences of sets $\mathbf {H}$ and $\mathbf {T}$ we say that $\mathbf {H}$ is smaller than $\mathbf {T}$, written $\mathbf {H}\le \mathbf {T}$, when $H_i \subseteq T_i$ for all $i\ge 0$. As usual, $\mathbf {H}< \mathbf {T}$ stands for: $\mathbf {H}\le \mathbf {T}$ and $\mathbf {H}\ne \mathbf {T}$.

Definition 3

A temporal quantified here-and-there (or just TQHT) interpretation is a tuple $\mathcal{M}$ = $\langle (\mathcal{D},\sigma ), \mathbf {H}, \mathbf {T}\rangle$ where $\langle (\mathcal{D},\sigma ), \mathbf {H}\rangle$ and $\langle (\mathcal{D},\sigma ), \mathbf {T}\rangle$ are two LTL-interpretations satisfying $\mathbf {H}\le \mathbf {T}$.    $\square$

In the definition above, we respectively call $\mathbf {H}$ and $\mathbf {T}$ the “here” and “there” components of $\mathcal{M}$. A TQHT-interpretation of the form $\mathcal{M}= \langle (\mathcal{D},\sigma ), \mathbf {T}, \mathbf {T}\rangle$ is said to be total. If $\mathcal{M}= \langle (\mathcal{D},\sigma ), \mathbf {H}, \mathbf {T}\rangle$ we write $\mathcal{M}[k]$ to stand for $\langle (\mathcal{D},\sigma ),\mathbf {H}[k],\mathbf {T}[k] \rangle$. The satisfaction relation for $\mathcal{M}=\langle (\mathcal{D},\sigma ), \mathbf {H}, \mathbf {T}\rangle$ and a formula $\alpha$, written $\mathcal{M}\models \alpha$, is recursively defined as follows:

where by $\varphi (d)$ we denote the replacement by d of all free occurrences of x in $\varphi (x)$. An interpretation $\mathcal{M}$ is a model of a theory $\varGamma$, written $\mathcal{M}\models \varGamma$, if it satisfies all the sentences in $\varGamma$. The resulting logic is called Temporal Quantified Here-and-There Logic with equality and static³ domains, and we simply abbreviate it as TQHT. It is not difficult to see that, if we restrict ourselves to total TQHT-interpretations, $\langle (\mathcal{D},\sigma ), \mathbf {T}, \mathbf {T}\rangle \models \varphi$ iff $\langle (\mathcal{D},\sigma ), \mathbf {T}\rangle \models \varphi$ in first-order LTL. Furthermore, the following properties can be easily checked by structural induction.

Proposition 2

For any formula $\varphi$, and interpretation $\langle (\mathcal{D},\sigma ), \mathbf {H},\mathbf {T} \rangle$:

• (i) if $\langle (\mathcal{D},\sigma ), \mathbf {H},\mathbf {T} \rangle \models \varphi$, then $\langle (\mathcal{D},\sigma ), \mathbf {T},\mathbf {T} \rangle \models \varphi$

• (ii) $\langle (\mathcal{D},\sigma ), \mathbf {H},\mathbf {T} \rangle \models \lnot \varphi$ iff $\langle (\mathcal{D},\sigma ), \mathbf {T},\mathbf {T} \rangle \not \models \varphi$

In general, it is clear that the other direction of (i) does not hold: any non-total interpretation contains atoms $\varphi =p(t_1,\dots ,t_n) \in T_i\setminus H_i$ for some $i \ge 0$. Without loss of generality, suppose $i=0$ (we can always take $\mathcal{M}[i]$ instead). Then, for those atoms, $\langle (\mathcal{D},\sigma ), \mathbf {T},\mathbf {T} \rangle \models \varphi$ but $\langle (\mathcal{D},\sigma ), \mathbf {H},\mathbf {T} \rangle \not \models \varphi$. Moreover, by (ii), the former also means $\langle (\mathcal{D},\sigma ), \mathbf {H},\mathbf {T} \rangle \not \models \lnot \varphi$, so we conclude that non-total interpretations falsify the formula $\varphi \vee \lnot \varphi$, a classical tautology known as the excluded middle axiom. This axiom is not valid either in intuitionistic logic or in the intermediate logic of Here-and-There [14], where ‘$\lnot$’ is weaker than classical negation. It is still possible to add this axiom for some predicates $p \in \mathcal{P}$ by forcing the condition:

The following results explain the effect of including (($\text {EM}_p$)) among the formulas of our theory.

Proposition 3

An interpretation $\mathcal{M}=\langle (\mathcal{D},\sigma ), \mathbf {H},\mathbf {T} \rangle$ satisfies ($\text {EM}_p$)for some $p \in \mathcal{P}$ iff, for all $i \ge 0$: $p(t_1,\dots ,t_n) \in T_i$ is equivalent to $p(t_1,\dots ,t_n) \in H_i$.

Corollary 1

Given language $\mathcal {L} =\langle \mathcal{C},\mathcal{P}\rangle$, let $\mathcal{P}' \subseteq \mathcal{P}$ be a subset of predicates and let $\mathcal{M}\models (\text {EM}_p)$ for all $p \in \mathcal{P}'$. Then, $\langle (\mathcal{D},\sigma ), \mathbf {H},\mathbf {T} \rangle \models \varphi$ amounts to $\langle (\mathcal{D},\sigma ), \mathbf {T},\mathbf {T} \rangle \models \varphi$ for any formula $\varphi$ in the language $\mathcal {L} =\langle \mathcal{C},\mathcal{P}' \rangle$.

Corollary 2

Given language $\mathcal {L} =\langle \mathcal{C},\mathcal{P}\rangle$, the addition of ($\text {EM}_p$)for all $p \in \mathcal{P}$ makes TQHT collapse into LTL.

As an illustration of TQHT satisfaction, consider the propositional formula:

$$\begin{aligned} \lnot inmune \rightarrow vulnerable \end{aligned}$$

(5)

This formula corresponds to the ASP ground rule:

Any model $\mathcal{M}=\langle (\mathcal{D},\sigma ), \mathbf {H}, \mathbf {T}\rangle$ of (5) must satisfy that $\langle (\mathcal{D},\sigma ), w, \mathbf {T}\rangle , 0 \not \models \lnot inmune$ or $\langle (\mathcal{D},\sigma ), w, \mathbf {T}\rangle , 0 \models vulnerable$ for all $w \in \{\mathbf {H},\mathbf {T}\}$. By Proposition 2 (ii), the former is equivalent to $\langle (\mathcal{D},\sigma ), \mathbf {T}, \mathbf {T}\rangle , 0 \models inmune$, that is, $inmune \in T_0$, whereas the latter ammounts to $vulnerable \in H_0$ for $w=\mathbf {H}$ and $vulnerable \in T_0$ for $w=\mathbf {T}$. Therefore, models of (5) are such that, if $inmune \not \in T_0$ then $vulnerable \in H_0 \subseteq T_0$.

To introduce non-monotonicity, we define a set of selected total TQHT models we will call temporal equilibrium models, or just temporal stable models, if we consider their corresponding LTL representation.

Definition 4

(Temporal Equilibrium Model). A temporal equilibrium model of a theory $\varGamma$ is a total model $\mathcal{M}=\langle (\mathcal{D},\sigma ),\mathbf {T},\mathbf {T}\rangle$ of $\varGamma$ such that there is no $\mathbf {H}< \mathbf {T}$ satisfying $\langle (\mathcal{D},\sigma ),\mathbf {H},\mathbf {T}\rangle \models \varGamma$. When this happens, we further say that the LTL-interpretation $\langle (\mathcal{D},\sigma ),\mathbf {T}\rangle$ is a temporal stable model of $\varGamma$.    $\square$

The logic induced by temporal equilibrium models is called Temporal Quantified Equilibrium Logic (TEL, for short). We can identify temporal logic programs with variables as a fragment of first order temporal theories. For a detailed definition of this fragment see [12]. In the previous simple example (5), we can observe that any total interpretation $\mathcal{M}=\langle (\mathcal{D},\sigma ),\mathbf {T},\mathbf {T}\rangle$ with $inmune \in T_0$ is a TQHT model, but we can always form another interpretation $\mathcal{M}'=\langle (\mathcal{D},\sigma ),\mathbf {H},\mathbf {T}\rangle$ with $H_0=T_0\setminus \{ inmune , vulnerable \}$ and $H_i=T_i$ for $i>0$ such that it is also a TQHT model of (5) but $\mathbf {H}< \mathbf {T}$, so $\mathcal{M}$ is not in equilibrium. If, on the contrary, $inmune \not \in T_0$, then the satisfaction of (5) requires $vulnerable \in H_0 \subseteq T_0$ for any TQHT model, and there is no way to form a smaller model by removing atoms in $T_0$. For the rest of situations $i>0$, any $T_i$ containing at least one atom can always be reduced to $H_i=\emptyset$ while keeping the satisfaction of (5), since this formula only affects to the initial situation. It is not difficult to see that the only temporal equilibrium model of (5) corresponds to $T_0=\{ vulnerable \}$ and $T_i=\emptyset$ for $i>0$. Let us consider next a more elaborated example.

Example 1

Take the following temporal logic program:

$$\begin{aligned} Person (x) \wedge Disease (y) \wedge \lnot Immune (x,y)\rightarrow & {} Vulnerable (x,y) \end{aligned}$$

(6)

$$\begin{aligned} \Box ( Immune (x,y)\rightarrow & {} \bigcirc Immune (x,y)) \end{aligned}$$

(7)

$$\begin{aligned} \Box ( Vulnerable (x,y) \wedge \lnot \bigcirc Immune (x,y)\rightarrow & {} \bigcirc Vulnerable (x,y)) \end{aligned}$$

(8)

$$\begin{aligned} \Box ( Vaccinate (x,y)\rightarrow & {} Immune (x,y)) \end{aligned}$$

(9)

$$\begin{aligned} \Box Person (\mathtt{John}) \wedge \Box Disease (\mathtt{Smallpox}) \end{aligned}$$

(10)

$$\begin{aligned} \bigcirc ^3 Vaccinate(\mathtt{John},\mathtt{Smallpox}) \end{aligned}$$

(11)

where we assume that all free variables in a formula are universally quantified. Formula (6) asserts that, initially, any person x is vulnerable to any desease y, unless we can prove it is immune. As we saw before, the effect of $\lnot \varphi$ in TEL is that of default negation of $\varphi$, that is, $\lnot \varphi$ holds when there is no evidence on $\varphi$. Formula (7) tells us that once somebody becomes immune to some disease, it remains so forever. A similar expression is (8), saying that someone vulnerable remains so, but this time is under the default condition that there is no evidence of becoming immune. Formulas of the form (8) are called inertia rules. The expression (9) means that the effect of vaccinating x against y is becoming immune. Finally, (10) contains some typing information saying that $\mathtt{John}$ is (always) a person and $\mathtt{Smallpox}$ is (always) a disease, whereas (11) asserts that $\mathtt{John}$ has been vaccinated at situation $i=3$. Program (6)–(11) has a temporal stable model $\langle (\mathcal{D},\sigma ),\mathbf {T} \rangle$ where $\mathcal{D}=\mathcal{C}=\{\mathtt{John},\mathtt{Smallpox}\}$, $\sigma$ is the identity relation and the only states making $Vulnerable (\mathtt{John},\mathtt{Smallpox})$ true are $i \in \{0,1,2\}$ whereas $Immune (\mathtt{John},\mathtt{Smallpox})$ becomes true for all $i \ge 3$. The rest of stable models only vary in the extension of $\mathcal{D}$ (we can have arbitrary unnamed individuals) and the assignment $\sigma$, provided that UNA is respected. Suppose we are said now that $\mathtt{John}$ has some genetic anomaly that made him immune to Smallpox from the very beginning. If we add the formula $Immune (\mathtt{John},\mathtt{Smallpox})$ to (6)–(11) then $Vulnerable (\mathtt{John},\mathtt{Smallpox})$ is never derived and we obtain $\Box Immune (\mathtt{John},\mathtt{Smallpox})$ as a conclusion. This last variation illustrates the non-monotonic behavior of TEL entailment relation.    $\square$

Without entering into further detail and just as an illustration, Fig. 1 shows an encoding of Example 1 in the language of the temporal ASP solver telingo [15]. The correspondence of program rules with the respective formulas (6)–(11) is pretty obvious in most cases. The only difference is that telingo uses the previous operator in rules representing transitions between two states, rather than the next operator. Thus, for instance, ’inmune(X,Y) must be read as “previously, inmune(X,Y) was true”. On the other hand, the next operator used on facts is represented as ${\texttt {>}}$, as we can see in the last line.

Fig. 1.

An encoding of Example 1 in the language of the temporal ASP solver telingo.

4 $\mathcal{ALC}$-LTL

The combination of description logics with temporal patterns is an important field of knowledge representation that has been widely studied in the literature (see, for instance, the surveys [16,17,18]). In a cornerstone paper, Baader, Ghilardi and Lutz [10] proposed the temporal extension $\mathcal{ALC}$-LTL where temporal operators are only introduced in front of $\mathcal{ALC}$ axioms, but not as concept constructors. This guaranteed decidability and significantly reduced the complexity of different reasoning tasks (depending on whether rigid roles are considered or not) while keeping enough expressiveness for solving many practical problems. According to [10], an $\mathcal{ALC}$-LTL formula $\varphi$ is defined by the grammar:

$$ \alpha \mid \varphi _1 \wedge \varphi _2 \mid \varphi _1 \vee \varphi _2 \mid \lnot \varphi \mid \varphi _1 \ \text {U}\ \varphi _2 \mid \bigcirc \varphi $$

where $\alpha$ is an $\mathcal{ALC}$ axioms. We assume the same abbreviations for temporal operators seen in Sect. 3. For $\mathcal{ALC}$-LTL formulas, $\varphi \rightarrow \psi$ can be defined as $\lnot \varphi \vee \psi$ and $\varphi \, \text {R}\, \psi$ can be defined as $\lnot ( \lnot \varphi \, \text {U}\, \lnot \psi )$ (something that, in general, TEL does not satisfy). The semantics for $\mathcal{ALC}$-LTL is provided in [10] by considering an infinite sequence $\{\mathcal{I}_i\}_{i\ge 0}$ of $\mathcal{ALC}$ interpretations $\mathcal{I}_i$. In our case, however, we will be more interested in the first order translation of $\mathcal{ALC}$-LTL. We assume that any $\mathcal{ALC}$ axiom $\alpha$ actually represents the first order formula $t(\alpha )$ as defined in Sect. 2. Then, an $\mathcal{ALC}$-LTL formula may be simply seen as an abbreviation of first order temporal formula. To give an example, the $\mathcal{ALC}$-LTL formula:

$$ \Diamond \Box (\mathtt{AIDS} : \exists \mathtt{curedBy}.\mathtt{Treatment}) $$

expresses the wish that a definitive treatment for AIDS is eventually found and, after applying translation $t(\cdot )$ becomes the first order temporal formula:

$$ \Diamond \Box \ \exists y (\mathtt{curedBy}(\mathtt{AIDS},y) \wedge \mathtt{Treatment}(y)) $$

Baader et al. define rigid concepts and roles as those whose interpretation does not vary along time (otherwise, they are called flexible instead). Using the FOL representation, for any rigid concept $\mathtt{c} \in N_C$ and rigid role $\mathtt{r} \in N_R$ we have:

$$\begin{aligned} \forall x \ (\mathtt{c}(x)&\leftrightarrow&\Box \mathtt{c}(x))\\ \forall x \forall y \ (\mathtt{r}(x,y)&\leftrightarrow&\Box \mathtt{r}(x,y)) \end{aligned}$$

5 $\mathcal{ALC}$-TEL

Following the encoding in [7] to incorporate hybrid theories in Equilibrium Logic, we describe now how $\mathcal{ALC}$ can be easily embodied in TEL. Given language $\mathcal {L} =\langle \mathcal{C},\mathcal{P}\rangle$ we suppose that $N_C \subseteq \mathcal{P}$ and $N_R \subseteq \mathcal{P}$ become unary and binary predicates, respectively, and that $N_I \subseteq \mathcal{C}$ become constant names. The crucial point in the encoding is the addition of the excluded middle axiom ($\text {EM}_p$)for every predicate $p \in N_C \cup N_R$. In this way, the translation of an $\mathcal{ALC}$ axiom is interpreted under classical FOL whereas the translation of any $\mathcal{ALC}$-LTL formula is interpreted under quantified LTL. The final result provides an expressive formalism that allows combining temporal logic programming and terminological knowledge. For instance, we can modify now our running example as follows.

Example 2

(Example 1 continued). We can incorporate axioms (1)–(4) assuming that $\mathtt{Vaccine}$, $\mathtt{Medication}$, $\mathtt{Treatment}$ and $\mathtt{Disease}$ are rigid concepts, whereas $\mathtt{curedBy}$ is flexible. We also include the rigid concept $\mathtt{Person}$ and the constant $\mathtt{John}$. Our logic program can be modified to include $\mathcal{ALC}$ expressions accordingly. For instance, we can keep untouched the formulas (7)–(9) and (11) since they do not refer to terminological knowledge, but we replace now (6) by⁴:

$$ (x : \mathtt{Person}) \wedge (y : \mathtt{Disease}) \wedge \lnot Immune (x,y) \rightarrow Vulnerable (x,y) $$

and (10) by the assertions:

$$ \mathtt{John}:\mathtt{Person} \mathtt{Smallpox}:\mathtt{Disease} $$

that do not need temporal operators, since these concepts are rigid.    $\square$

An important issue may occur when dealing with flexible concepts or roles. For instance, since $\mathtt{curedBy}$ is flexible, the fact that smallpox is cured by a vaccine, (3), is not guaranteed to persist throughout the temporal narrative. To do so, we can add a rule for strict persistence like (7) as follows:

$$ \Box (\mathtt{curedBy}(x,y) \rightarrow \bigcirc \mathtt{curedBy}(x,y)) $$

which works in this case since we can assume that a curable disease does not cease to be so. However, if we wanted to transform this rule into a general inertia default, it would not be directly possible, since $\mathtt{curedBy}$ behaves as a classical predicate due to ($\text {EM}_p$). An additional auxiliary predicate could still be used for that purpose. A more ambitious solution would be removing the ($\text {EM}_p$)axiom and allowing concepts and roles to behave as logic programming predicates. This would allow expressing defaults on Description Logic axioms, but would depart from the standard interpretation of $\mathcal{ALC}$.

6 Conclusions

We have defined a logical formalism $\mathcal{ALC}$-TEL that, under a modal temporal basis, combines the Description Logic $\mathcal{ALC}$ [11] with logic programming under Equilibrium Logic semantics. On the one hand, if we disregard the temporal operators, this formalism embeds hybrid theories from [7], allowing the combination of description logics (in our case, $\mathcal{ALC}$) with logic programming. On the other hand, if we add the excluded middle axiom ($\text {EM}_p$)  for all the predicates in the language, $\mathcal{ALC}$-TEL collapses into $\mathcal{ALC}$-LTL as defined by Baader et al. in [10]. Moreover, $\mathcal{ALC}$ is encoded in terms of its First Order translation, so that, once $\mathcal{ALC}$ expressions are translated, we simply get Temporal (Quantified) Equilibrium Logic [6, 12] as underlying formalism.

The current proposal opens the exploration of many possible directions. A first obvious line of future work is the study of syntactic fragments and the analysis of complexity for their satisfiability problem. An obviously related line has to do with implementation. For instance, model checking techniques have been applied both to $\mathcal{ALC}$-LTL [19] and to TEL [20, 21] and their efficient combination could be a interesting topic for future investigation. An adaptation of TEL for practical problem solving in the spirit of ASP has led to a variant [15] defined on finite traces and its corresponding ASP solver, telingo. The $\mathcal{ALC}$-TEL formalism may help us to incorporate terminological knowledge in telingo in the form of DL knowledge bases. Besides, the use of finite traces on temporal description logics has also been recently proposed in [22]. Another exploratory line could be a more integrated combination of DL and logic programs where defaults were also introduced in DL concepts and roles. Finally, another possible research direction is the use of $\mathcal{ALC}$-TEL in application domains that involve temporal reasoning and rich ontologies, following similar steps as [23] in the medical domain.