The newly introduced ALCP(D) extends ALC with path constraints over concrete domains D. Previous work showed decidability of the satisfiability problem in ALCP(D) for various concrete domains, including integer domains. However, the proof of this general result did not provide a complexity upper bound on the problem, or an explicit algorithm for model construction, which is necessary for some reasoning tasks such as abduction. In this paper, we initiate an investigation of the complexity of the satisfiability and model construction problems in ALCP(Z), where Z = hZ; =; <i. As a preliminary result towards establishing complexity upper bounds, we present a procedure for deciding satisfiability in a constructive way.
Introduction
Reasoning in description logics (DL) with the addition of data from concrete domains
is a highly relevant research problem motivated by the practical need to include data
values and express constraints on top of them in ontologies. Di erent extensions of
DLs with concrete domains were investigated [
The language ALCP(D), recently introduced by Carapelle and Turhan [
In this paper, we take initial steps towards a constructive satisfiability procedure for
ALCP(Z), where Z = hZ; =; <i is the structure induced on the integers by the equality
and linear order relations. Our satisfiability procedure is split into two parts. Firstly,
ALC satisfiability is checked for an abstraction of the TBox and the target concept,
similarly to Carapelle and Turhan [
The paper is structured as follows. After providing necessary background in Section 2, we introduce integer graphs in Section 3, and discuss their relationship to models of ALCP(Z) concepts. In Sections 4 and 5 we present procedures for constructing integer graphs and extracting a satisfying interpretation from them. Finally, in Section 6, we discuss the results and future research. Due to space limitations, the proofs are sketched or omitted. 2
Preliminaries for ALC P(Z)
The ALCP(D) description logics were defined by Carapelle and Turhan [
Example 1. Throughout the paper we return to the same examples to demonstrate concepts and definitions. We underline symbols introduced in the examples to distinguish them from the rest of the paper.
Let 1(y; z) := y < z and 2(x; z) := z < x. The constraint 1;2(x; y; z) := 1(y; z) ^ 2(x; z) has arity 3, and we have Z j= 1;2(3; 1; 2).
Let NC, NR, and Reg be countably infinite sets of concept names, role names, and register names, respectively. A sequence P = r1 rn, where ri 2 NR for i 2 [n], is a role path of length n. ALCP(Z) concepts C are inductively defined by:
C; D := A j :C j (C u D) j 9r:C j 9P:c(Si1 x1; : : : ; Sik xk) where A 2 NC, r 2 NR, P is a role path of length n 0, c is a constraint of arity k, x1; : : : ; xk 2 Reg, and 0 i1; : : : ; ik n. We call 9P:c(Si1 x1; : : : ; Sik xk) a path constraint. The symbol S appearing in the path constraint stands for successor, as the term Si x points to the register variable x of the i-th element on the path P.
A Z-interpretation I is a tuple ( I; I; ), where I is the domain, I is the interpretation function, and : I Reg ! Z is the valuation function, assigning an integer value to each register variable of each element in the domain. The interpretation function maps each concept name A 2 NC to some AI I and each role name r 2 NR to a binary relation rI I I. The interpretation function is then extended to :C; C u D; 9r:C as usual.3 Let P = r1; : : : ; rn be a role path of length n.
Then PI is defined by: PI = f(v0; : : : ; vn) 2 ( I)n+1 j (vi 1; vi) 2 riI for i 2 [n]g, and (9P:c(Si1 x1; : : : ; Sik xk))I is defined by: fv 2
I j 9(v0; : : : ; vn) 2 PI s.t. v0 = v; and Z j= c( (vi1 ; x1); : : : ; (vik ; xk))g
We explain the interpretation of 9P:c(Si1 x1; : : : ; Sik xk) further. If an element v 2 I is in (9P:c(Si1 x1; : : : ; Sik xk))I, then there are v1; : : : ; vn 2 I such that there is a path starting at v which matches the pattern P, that is (v; v1; : : : ; vn) 2 PI, and such that for the assignment (v ji ; x j) 7! a j, we have Z j= c(a1; : : : ; ak).
Example 2. Let C := 9rst:
1;2(x; y; z) ^ 3;4(S1 x; S2 x; S3 x) where:
3;4(S1 x; S2 x; S3 x) := 3(S1 x; S2 x) ^ 4(S2 x; S3 x)
3(S1 x; S2 x) := S1 x < S2 x
4(S2 x; S3 x) := S2 x = S3 x
The interpretation of C would contain elements v0 from which a path rst originates,
meaning there are elements vi, i 2 [
As usual, C t D := :(:C u :D) and 8R:C = :9R::C, > := A t :A are defined as syntactic sugar. In addition, also define 8P:c(Si1 x1; : : : ; Sik xk) := :9P::c(Si1 x1; : : : ; Sik xk) and 9P:C := 9r1:9r2: : : : 9rn:C. A General Concept Inclusion (GCI) is an expression C v D, where C and D are concepts. A TBox is a finite set of GCIs. For a concept C and TBox T , denote by RegC;T the set of register names appearing in C and T . Models and satisfiability are also defined as usual: let T be a TBox and let C be a concept. A Z-interpretation I models T if and only if CI DI for every GCI C v D in T . We denote I j= T in this case. C is satisfiable w.r.t. T i there is a Z-interpretation I which models T and CI , ;. We denote I j=T C in this case.
We say I is tree-shaped if I ? is (isomorphic to) a prefix-closed set of strings
over some finite alphabet , and if additionally, for u; v 2 I, we have u ! v if and
ownellyl-kifnvow=n uresuflotrfosromAeLC, 2[
Relying further on the treatment in [
Fix a concept C and a TBox T in constraint normal form. For an atomic constraint (Si x; S jy), we call d = maxfi; jg the depth of , and for a constraint c, the depth is the maximal depth of the atomic constraints in c. Denote by the set of atomic constraints occurring in C and T . Let B = fB1; : : : ; Bj jg be a set of fresh concept names, called placeholders, which do not appear in C or T .
We can now define abstracted concepts and constraint graphs, which allow us to split the satisfiability check into testing usual ALC-satisfiability of the abstracted TBox, and verifying the constraints in the appropriate constraint graph can be satisfied. Definition 2 (Abstracted concepts). Let P = r1 : : : rn and let 1; : : : ; m 2 have depths d1 : : : dm, respectively. Define d0 = 0 and dm+1 = n. For a conjunction c of 1; : : : ; m, the abstraction of 9P:c(Si1 x1; : : : ; Sik xk) is defined as: 9P1:(B1 u 9P2:(B2 u 9Pm:(Bm u 9Pm+1:>) )) )): where 9Pi is short for 9rdi 1+1 : : : 9rdi . If di = di+1 then 9Pi+1 is empty. For a disjunction c0 of 1; : : : ; m, the abstraction of 8P:c0(Si1 x1; : : : ; Sik xk) is defined as: 8P1:(B1 t 8P2:(B2 t
8Pm:(Bm t 8Pm+1:?) Define Ca and Ta to be the ALC concept and TBox, respectively, obtained by replacing every path constraint with its abstraction.
Example 3. The abstraction of C is given as follows. We have n = 3, m = 4, d0 = d1 = d2 = 0, d3 = 2, and d4 = d5 = 3. We have that 9P1, 9P2, and 9P5 are empty, and 9P3 = 9r9s, and 9P4 = 9t. All in all, we have:
Ca := B1 u B2 u 9r9s:B3 u 9t:B4 u (>) An ordinary interpretation I that models Ca is shown in Figure 1, where ai is shorthand for i repetitions of a. Note that elements in the interpretation of a path-constraint are at the origins of the paths, whereas in the abstraction, the placeholders are satisfied by elements along the path, with the d-th element satisfying the placeholders for constraints of depth d.
a1 B1; B2 r a2 s a3 B3 t a4
B4
For a graph G, we denote by V(G) its set of vertices and by E(G) its set of edges. Definition 3 (Constraint graph). Given an ordinary tree-shaped interpretation I = ( I; I), the constraint graph of I is the edge-labeled graph GI = (G; ) where V(G) =
I RegC;T , and : E(G) ! fl=; l<g, and E(G) are as follows. For every (u; x); (v; y) 2 V(G) and 2 f=; <g, we have ((v; y); (u; x)) 2 E(G) and ((v; y); (u; x)) = l i 1. u is a prefix of v, and 2. there exists B j 2 B such that j = (Sjvj jujy; x) or j = (x; Sjvj jujy), and v 2 B Ij. Let p¯ be a (finite or infinite) path in I. The constraint graph GI;p¯ is given by the labeled subgraph of GI induced by f(u; x) j u 2 I; u is on the path p¯; x 2 RegC;T g: <
Example 4. The constraint graph of I from Example 3 is shown in Figure 2.
Theorem 4 ([
A tableau reasoner may be used to verify that I j=Ta Ca. As I may be infinite,
such a reasoner constructs a finite representation of I in which the infinite parts of
I are represented by paths between blocking and blocked nodes. The infinite version
can be obtained by a construction known as unraveling. For more details, see [
In this section we define integer graphs, which represent such homomorphisms in a general form. As the extraction of homomorphisms from a general integer graph is somewhat cumbersome, we also introduce compacted integer graphs which simplify said extraction.
Let G be a (possibly infinite) directed graph. Define LPathG : V(G)2 ! Z+ [ f1g as follows. For u; v 2 V(G), LPathG(u; v) is undefined if v is not reachable from u, is equal to k if k is the length of the longest path from u to v, and is equal to 1 if for every k 2 Z+, there is a path of length at least k from u to v. Let be an equivalence relation on V(G). For v 2 V(G), denote the equivalence class of v in by [v] . The quotient graph G= is given by V(G= ) = f[v] j v 2 V(G)g, and:
E(G= ) = f([u] ; [v] ) j (u0; v0) 2 E(G) for some u0 2 [u] ; v0 2 [v] g: Define I to be the equivalence relation on V(GI) induced by the reflexive symmetric transitive closure of the edges in E(GI) labeled with l=. Define G< = (V(GI); E<(GI)) I where E<(GI) = fe 2 E(GI) j I(e) = l<g. For a path p¯ in I, define p¯ and G<p¯ similarly. Definition 6 (Integer graph). Let be an equivalence relation on V(GI) such that LPIartehfiHne(sa; b,)a,nd1d,ewnoetesaGy<IH= ibsyaHn Iin.tIefgHerIgirsapahcy.cWliec saanydHif f oisr aevceormypaa;cbte2d Vin(tHegIe)r, graph ifI, in addition, for everyIa; b 2 V(H ), either a is reachaIble from b or vice versa. For a path p¯ in I and such that p¯ refinIes , define Hp¯ similarly.
When H I is an integer graph, we often refer to it as the integer graph of I.
I Definition 7 (Vertex contraction). Let G = (V(G); E(G)) and let a; b 2 V(G). The result of contracting a and b, denoted G=fa;bg, is given by replacing a and b with a fresh vertex c whose neighborhood is the union of the neighborhoods of a and b. That is, V(G=fa;bg) = (V(G) n fa; bg) [ fcg and for every a0 2 V(G) n fa; bg, we have (a0; c) 2 E(G=fa;bg) i f(a0; a); (a0; b)g \ E(G) , ; (and similarly for (c; a0)). If G is quotient graph, the fresh vertex c is the union of the equivalence classes a and b.
Notice that vertex contractions do not introduce new edges. For a quotient graph G= , we have that the equivalence relation refines the equivalence relation obtained after contracting vertices in G= . Hence, we have that all the integer graphs of a given model I can be obtained from H I by contracting vertices in H I . Moreover, we have:
I I Lemma 8. If H I is an integer graph, I has a compacted integer graph.
I Example 5. The equivalence relation I of I from Example 3 only contains the pair ((a3; x); (a4; x)). The integer graph H I is shown in Figure 3(a) with the isolated ver
I tices omitted. A compaction of H I is given by the integer graph induced by the equiv
I alence relation , where: (a3; x) is equivalent to (a4; x), (a1; x) is equivalent to (a2; x), and (a1; y), (a2; y), (a2; z), (a3; y), (a3; z), (a4; y), (a4; z) are equivalent to each other, and (a1; z) is only equivalent to itself. Note that I indeed refines , H (shown in Figure 3(b)) is acyclic, and for any pair of vertices, one is reachable from another. The vertex [(a1; y)] denotes the equivalence class f(a1; y); (a2; y); (a2; z); (a3; y); (a3; z); (a4; y); (a4; z)g. f(a1; y)g f(a1; z)g f(a1; x)g [(a1; y)] f(a1; z)g f(a2; x)g f(a3; x); (a4; x)g f(a1; x); (a2; x)g
f(a3; x); (a4; x)g (a) H I
I
(b) H
Note that integer graphs naturally induce a homomorphism (in fact, infinitely many) from GI to Z, as they are directed acyclic graphs: Observation 9. Let H be an integer graph. There exists a function num : V(H) ! Z such that for a; b 2 V(H) where a , b, if b is reachable from a, then num(a) < num(b).
This allows us to reduce the problem of deciding the existence of a homomorphism to checking whether there exists an integer graph for I: Lemma 10. There is a homomorphism from GI to Z i I has an integer graph.
Combining this with the previous result of Carapelle and Turhan, we have: Corollary 11. C is satisfiable w.r.t. T if and only if there exists an ordinary model I of Ca w.r.t. Ta which has an integer graph.
The next lemma will allow us to break the task of deciding whether I has an integer graph into simpler steps: Lemma 12. I has an integer graph if and only if every path in I which starts at the root has an integer graph.
Proof (Sketch). One direction is immediate. For the other direction, assume every path starting at the root in I has an integer graph. We show the claim by induction on the number T of (blocked or maximal and finite) paths in I. The case where T = 1 is immediate. Assume the claim holds for T . Let I have T + 1 such paths which all have integer graphs. Let p¯ be one of these paths, and consider the sub-tree I0 induced by the T paths in I other than p¯. Then by the induction hypothesis, I0 has an integer graph HI0I0 . Let Hp¯ p¯ be the integer graph of p¯. Let Ip¯ denote the elements on p¯, and let I0 denote the elements in I0. Then the integer graph H I of I is as follows. H I is given I I by taking the disjoint union of Hp¯ p¯ and H 0I0 and contracting (see Definition 7) the
I vertices [(u; x)] p¯ and [(u; x)] I0 for every u 2 Ip¯ \ I0 and x 2 RegC;T .
We have now established that in order to check satisfiability of C w.r.t. T , it is enough to obtain an ordinary tree-shaped model I for their abstractions and to check that each path in I starting at the root has an integer graph. 4
Constructing Integer graphs In this section, we describe how the existence of an integer graph for a path in I can be tested. First, observe that for finite paths, this task is simple: Observation 13. Let p¯ be a finite path in I. It is straightforward to construct its constraint graph Gp¯ , compute p¯ and then construct the graph Hp¯ p¯ and test it for for being acyclic, as these are all finite structures. Together with the construction described in the proof of Lemma 12, we have that we can compute the integer graph (if it exists) of any finite tree-shaped prefix of I.
We still need conditions for the existence of integer graphs for infinite ultimately
periodic paths which can be verified in finite time.4 Such paths ¯ ( ¯)! require caution,
since it is possible for their prefixes ¯ ( ¯)t have an integer graph for any t 2 Z+ while
they themselves do not. This behavior is demonstrated in the following example:
4 We will sometimes abuse notation and denote an ultimately periodic path by ¯ ( ¯)!, where ¯
and ¯ list the labels appearing in the non-periodic and respectively periodic parts of the path.
Example 6. Let 5 := x = S1 x, 6 := y = S1y, and 7 := z < S1z, and let B5;6;7
be a placeholder for 5 ^ 6 ^ 7. Let B1;2 be a placeholder for 1;2 (see Example 1).
Consider the ultimately periodic path b1b2 : : :, where b1 is labeled with B1;2 and for
i 2, bi is labeled with B5;6;7. Essentially, these constraints fix two integer values,
held in the x and y registers, and with each repetition of B5;6;7, add a fresh integer
value between them. Hence, for any t 2 Z+, b1 : : : bt+1 has an integer graph which is
a simple path of length t + 1, since for any t 2 Z+ there is a choice of two integer
values with enough di erent values between them. See Figure 4 for the integer graph of
b1 : : : b4, with the isolated vertices omitted and where [(b1; x)] = f(bi; x) j i 2 [
[(b1; x)] f(b4; z)g f(b3; z)g f(b2; z)g f(b1; z)g [(b1; y)]
We first need to introduce the notion of integer graph extensions, which can be roughly seen as the subgraph relation adapted to quotient graphs: Definition 14 (Integer graph extension). Let H0 and H be integer graphs. We say H0 extends H if for every [v] 2 V(H), 1. there exists [v0] 2 V(H0) such that [v] [v0], and 2. if ([u]; [v]) 2 E(H) for some [u] 2 V(H), then ([u]; [v]) 2 E(H0).
Lemma 15. Let p¯ be a (finite or infinite) path in I and let ¯ be a prefix of p¯. If p¯ has an integer graph Hp¯ , then ¯ has an integer graph H ¯ and Hp¯ extends H ¯ .
The behavior in Example 6 we wish to avoid, namely, having the length of the longest path between two vertices grow in subsequent extensions, can be expressed using the following: Definition 16 (Non-disrupting extensions). Let H00, and H0, and H be integer graphs such that H00 extends H0 and H0 extends H. We say that H00 extends H0 without disrupting H if for every u; v 2 V(H), LPathH0 (u; v) = LPathH00 (u; v).
Through these two notions we can characterize the (finite or infinite) paths which have integer graphs, using conditions which can be verified in finite time. The following lemma is the most technically involved result of the paper. Recall that n denotes the maximal depth of constraints appearing in I.
Lemma 17. Let p¯ = ¯ ( ¯)! be an ultimately periodic path in I, beginning at the root. Then p¯ has an integer graph if and only if: (C) ¯ ( ¯)n+1 has an integer graph Hp¯;n+1 which extends Hp¯;n without disrupting Hp¯;1, where Hp¯;1 and Hp¯;n are the integer graphs of ¯ ( ¯) and ¯ ( ¯)n, respectively.
The following example shows that the bound in Lemma 17 on the number n + 1 of repetitions needed is tight: Example 7. Let 8 := x < y with placeholder B8 and let 9;10 := (x < S3 x) ^ (S3y < y) with placeholder B9;10. Consider the path u1u2 : : :, where if i = 1 mod 4, ui is labeled with B8, and otherwise ui is labeled with B8 u B9;10. It is straightforward, albeit tedious, to verify that the integer graph of u1u2u3u4 is disrupted by its extensions up to i = 16. Also note that condition (C) may be verified for a path ¯ ( ¯)! in finite time; by Observation 13, it is straightforward to construct the graphs Hp¯;1, Hp¯;n, Hp¯;n+1 and to verify they are acyclic. Then it is immediately verifiable that for every u; v 2 V(Hp¯;1), it holds that LPathHp¯;n (u; v) = LPathHp¯;n+1 (u; v).
Proof (Sketch). Recall that I, and therefore also p¯, satisfies the blocking condition described in Remark 5. To reduce notational clutter, in this proof we omit p¯ and denote by Ht the integer graph of ¯ ( ¯)t where relevant.
Our blocking condition allows us to define a graph operation which, in a way, appends some fixed graph induced by the periodic part of p¯ to Ht in order to obtain Ht+1. This regularity in the structure of the integer graphs of the prefixes of p¯ allows us to show that if condition (C) holds, then (*) for every t 2 Z+, ¯ ( ¯)t+n has an integer graph Ht+n which extends Ht+n 1 without disrupting Ht. We can further show that acyclicity is preserved when taking the limit H1 = limt!1 Ht. Therefore, if H1 is not the integer graph of p¯, there are u; v 2 V(H1) such that LPathH1 (u; v) = 1. Fix such u and v. Let t 2 Z+ be the minimal number for which u; v 2 V(Ht). We have that ¯ ( ¯)t is finite, so Ht is a finite directed acyclic graph, therefore LPathHt (u; v) is also finite. Since by our assumption, LPathH1 (u; v) = 1, there exists some minimal t0 t + n for which LPathHt0 (u; v) > LPathHt (u; v). Then we have that Ht0 disrupts Ht. In fact, we have that Ht0 disrupts Ht00 for every t t00 < t0. In particular, for t00 = t0 n we have that t t00 < t0, so Ht0 = Ht00+n disrupts Ht00 while extending Ht00+n 1, in contradiction to (*). We conclude that there are no u; v 2 V(H1) such that LPathH1 (u; v) = 1. Therefore H1 satisfies all conditions of Definition 6, making it the integer graph of p¯.
For the other direction, assume that p¯ has an integer graph H. First, note that ¯ ( ¯)t is a prefix of p¯ for every t 0. Therefore, by Lemma 15, for every t 2 Z+, ¯ ( ¯)t has an integer graph Ht. Furthermore, for every t < t0, we have that Ht0 extends Ht. In particular, this is true for t = n and t0 = n + 1. Therefore, to satisfy condition (C), it remains to show that Hn+1 does not disrupt H1 when extending Hn.
Assume for contradiction that Hn+1 does disrupt H1 when extending Hn. Then, relying on the fact that the depth of the placeholders in ¯ is limited by the length of ¯, we can show that there are w; w0 2 V(H1) such that LPathHt (w; w0) < LPathHt+1 (w; w0) for every t n. Since the length of the longest path between w and w0 grows with each t, we have that for every k 2 Z+, there exists some tk 2 Z+ such that LPathHtk (w; w0) > k. Hence, in H, we have that LPathH(w; w0) = 1, in contradiction to our assumption that H is an integer graph. We conclude that Hn+1 does not disrupt H1 when extending Hn, and condition (C) holds.
Putting it Together – the Constructive Procedure It remains to construct an assignment to the registers. Since a homomorphism can be easily extracted from a compacted integer graph, we show in this section that such compactions are e ectively computable. Let P¯ fin be the set of maximal finite paths in I beginning at the root, and let P¯ prd be the set of infinite ultimately periodic paths in I beginning at the root. For t 2 Z+, let Ut = fu 2 p¯ j p¯ 2 P¯ fing [ fu 2 ¯ ( ¯)t j ¯ ( ¯)! 2 P¯ prdg. That is, all elements that appear either on maximal finite paths or by the t-th iteration of the ultimately periodic paths. Define It be the sub-tree of I induced by the elements in Ut. Let u1; u2; : : : be a lexicographical ordering of I RegC;T .
Input: An integer graph Ht of It for t 2 Z+ Output: A compaction Ht;c of Ht 1: V(Ht;c) = V(Ht) 2: E(Ht;c) = E(Ht) 3: a = [u1] 4: for b; b0 2 V(Ht;c) do 5: if LPathHt;c (a; b) = LPathHt;c (a; b0) 2 Z or LPathHt;c (b; a) = LPathHt;c (b0; a) 2 Z then 6: contract b and b0 in V(Ht;c) . We refer to the equivalence classes in Ht;c 7: for i = 2; : : : ; jV(Ht)j do 8: if a is not reachable from [ui] in Ht;c nor vice versa then 9: contract a and [ui] in V(Ht;c) 10: 11: 12: 13: a = [ui] for b; b0 2 V(Ht) do if LPathHt;c (a; b) = LPathHt;c (a; b0) 2 Z or LPathHt;c (b; a) = LPathHt;c (b0; a) 2 Z then contract b and b0 in V(Ht;c) 14: Ht;c = (V(Ht;c); E(Ht;c)) 15: return Ht;c Lemma 18. Let t 2 Z+ and let Ht be the integer graph of It. There is an e ectively computable compaction Ht;c of Ht.
Proof (Sketch). We claim that Algorithm 1 outputs a compaction of Ht. Acyclicity is preserved by operations in Lines 6, 9, and 13. As for the reachability condition, first note that for every b 2 V (Ht;c), either b is reachable from [u1] or vice versa. Let b; b0 2 V (Ht;c). Assume for contradiction that b is not reachable from b0 nor vice versa. Then, either both b; b0 are reachable from [u1], or [u1] is reachable from both. Assume w.l.o.g. that it is the former. If LPathHt (u1; b) = LPathHt (u1; b0), then b and b0 would have been contracted during the run of the algorithm. Therefore either LPathHt (u1; b) < LPathHt (u1; b0) or LPathHt (u1; b) > LPathHt (u1; b0). If LPathHt (u1; b) < LPathHt (u1; b0), there is some b00 2 V (Ht;c) such that LPathHt (u1; b0) = LPathHt (u1; b00)+LPathHt (b00; b0) and such that LPathHt (u1; b00) = LPathHt (u1; b). Hence, b and b00 would have been contracted during the run of the algorithm, producing a path from b to b0, in contradiction to our assumption. The other case is analogous. Therefore, for every b; b0 2 V(Ht;c), either b is reachable from b0 or vice versa, making Ht;c a compacted integer graph. Theorem 19. Let I have an integer graph. There is an e ectively computable valuation function : I RegC;T ! Z such that ( I; I; ) satisfies C w.r.t. T . Proof (Sketch). We describe a procedure which, given input (u; x) 2 RegC;T , outputs an integer value. It first constructs a compacted integer graph using Observation 13 and Algorithm 1, then assigned it a value based on the length of the longest path between [(u; x)] and [("; x1)]. For t 2 Z+, denote by Ht the integer graph of It. Let t 2 Z+ be the minimal t for which [(u; x)] appears in Ht, and denote t0 = t + n + 1. Generate Ht0 using Observation 13 and then generate the compacted Ht0;c using Algorithm 1. Denote [(u; x)] = b and [("; x1)] = a and return (u; x) = LPathHt0;c (b; a) if LPathHt0;c (b; a) 2 Z+, and (u; x) = LPathHt0;c (a; b) otherwise. Recall that for every b 2 V(Ht;c) we have that either b is reachable from a or vice versa, therefore is well-defined. Also note that our blocking condition together with Lemma 17 guarantee that the length of the longest path between two vertices is final after n iterations, therefore, if [(u; x)] is reachable (and di erent) from [(v; y)], then (u; x) > (v; y). Now apply Lemma 10. 6
Conclusion ALCP(D) is an interesting family of DLs which enable the expression of constraints over register values of individuals along a specified path, where the values and the constraints are over a domain structure D. In this work, we have provided a constructive satisfiability procedure for ALCP(Z) instantiated to the integer domain Z = hZ; =; <i. The construction is two-fold: in order to construct the Z-model of an ALCP(Z) concept C w.r.t. a TBox T , first an ordinary ALC-model I is constructed for the abstracted versions of T and C; and consecutively the so-called integer graph of I, which provides a general representation of the relationships between the registers, is constructed and used for assigning the registers with values from Z.
We believe that this result will enable to employ ALCP(Z) in reasoning tasks where
model construction is required, e.g., ABox abduction and query answering. Although
complexity issues were not addressed in this paper, a complexity upper bound can be
obtained by analyzing our procedures. This would already be an improvement, as the
reductions in [
Acknowledgments. We thank Mantas Šimkus for comments on early stages of this work, and we are grateful to the anonymous reviewers for their fruitful comments. This work was supported by the FWF (project W1255).