The Curse of Finiteness: Undecidability of Database-Inspired Reasoning Problems in Very Expressive Description Logics? Sebastian Rudolph TU Dresden Germany sebastian.rudolph@tu-dresden.de Abstract. Recently, the field of knowledge representation is drawing a lot of inspiration from database theory. In particular, in the area of description logics and ontology languages, interest has shifted from satisfiability checking to query answering, with various query notions adopted from databases, like (unions of) conjunctive queries or different kinds of path queries. Likewise, the finite model semantics is being established as a viable and interesting alternative to the tradi- tional semantics based on unrestricted models. In this paper, we investigate diverse database-inspired reasoning problems for very expressive description logics (all featuring the worrisome triad of inverses, counting, and nominals) which have in common that role paths of unbounded length can be described (in the knowledge base or of the query), leading to a certain non-locality of the reasoning problem. We show that for all the cases considered, undecidability can be established by very similar means. Most notably, we show undecidability of finite entailment of unions of conjunc- tive queries for a fragment of SHOIQ (the logic underlying the OWL DL ontol- ogy language), and undecidability of finite entailment of conjunctive queries for a fragment of SROIQ (the logical basis of the more recent and popular OWL 2 DL standard). Introduction Over the past two decades, fostered by the growing practical impact of DL research, the scope of interest has widened to include new types of reasoning problems. Thereby, not very surprisingly, the area of databases has been an important source of inspiration. In fact, the fields of logic-based knowledge representation and reasoning have been significantly converging over the past years and seen a lot of cross-fertilization [24]. Two major conceptual contributions of database theory can be identified: query an- swering as the central reasoning problem and finite-model semantics. Query Answering As opposed to satisfiability checking, evaluating queries in the presence of a background knowledge base (referred to as ontology-based query answer- ing) allows us to express more complex information needs. A very basic, yet prominent ? This is a shortened version of a paper accepted at KR’16 [25], appended to this submission. Definitions common in the DL community and proofs have been omitted due to space reasons. query formalism often encountered in databases and nowadays in description logics is that of conjunctive queries (CQs) corresponding to the SELECT-PROJECT-JOIN frag- ment of SQL [12] and unions of conjunctive queries (UCQs). Answering conjunctive queries over DL knowledge bases was first mentioned as a topic in the 1990s [17] and since then investigated for a great variety of description logic languages. The most ex- pressive DLs with inverses, counting, and nominals where CQ and UCQ entailment1 are known to be decidable are ALCHOIQb [26] and Horn-SROIQ [20]. In the context of semi-structured databases, other query formalisms have been de- veloped which allow for expressing information needs related to reachability, so-called path queries or navigational queries [8]. Beyond expressing more elaborate informa- tion needs, such queries can also be used to internalize ontological knowledge into the query to a certain degree [3]. Over the past decade, a variety of results regarding answering of (diverse variants of) path queries over DL knowledge bases have been established [10, 11, 2] the most popular classes of queries currently considered are two- way regular path queries (2RPQs) and (unions of) conjunctive two-way regular path queries ((U)C2RPQs). The most expressive DL fragment with inverses, counting, and nominals combined where a UC2RPQs answering is known to be decidable is again Horn-SROIQ [20]. Current research progresses to even more expressive query lan- guages most of which can be seen as fragments of Datalog [27, 7]. Finite Satisfiability As stated above, the finite model semantics, while very popular in the database domain, has historically received little attention from DL researchers. This may be partially due to the fact, that many of the less expressive DLs (all sublogics of SROI) have the finite model property, where the two satisfiability notions (for finite vs. arbitrary models) coincide. This property, however is lost as soon as inverses and counting are involved. First investigations into finite satisfiability of such DLs go back to the last millenium [9] but spawned only little follow-up work [18, 14]. It was only in 2008 when finite satisfiability for SROIQ (and all its sublogics) was shown to be decidable [15], exploiting a result on the finite satisfiability for the counting two- variable fragment of first-order logic [22]. Finite Query Entailment Query entailment under the finite model semantics (short: finite query entailment) has so far received very little attention from the DL commu- nity. Note that the finite model property does not help here. The equivalent notion, holding when query entailment and finite query entailment coincide, is called finite controllability. Luckily, very recent results on the guarded fragment of first order logic [1] which extend previous work on finite controllability in databases under the open- world assumption [23] entail that for ALCHOIb (and all its sublogics), answering CQs and UCQs is finitely controllable, therefore for all those logics, decidability of finite (U)CQ entailment follows from decidability of (U)CQ entailment of the more ex- pressive ALCHOIQb [26]. For the case where the underlying logic has counting, or role chains can be described in the knowledge base or the query, results on finite query entailment are very scarce, the only DL not subsumed by ALCHOIb for which finite UCQ entailment is known to be decidable is Horn-ALCF I [14]. 1 The computation problem of query answering is polynomially reducible to the decision prob- lem of (Boolean) query entailment, so we focus on the latter in the following. The contribution of this paper consists in a sequence of undecidability results re- garding database-inspired reasoning problems which are established by very similar constructions encoding the classical undecidable Post Correspondence Problem. In par- ticular, we prove undecidability of (1) finite UCQ entailment from SHOIF KBs, (2) finite CQ entailment from SROIF − KBs (3) finite 2RPQ entailment from ALCOIF KBs (4) 2RPQ entailment from ALCOIF reg KBs, (5) satisfiability of ALCOIF ωreg KBs, and (6) 2ωRPQ entailment from ALCOIF KBs. The last two reasoning problems feature two-way ω-regular path expressions (in the logic vs. in the query language) used to describe infinite paths. We will draw connec- tions from this novel descriptive feature to existing logics. Preliminaries Finite Model Reasoning Beyond the standard semantics for DLs, this paper also ad- dresses reasoning under the finite-model semantics, a prominent (or even the standard) setting in database theory. Definition 1 (Finite Model Semantics). A knowledge base K is said to be finitely satisfiable if it has a finite model, i.e., there exists an interpretation I = (∆I , ·I ) with I |= K and ∆I finite. Likewise we say K finitely entails a conjunctive query q (or a union of conjunctive queries Q) and write K |=fin q (K |=fin Q), if I |= q (I |= Q) holds for every interpretation I = (∆I , ·I ) with I |= K and finite ∆I . It is obvious that finite satisfiability implies satisfiability, while the other direction holds only if the underlying logic has the finite model property. Likewise, entailment implies finite entailment but not vice versa. Example 1. Consider the knowledge base K1 consisting of the axioms Fun(r− ), > v ∃r.>, and {a} v ¬∃r− .>. We find that K1 is satisfiable (witnessed by the interpretation (N, {a 7→ 0, r 7→ succ}) ) but not finitely satisfiable (since the sum of r-indegrees and the sum of r-outdegrees cannot match in a finite model). In a similar way, the SHOIF knowledge base K2 containing the axioms Fun(r− ), > v ∃r.>, r v r0 , and Trans(r0 ) does not entail the CQ {r0 (x, x)} (witnessed by the interpretation (N, {r 7→ succ, r0 7→ <}) ), but K2 |=fin {r0 (x, x)}. The Post Correspondence Problem We will establish our undecidability result by a reduction from the well-known Post Correspondence Problem [21] defined as follows: Definition 2 (Post Correspondence Problem). Let P = {(g1 , g10 ), . . . , (gµ , gµ0 )} be an arbitrary finite set of pairs of non-empty strings over the alphabet {a, b}. A nonempty finite sequence i1 , . . . , in of natural numbers from {1, . . . , µ} is called a solution se- quence of P if gi1 · · · gin = gi01 · · · gi0n . The Post Correspondence Problem (short: PCP) requires to determine if there exists a solution sequence for a given P. Example 2. Let P = {(g1 , g10 ), (g2 , g20 ), (g3 , g30 )} where g1 = b, g10 = bbb, g2 = ab, g20 = a, g3 = bbba, and g30 = a. Then 2, 1, 1, 3 is a solution sequence due to the fact that g2 g1 g1 g3 = (ab)(b)(b)(bbba) = abbbbbba = (a)(bbb)(bbb)(a) = g20 g10 g10 g30 . Therefore the answer to the PCP instance P is “yes”. Theorem 1 (Post, 1946). The Post Correspondence Problem is undecidable. corr corr corr corr corr start next next next next next next next next end  a ab abb abbb abbbb abbbbb abbbbbb abbbbbba La Lb Lb Lb Lb Lb Lb La New , New 2 New , New 1 New , New 1 New , New 3 New New 0 , New 02 New 0 , New 01 New 0 , New 01 New 0 , New 03 New 0 Fig. 1. Solution model for the PCP instance and solution sequence described in Example 2. Undecidability of finite UCQ Entailment in SHOIF We are now ready to establish our first undecidability result. To this end, we will for a given instance of the PCP construct a SHOIF knowledge base and a union of conjunc- tive queries such that every model of the knowledge base not satisfying the UCQ (also called a counter-model) encodes a solution to the problem instance, and, conversely, every solution to the problem instance gives rise to such a counter-model. Solution Models We first formally define in which way the counter-models are supposed to encode solu- tions to the provided PCP instance. Definition 3 (Solution Model). Given a PCP instance P = {(g1 , g10 ), . . . , (gµ , gµ0 )}, an interpretation I = (∆I , ·I ) is called a solution model for P if there is a solution sequence i1 , . . . , in of P such that for w = gi1 · · · gin = gi01 · · · gi0n , the following hold: – ∆I = Prefixes(w) = {v | w = vv 0 , v 0 ∈ {a, b}∗ } – startI =  and endI = w – LIa = {v | va ∈ ∆I } and LIb = {v | vb ∈ ∆I } – New I = {} ∪ {gi1 · · · gi` | 1≤`≤n} and New 0I = {} ∪ {gi01 · · · gi0` | 1≤`≤n} – New Ik = {gi1· · · gi`−1 | i` =k, 1≤`≤n} and New 0I 0 0 k = {gi1· · · gi`−1 | i` =k, 1≤`≤n} – next I = {(v, vc) | c ∈ {a, b}, v, vc ∈ ∆I } – corrI = {(, )} ∪ {(gi1 · · · gi` , gi01 · · · gi0` ) | 1 ≤ ` ≤ n} Thereby, start and end are two individual names, La , Lb , New , New 0 , New 1 , New 01 , . . . New µ , New 0µ , are concept names and next and corr are role names. Figure 1 displays a solution model for the PCP instance P and solution sequence presented in Example 2. Axiomatization of Solution Models The purpose of the subsequently defined knowledge base KP is to enforce that all its finite models that do not satisfy a certain UCQ must be isomorphic to some solution model of P. We now introduce the axioms bit by bit and explain their purpose. First, we stipulate that the starting and the ending element do not coincide (and thereby the word encoded by the solution model is nonempty). {start} u {end} v ⊥ (1) Next, we enforce that every but the ending element has an outgoing next role, and that every but the starting element has an incoming such role. ¬{end} ≡ ∃next.> (2) ¬{start} ≡ ∃next − .> (3) Also, we make sure that there is no more than one outgoing and no more than one incoming next role for every element. Fun(next) (4) Fun(next − ) (5) I Now we ensure that every domain element except end is labeled with exactly one of La or Lb . ¬{end} ≡ La t Lb (6) La u Lb v ⊥ (7) Next, we describe “marker concepts” for the elements at the boundaries of the con- catenated words (two versions for the two different concatenations). Also, we make sure that at each such boundary that is not the ending element, a choice is made regarding which of the µ possible words comes next, and we implement this choice. Thereby, for a word g = c1 · · · c` we let Ig := Lc1 u∃next.(¬New uLc2 u∃next.(¬New u. . . Lc` u ∃next.New . . .)) and Ig0 := Lc1 u ∃next.(¬New 0 u Lc2 u ∃next.(¬New 0 u . . . Lc` u ∃next.New 0 . . .)). {start} v New u New 0 (8) New u ¬{end} ≡ New 1 t . . . t New µ (9) New i u New j v ⊥ (10) 0 New u ¬{end} ≡ New 01 t . . . t New 0µ (11) New 0i u New 0j v ⊥ (12) New k v Igk (13) New 0k v Ig0 k (14) We now turn to the corr role which is supposed to help synchronizing the two con- catenation schemes. To this end, corr is supposed to connect corresponding word bound- aries of one scheme with those of the other. We let corr connect exactly the New ele- ments with New 0 elements and make sure that this connection is a bijection. New ≡ ∃corr.> (15) New 0 ≡ ∃corr− .> (16) Fun(corr) (17) Fun(corr− ) (18) Also, we require that at corresponding word boundaries of the two schemes, the cor- responding words are to be chosen. New k v ∃corr.New 0k (19) New 0k v ∃corr− .New k (20) Last, we use a role inclusion and a transitivity axiom to introduce and describe an auxiliary role: the word role spans over chains of consecutive next roles. next v word (21) Trans(word) (22) Lastly but importantly, we define conjunctive queries which are supposed to detect “errors” in a model of the knowledge base defined so far. The CQ q1 = {word(x, x)} is supposed to detect looping next-chains (which must not exist in a solution model) and corr corr corr corr corr π(x2 ) π(x4 ) π(x3 ) π(x1 ) next next next next next next next next start end  a ab abb abba abbab abbabb abbabbb abbabbba La Lb Lb La Lb Lb Lb La New , New 1 New , New 2 New , New 3 New , New 4 New New 0 , New 01 New 0 , New 03 New 0 , New 02 New 0 , New 04 New 0 Fig. 2. Model for the knowledge base KP0 derived from the PCP instance P0 described in Exam- ple 3. For better readability, the word role has not been drawn, it is defined to hold between any two individuals connected by a directed chain of next roles. Note that this model is not a solution model. The provided evaluation π witnesses that the query q2 = {corr(x1 , x2 ), word(x2 , x3 ), corr(x4 , x3 ), word(x4 , x1 )} is satisfied in that model. the CQ q2 = {corr(x1 , x2 ), word(x2 , x3 ), corr(x4 , x3 ), word(x4 , x1 )} intuitively en- codes the phenomenon of two “crossing” corr relationships, which also are not allowed to occur in a solution model. Correctness of the Reduction After presenting the knowledge base and the queries, we will now formally prove the correspondence between the PCS and non-entailment. Thereby, the introduced notion of solution models will come in handy. Lemma 1. Let P be a PCP instance, and let I be a corresponding solution model. Then I can be extended into a model I 0 of KP such that I 0 6|= {q1 , q2 }. Lemma 2. Let P be a PCP. Then every finite model I of KP with I 6|= {q1 , q2 } is isomorphic to a solution model of P. To illustrate the idea behind the construction, we will provide an example with an “out of sync” pseudo-solution and show how the query q2 catches this problem. Example 3. Consider P0 = {(g1 , g10 ), (g2 , g20 ), (g3 , g30 ), (g4 , g40 )} with g1 = abb, g10 = ab, g2 = ab, g20 = bbb, g3 = b, g30 = ba, g4 = ba, and g40 = a. Then, the interpretation depicted in Fig. 2 is a model of KP0 but not a solution model, as witnessed by q2 being satisfied. The two lemmas together now give rise to the following theorem linking the PCP with finite UCQ entailment in SHOIF. Theorem 2. Let P be a PCP instance and let KP be the SHOIF knowledge base con- sisting of Axioms 1–22. Then the answer to P is “yes” if and only if KP 6|=fin {q1 , q2 }. Corollary 1. Finite entailment of unions of conjunctive queries from SHOIF knowl- edge bases is undecidable.2 2 Briefly before submitting the camera ready version of this paper, the author was made aware by Carsten Lutz that this corollary can indeed be strengthened to plain conjunctive queries by a refinement of the construction used in the proof. For didactic and space reasons, we decided against including the not too difficult, yet somewhat unwieldy argument. Related Undecidability Results The construction used to establish the above undecidability result can be modified to show undecidability of other reasoning problems where nominals, counting, inverses and path expressions are involved. In the following we will introduce the logics and queries considered and describe how the reasoning problem needs to be adapted Finite CQ Entailment in SROIF − The description logic SROIF − is obtained from SHOIF by allowing so called com- plex role inclusion axioms3 of the form r1 ◦ . . . ◦ rn v r for r1 , . . . , rn , r ∈ R. We now show how the added expressive power of complex role inclusions can be used to incorporate the error detection previously carried out by two CQs into just one CQ. The basic idea is that both CQs are supposed to detect cycles of a certain kind. So we can define a new role badcycle that spans role chains which, if we identified their first and their last elements would lead to q1 or q2 being satisfied. word v badcycle (23) corr ◦ word ◦ corr− ◦ word v badcycle (24) Note that these axioms are in accordance with the simplicity and regularity constraints commonly imposed on DLs with role chain axioms. Obviously, in order to ensure that an interpretation matches neither q1 nor q2 , we just have to forbid badcycle-loops, i.e., we must require that the one-atom CQ {badcycle(x, x)} is not satisfied. Theorem 3. Let P be a PCP instance and let KP0 be the SROIF − KB consisting of Axioms 1–24. Then the answer to P is “yes” if and only if KP0 6|=fin {badcycle(x, x)}. Corollary 2. Finite conjunctive query entailment from SROIF − knowledge bases is undecidable. Finite 2RPQ Entailment from ALCOIF KBs We next show undecidability of a problem involving two-way regular path queries (2RPQs). We assume the reader to be familiar with these queries as well as the under- lying notion of two-way regular path expressions (2RPEs). Recall that an ALCOIF knowledge base is a SHOIF knowledge base that does not have role inclusions nor transitivity axioms. It has been established that the problem of CQ entailment from SROIQ KBs can be reduced to the problem of conjunctive 2RPQ entailment from ALCHOIQ KBs using automata-theoretic methods for modifying the knowledge base and rewriting the query [15, 13, 20]. As this technique is modular with respect to most used modeling features and preserves (cardinality of) models, it can be used to transform the problem of (finite) entailment of one-atom-CQ from SROIF − KBs to the problem of (finite) 2RPQ entailment from ALCOIF KBs. In particular, this reduction can be used to establish the following result. 3 We denote this description logic by SROIF − , since according to the common nomenclature, SROIF would contain more modeling features such as self-loops, the universal role, and role disjointness. Theorem 4. Let P be a PCP instance and let KP00 be the ALCOIF knowledge base consisting of Axioms 1–20. Then the answer to P is “yes” if and only if KP00 6|=fin (next)+ ∪ corr·(next)+ ·corr− ·(next)+ (x, x). Note that, instead of employing the transformation sketched above, this theorem can also be directly proven very much along the lines of the previous proof with only very minor modifications. Corollary 3. Finite entailment of two-way regular path queries from ALCOIF knowl- edge bases is undecidable. 2RPQ Entailment from ALCOIF reg KBs The description logic ALCOIF reg is obtained from ALCOIF by allowing concept expressions of the form ∃exp.C where exp is a 2RPE and C is a concept expression. The semantics of such concept expressions is defined in the straightforward way, based on semantics of 2RPEs introduced above. Note that progressing from ALCOIF to ALCOIF reg is quite a significant exten- sion. Most notably, unlike most mainstream description logics, ALCOIF reg is not a fragment of first-order logic, as it for instance allows for expressing reachability. In our case, we can use the new type of expressions to axiomatically enforce that each model must be a finite chain of nexts leading from startI to endI without “externally” imposing the finite model assumption. We simply state that every domain element starts a path of nexts ending in endI and a path of next − s ending in startI . > v ∃next ∗ .{end} (25) > v ∃(next − )∗ .{start} (26) With this additional axioms at hand, we can now easily establish the next theorem. Theorem 5. Let P be a PCP instance and let KP000 be the ALCOIF reg knowledge base consisting of Axioms 1–20 and Axioms 25 and 26. Then the answer to P is “yes” if and only if KP00 6|= corr·(next)+ ·corr− ·(next)+ (x, x). Note that here, the query does not need to detect looping next chains since their existence is already prevented by Axioms 25 and 26 together with Axioms 1–5. Corollary 4. Entailment of two-way regular path queries from ALCOIF reg knowl- edge bases is undecidable. It might be worth noting that dropping one of the three constructs of inverses, func- tionality or nominals from the logic makes the problem decidable again, even if further modeling features are added and positive 2RPQs (i.e., arbitrary Boolean combinations of 2RPQs) are considered [11]. Note that the above finding can be turned into a slight generalization of an already known result: Let ALCOIF ∗ be the restriction of the description logic ALCOIF reg where all regular expressions are of the form r∗ for r ∈ R. A transitive closure- enhanced conjunctive query (TC-CQ) is a conjunctive query allowing for atoms of the form r∗ (t1 , t2 ) for r ∈ R. Satisfaction and entailment of such queries are defined in the straightforward way. It was shown that entailment of unions of TC-CQs from ALCOIF ∗ knowledge bases is undecidable [19]. By using the above construction and noting that the 2RPQ corr·(next)+ ·corr− ·(next)+ (x, x) is (with respect to entailment) equivalent to the TC-CQ {corr(x1 , x2 ), next(x2 , x3 ), next∗ (x3 , x4 ), corr(x5 , x4 ), next(x5 , x6 ), next∗ (x6 , x1 )}, we can establish the following corollary slightly strength- ening the previous result. Corollary 5. Entailment of TC-CQs from ALCOIF ∗ knowledge bases is undecidable. Satisfiability of ALCOIF ωreg KBs The DL ALCOIF reg introduced in the previous section featured the possibility to describe unbounded, yet finite chains of roles. Opposed to this, it might also be desirable to describe infinite chains of roles. In fact, this is a feature not uncommon in temporal variants of modal logics and can, e.g., be used to express liveness properties. While regular expressions are used to characterize finite role chains, the appropriate notion for infinite role chains would be ω-regular expressions. Definition 4 (ω-Regular Expressions, 2ωRPQs). For an alphabet A, the set OEX of ω-regular expressions over A is OEX ::= NEX ω | OEX ∪ OEX | EX · OEX , where NEX are the regular expressions not matching the empty word, and EX are all regular expressions. We associate with each ω-regular expression exp over A a set of infinite words over A, denoted by [exp], in the straightforward way (where expω denotes indefinite repetition of words matching exp). If for an ω-regular expression exp, an infinite word v satisfies v ∈ [exp], we also say v matches exp. Given a set R of roles (i.e., role names and their inverses), a two-way ω-regular path expression (2ωRPE) is a ω-regular expression over the alphabet R. We now let ALCOIF ωreg denote the description logic ALCOIF extended by con- cept expressions of the form ∃exp.∞ with exp an 2ωRPE. The semantics of these expressions, which we call ω-concepts, is defined as follows: (∃exp.∞)I consists of those δ ∈ ∆I for which there exist an infinite word r1 r2 · · · over role names and their inverses matching exp and an infinite sequence δ0 , δ1 , . . . of elements from ∆I such that δ = δ0 and (δi , δi+1 ) ∈ riI holds for every i ∈ N. Intuitively, we will use the new expressivity provided by ω-concepts to prevent the existence of infinite paths of certain shapes. In particular, we prevent infinite next- paths as well as paths of infinitely repeated corr · nextn · corr− · nextm -sequences. ∃nextω .∞ v ⊥ (27) ∃(corr · next + · corr− · next + )ω .∞ v ⊥ (28) Theorem 6. Let P be a PCP instance and let KP0000 be the ALCOIF reg knowledge base consisting of Axioms 1–20 and Axioms 27 and 28. Then the answer to P is “yes” if and only if KP0000 is satisfiable. Corollary 6. Satisfiability of ALCOIF ωreg knowledge bases is undecidable. The DL ALCOIF ωreg might seem a bit contrived at the first glance. It should how- ever be noted that it constitutes a fragment of the so-called fully enriched µ-calculus and its DL version µALCIOf [4, 6, 5]. We will not go into details here, we just note that in particular, ∃nextω .∞ can be expressed in µALCIOf as νX.∃next.X and ∃(corr · next + · corr− · next + )ω .∞ can beexpressed by νX.∃corr.∃next.µY. (∃next.Y ) t ∃.corr− .∃next.µZ.(∃next.Z) t X . These concept expressions correspond to the so- called aconjunctive fragment of the µ-calculus [16] which, roughly speaking, only al- lows one to describe situations which are essentially linear. We let µALCIOacon f denote µALCIOf where fixpoint expressions are in aconjunctive form. Then the following corollary improves on a previous undecidability result for µALCIOf [4] (the proof of which hinges upon the use of non-aconjunctive fixpoint expressions). Corollary 7. Satisfiability of µALCIOacon f knowledge bases is undecidable. Again it is noteworthy that removing any of the three modeling features inverses, functionality, or nominals (in µ-calculus terminology: the features of being full, graded, or hybrid), makes the problem decidable again [5]. ω2RPQ Entailment from ALCOIF KBs The last reasoning problem considered here is very close to the previous one, the dif- ference being that we allow ω-regular expressions in the query language rather than in the logic itself. Definition 5 (Two-way ω-Regular Path Queries). A two-way ω-regular path query (2ωRPQ) is an atom of the shape exp(t) where exp is a 2ωRPE and t is a term. For an interpretation I and an evaluation π, we define that I |=π exp(t) holds iff there exist an infinite word r1 r2 · · · over role names and their inverses matching exp and an infinite sequence δ0 , δ1 , . . . of elements from ∆I such that π(t) = δ0 and for every i ∈ N holds (δi , δi+1 ) ∈ riI . Entailment of 2ωRPQs from knowledge bases is defined in the straightforward way. Note that the query atom must be of arity one, since an infinite chain of roles has only a defined starting but no ending point. As it turns out, the previous undecidability result concerning satisfiability of ALCOIF ωreg KBs can be directly transformed into one re- garding ω2RPQ entailment from ALCOIF KBs, since in the former, ω-concepts were only used to detect and exclude problematic situations. This allows us to effortlessly rephrase the construction into a query entailment problem. Theorem 7. Let P be a PCP instance and, as before, let KP00 be the ALCOIF knowl- edge base consisting of Axioms 1–20. Then the answer to P is “yes” if and only if KP00 6|= nextω ∪ (corr · next + · corr− · next + )ω (x). Corollary 8. Entailment of two-way ω-regular path queries from ALCOIF knowl- edge bases is undecidable. Conclusion and Future Work We have established undecidability for database-inspired reasoning problems regard- ing very expressive description logics that allow for inverses, counting and nominals coupled with expressive means for describing role chains of unbounded or even infinite length. Focusing on query answering and the finite model semantics, we showed that for several reasoning problems from that realm, a reduction of the Post Correspondence Problem can be achieved through slight modifications of one generic construction. These findings clarify the decidability status of interesting reasoning problems, many of which are complemented by decidability results for sublogics with just one model- ing feature removed. Still, there are numerous related reasoning problems whose de- cidability status remains open. In particular, decidability is unknown for the following problems (with some dependencies between them as stated below): P1 (U)CQ entailment from SHOIF KBs. A version of a very prominent long- standing open problem. For UCQs, the finite-model version has been settled (negatively) in this paper, but there is little hope that this will provide insights toward a solution of the unrestricted model case. P2 Finite CQ entailment from SHOIF KBs. P3 (U)CQ entailment from SROIF KBs. Decidability of this problem would entail decidability of P1 and essentially boil down to decidability of conjunctive query answering in OWL 2 DL. P4 2RPQ entailment from ALCOIF KBs. Note that the case is open only for “looping” 2RPQs, where the two terms in the atom are the same variable. For all other 2RPQs, the problem is decidable by a reduction to (un)satisfiability of ALCOIF. The finite entailment case was settled (negatively) in this paper. P5 (Unions of) Conjunctive 2RPQ entailment from ALCOIF KBs. This problem is equivalent to P3 and its decidability would entail decidability of P4 and P1. P6 Finite satisfiability of ALCOIF reg KBs P7 Satisfiability of ALCOIF reg KBs. Decidability of this problem entails decid- ability of P6, since model-finiteness can be axiomatized in ALCOIF reg . P8 Finite CQ entailment from ALCOIF reg KBs. Clearly, decidability of this problem entails decidability of P6. P9 CQ entailment from ALCOIF reg KBs. For the aforementioned reasons, de- cidability of this problem would entail decidability of all P8, P7, and P6. It should be noted that for many of the problems, removing one of the features in- verses, nominals, or functionality would make the problem decidable. This is the case for P1, P3, P4, P5, P7, and P9 as can be inferred from decidability of positive two-way relational path query (P2RPQ) entailment from the extremely expressive DLs ZIQ, ZOQ, and ZOI knowledge bases [11]. On another note, the same subset of the prob- lems are known to be decidable when just the Horn fragment of the underlying de- scription logic is considered, following from the decidability of entailment of unions of conjunctive 2RPQs from Horn-SROIQ KBs [20].4 4 Regarding P7 and P9, to be fair, one should state that going to the Horn fragment essentially disables the interesting uses of regular expressions, i.e., Horn-ALCOIF reg is not more ex- pressive than Horn-ALCOIF. References 1. Vince Bárány, Georg Gottlob, and Martin Otto. Querying the guarded fragment. Logical Methods in Computer Science, 10(2), 2014. 2. Meghyn Bienvenu, Diego Calvanese, Magdalena Ortiz, and Mantas Simkus. Nested regular path queries in description logics. In Chitta Baral, Giuseppe De Giacomo, and Thomas Eiter, editors, Proc. 14th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR’14). AAAI Press, 2014. 3. Stefan Bischoff, Markus Krötzsch, Axel Polleres, and Sebastian Rudolph. Schema-agnostic query rewriting for SPARQL 1.1. In Peter Mika, Tania Tudorache, Abraham Bernstein, Chris Welty, Craig A. Knoblock, Denny Vrandečić, Paul T. Groth, Natasha F. Noy, Krzysztof Janowicz, and Carole A. Goble, editors, Proc. 13th Int. Semantic Web Conf. (ISWC’14), volume 8796 of LNCS, pages 584–600. Springer, 2014. 4. Piero A. Bonatti. On the undecidability of description and dynamic logics with recursion and counting. In Georg Gottlob and Toby Walsh, editors, Proc. 18th Int. Joint Conf. on Artificial Intelligence (IJCAI’03), pages 331–336. Morgan Kaufmann, 2003. 5. Piero A. Bonatti, Carsten Lutz, Aniello Murano, and Moshe Y. Vardi. The complexity of enriched mu-calculi. Logical Methods in Computer Science, 4(3), 2008. 6. Piero A. Bonatti and Adriano Peron. On the undecidability of logics with converse, nominals, recursion and counting. Artificial Intelligence, 158(1):75–96, 2004. 7. Pierre Bourhis, Markus Krötzsch, and Sebastian Rudolph. How to best nest regular path queries. In Meghyn Bienvenu, Magdalena Ortiz, Riccardo Rosati, and Mantas Simkus, ed- itors, Informal Proc. 27th Int. Workshop on Description Logics (DL’04), volume 1193 of CEUR Workshop Proceedings, pages 404–415. CEUR-WS.org, 2014. 8. Peter Buneman. Semistructured data. In Alberto O. Mendelzon and Z. Meral Özsoyoglu, editors, Proc. 16th Symposium on Principles of Database Systems (PODS’97), pages 117– 121. ACM Press, 1997. 9. Diego Calvanese. Finite model reasoning in description logics. In Luigia Carlucci Aiello, Jon Doyle, and Stuart C. Shapiro, editors, Proc. 5th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR’96), pages 292–303. Morgan Kaufmann, 1996. 10. Diego Calvanese, Thomas Eiter, and Magdalena Ortiz. Answering regular path queries in expressive description logics: An automata-theoretic approach. In Proc. 22nd AAAI Conf. on Artificial Intelligence (AAAI’07), pages 391–396. AAAI Press, 2007. 11. Diego Calvanese, Thomas Eiter, and Magdalena Ortiz. Regular path queries in expressive description logics with nominals. In Craig Boutilier, editor, Proc. 21st Int. Joint Conf. on Artificial Intelligence (IJCAI’09), pages 714–720. IJCAI, 2009. 12. Ashok K. Chandra and Philip M. Merlin. Optimal implementation of conjunctive queries in relational data bases. pages 77–90, 1977. 13. Stéphane Demri and Hans Nivelle. Deciding regular grammar logics with converse through first-order logic. J. of Logic, Language and Information, 14(3):289–329, 2005. 14. Yazmin Angélica Ibáñez-Garcı́a, Carsten Lutz, and Thomas Schneider. Finite model reason- ing in Horn description logics. In Chitta Baral, Giuseppe De Giacomo, and Thomas Eiter, editors, Proc. 14th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR’14). AAAI Press, 2014. 15. Yevgeny Kazakov. RIQ and SROIQ are harder than SHOIQ. In Gerhard Brewka and Jérôme Lang, editors, Proc. 11th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR’08), pages 274–284. AAAI Press, 2008. 16. Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354, 1983. 17. Alon Y. Levy and Marie-Christine Rousset. CARIN: A representation language combining Horn rules and description logics. In Wolfgang Wahlster, editor, Proc. 12th European Conf. on Artificial Intelligence (ECAI’96), pages 323–327. John Wiley and Sons, 1996. 18. Carsten Lutz, Ulrike Sattler, and Lidia Tendera. The complexity of finite model reasoning in description logics. Information and Computation, 199(1-2):132–171, 2005. 19. Magdalena Ortiz, Sebastian Rudolph, and Mantas Simkus. Query answering is undecidable in DLs with regular expressions, inverses, nominals, and counting. INFSYS Research Report 1843-10-03, TU Vienna, 2010. 20. Magdalena Ortiz, Sebastian Rudolph, and Mantas Simkus. Query answering in the Horn fragments of the description logics SHOIQ and SROIQ. In Toby Walsh, editor, Proc. 22nd Int. Joint Conf. on Artificial Intelligence (IJCAI’11), pages 1039–1044. IJCAI/AAAI, 2011. 21. Emil L. Post. A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society, 52, 1946. 22. Ian Pratt-Hartmann. Complexity of the two-variable fragment with counting quantifiers. J. of Logic, Language and Information, 14:369–395, 2005. 23. Riccardo Rosati. On the finite controllability of conjunctive query answering in databases under open-world assumption. J. of Computer and System Sciences, 77(3):572–594, 2011. 24. Sebastian Rudolph. The two views on ontological query answering. In Georg Gottlob and Jorge Pérez, editors, Proc. 8th Alberto Mendelzon Workshop on Foundations of Data Man- agement (AMW’14), volume 1189 of CEUR Workshop Proceedings. CEUR-WS.org, 2014. 25. Sebastian Rudolph. Undecidability results for database-inspired reasoning problems in very expressive description logics. In Proc. 15th Int. Conf. on Principles of Knowledge Represen- tation and Reasoning (KR’15). AAAI Press, 2016. to appear. 26. Sebastian Rudolph and Birte Glimm. Nominals, inverses, counting, and conjunctive queries or: Why infinity is your friend! J. of Artificial Intelligence Research, 39:429–481, 2010. 27. Sebastian Rudolph and Markus Krötzsch. Flag & check: Data access with monadically defined queries. In Richard Hull and Wenfei Fan, editors, Proc. 32nd Symp. on Principles of Database Systems (PODS’13), pages 151–162. ACM, 2013.