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 traditional 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 conjunctive queries for a fragment of SHOIQ (the logic underlying the OWL DL ontology 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).
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 [
Two major conceptual contributions of database theory can be identified: query answering 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
answering) 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 [
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
fragment of SQL [
In the context of semi-structured databases, other query formalisms have been
developed which allow for expressing information needs related to reachability, so-called
path queries or navigational queries [
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 [
Finite Query Entailment Query entailment under the finite model semantics (short:
finite query entailment) has so far received very little attention from the DL
community. 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
[
The contribution of this paper consists in a sequence of undecidability results regarding database-inspired reasoning problems which are established by very similar constructions encoding the classical undecidable Post Correspondence Problem. In particular, 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 connections from this novel descriptive feature to existing logics.
Finite Model Reasoning Beyond the standard semantics for DLs, this paper also addresses reasoning under the finite-model semantics, a prominent (or even the standard) setting in database theory.
satisfiable if it has a finite model, i.e., there exists an interpretation I = ( I ; I ) with I j= K and I finite. Likewise we say K finitely entails a conjunctive query q (or a union of conjunctive queries Q) and write K j= n q (K j= n Q), if I j= q (I j= Q) holds for every interpretation I = ( I ; I ) with I j= 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 9r:>, and fag v :9r :>. We find that K1 is satisfiable (witnessed by the interpretation (N; fa 7! 0; r 7! succg) ) 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 9r:>, r v r0, and Trans(r0) does not entail the CQ fr0(x; x)g (witnessed by the interpretation (N; fr 7! succ; r0 7! <g) ), but K2 j= n fr0(x; x)g.
The Post Correspondence Problem We will establish our undecidability result by a
reduction from the well-known Post Correspondence Problem [
Theorem 1 (Post, 1946). The Post Correspondence Problem is undecidable.
corr start next next
next a
Lb La New; New2 New0; New02 New0; New01 ab abb abbb Lb Lb Lb New; New1 New; New1 New; New3
New0; New01 abbbb Lb corr next
next abbbbb Lb
next abbbbbb La
New New0; New03 New0 corr
end abbbbbba Undecidability of finite UCQ Entailment in SHOI F 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 conjunctive 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.
We first formally define in which way the counter-models are supposed to encode solutions to the provided PCP instance.
Definition 3 (Solution Model). Given a PCP instance P = f(g1; g10); : : : ; (g ; g0 )g, 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 = Pre xes(w) = fv j w = vv0; v0 2 fa; bg g – startI = and endI = w – LaI = fv j va 2 I g and LbI = fv j vb 2 I g – New I = f g [ fgi1 gi` j 1 ` ng and New 0I = f g [ fgi01 gi0` j 1 ` ng – New kI = fgi1 gi` 1 j i`=k; 1 ` ng and New 0kI = fgi01 gi0` 1 j i`=k; 1 ` ng – next I = f(v; vc) j c 2 fa; bg; v; vc 2 I g – corrI = f( ; )g [ f(gi1 gi` ; gi01 gi0` ) j 1 ` ng
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.
fstartg u fendg v ?
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.
Also, we make sure that there is no more than one outgoing and no more than one incoming next role for every element.
Now we ensure that every domain element except endI is labeled with exactly one of La or Lb.
Next, we describe “marker concepts” for the elements at the boundaries of the concatenated 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 u9next :(:New uLc2 u9next:(:New u: : : Lc` u 9next:New : : :)) and Ig0 := Lc1 u 9next :(:New 0 u Lc2 u 9next:(:New 0 u : : : Lc` u 9next:New 0 : : :)).
fstartg v New u New 0 New u :fendg New 0 u :fendg
New 1 t : : : t New
New 01 t : : : t New 0 (11) New k v Igk (2) (4) (6) (15) (17) (19) (21) (3) (5) (7) (16) (18) (20) (22) (9) (13)
New i u New j v ? New 0i u New 0j v ?
New 0k v Ig0k (8) (10) (12) (14)
We now turn to the corr role which is supposed to help synchronizing the two concatenation schemes. To this end, corr is supposed to connect corresponding word boundaries of one scheme with those of the other. We let corr connect exactly the New elements with New 0 elements and make sure that this connection is a bijection.
Also, we require that at corresponding word boundaries of the two schemes, the corresponding words are to be chosen.
New
9corr:> Fun(corr)
New 0
9corr :> Fun(corr ) New k v 9corr:New 0k New 0k v 9corr :New k
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 Trans(word)
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 = fword(x; x)g is supposed to detect looping next-chains (which must not exist in a solution model) and corr corr start
next La New; New1 New0; New01 a Lb next (x2) next (x4) ncoerxrt (x3) next (x1) next the CQ q2 = fcorr(x1; x2); word(x2; x3); corr(x4; x3); word(x4; x1)g intuitively encodes the phenomenon of two “crossing” corr relationships, which also are not allowed to occur in a solution model.
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 I0 of KP such that I0 6j= fq1; q2g.
Lemma 2. Let P be a PCP. Then every finite model I of KP with I 6j= fq1; q2g 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 = f(g1; g10); (g2; g20); (g3; g30); (g4; g40)g 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 consisting of Axioms 1–22. Then the answer to P is “yes” if and only if KP 6j= n fq1; q2g. Corollary 1. Finite entailment of unions of conjunctive queries from SHOIF knowledge 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.
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
The description logic SROIF is obtained from SHOIF by allowing so called complex role inclusion axioms3 of the form r1 : : : rn v r for r1; : : : ; rn; r 2 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 fbadcycle(x; x)g 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 6j= n fbadcycle(x; x)g. Corollary 2. Finite conjunctive query entailment from SROIF undecidable. knowledge bases is
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 underlying 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 [
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 6j= n (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 knowledge bases is undecidable.
The description logic ALCOIF reg is obtained from ALCOIF by allowing concept expressions of the form 9exp: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 extension. 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 next s leading from startI to endI without “externally” imposing the finite model assumption. We simply state that every domain element starts a path of next s ending in endI and a path of next s ending in startI . > v 9next :fendg (25) > v 9(next ) :fstartg (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 6j= 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 knowledge bases is undecidable.
It might be worth noting that dropping one of the three constructs of inverses,
functionality 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 [
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 2 R. A transitive
closureenhanced conjunctive query (TC-CQ) is a conjunctive query allowing for atoms of the
form r (t1; t2) for r 2 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 [
Corollary 5. Entailment of TC-CQs from ALCOIF knowledge bases is undecidable.
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 ! j OEX [ OEX j 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 2 [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 concept expressions of the form 9exp:1 with exp an 2!RPE. The semantics of these expressions, which we call !-concepts, is defined as follows: (9exp:1)I consists of those 2 I for which there exist an infinite word r1r2 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) 2 riI holds for every i 2 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 nextpaths as well as paths of infinitely repeated corr nextn corr nextm-sequences. 9next!:1 v ? (27) 9(corr next + corr next +)!:1 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
however be noted that it constitutes a fragment of the so-called fully enriched -calculus and
its DL version ALCIOf [
ALCIOf where fixpoint expressions are in aconjunctive form. Then the following
corollary improves on a previous undecidability result for ALCIOf [
Corollary 7. Satisfiability of
ALCIOfacon 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 [
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 j= exp(t) holds iff there exist an infinite word r1r2 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 2 N holds ( i; i+1) 2 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 regarding !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 knowledge base consisting of Axioms 1–20. Then the answer to P is “yes” if and only if KP00 6j= next! [ (corr next + corr next +)!(x).
Corollary 8. Entailment of two-way !-regular path queries from ALCOIF knowledge bases is undecidable.
We have established undecidability for database-inspired reasoning problems regarding 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 modeling feature removed. Still, there are numerous related reasoning problems whose decidability 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 longstanding 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 decidability 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, decidability 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
inverses, 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 [