Since the introduction of the SHACL standard, understanding its computational features and formal foundations has become essential. Some research has focused on the semantics of recursive constraints and the complexity of validation, but the satisfiability of SHACL constraints remains largely unexplored. The most significant previous work in this direction is rather coarse, obtaining very few positive results for finite satisfiability and for fragments with counting. In this paper, we build on description logics to paint a comprehensive and fine-grained boundary for SHACL fragments with a decidable satisfiability problem under the supported semantics, both for unrestricted and finite models.
Since the SHACL standard was introduced, the need for a solid understanding of its computational
features and formal foundations has been apparent. Several works have leveraged related logic formalisms
to give semantics to recursive constraints, obtain complexity bounds, and solve basic tasks including
validation [
Given the importance of the problem, there are remarkably few results concerning its decidability
and complexity. Indeed, the most notable work in this direction, [
In this paper, we revisit satisfiability under the supported model semantics. We build on Description Logics (DLs), a well-known family of languages for Knowledge Representation and Reasoning that ofers decades of research in the fine-grained study of logical fragments and the efect that the interaction between diferent shapes of subformulas has on the complexity of reasoning. The close relationship between DLs and SHACL is well-known, and in this paper, we leverage it to paint a much finer boundary of SHACL fragments that have decidable satisfiability problems, both over unrestricted graphs and over graphs with a finite domain.
Contributions. We build on the DL literature to pinpoint much tighter complexity bounds than previously known for SHACL, based on the close connection between DL - and SHACL satisfiability; we revisit this connection and explain how to translate complexity results in both ways. To emphasise this tight bond, we provide a DL inspired naming convention: we write ℒ to denote the SHACL fragment similar to the DL ℒ. Moreover, we add some lack of finite model property results to the landscape: we show this for ℒ plus counting over regular path expressions, which also provides an alternative undecidability proof; and, we show that adding either eq(, ) or disj(, ) to ℒ also breaks the ifnite model property of ℒ.
Related Literature. There are two other theoretical papers considering satisfiability of (recursive)
SHACL [
Data Graphs and Interpretations. Let , and denote countably infinite, mutually disjoint sets of concept names, role names, and individuals, respectively. Let + := {, − | ∈ } be the set of roles. For every ∈ , set (− )− = . An atom is an expression of the form () or (, ′), for ∈ , ∈ and {, ′} ⊆ . An ABox (or data graph) is a finite set of atoms.
An interpretation is a pair ℐ = (Δℐ , · ℐ ), where Δℐ is a non-empty set (called domain) and · ℐ is a function that maps every ∈ to a set ℐ ⊆ Δℐ , every ∈ to a binary relation ℐ ⊆ Δℐ × Δℐ , and every individual ∈ to an element ℐ ∈ Δℐ . Let (− )ℐ := {(′, ) | (, ′) ∈ ℐ }. We call an interpretation ℐ finite when Δℐ is finite. We make the standard name assumption, meaning ℐ = for all interpretations ℐ, and all ∈ . The canonical interpretation ℐ of a set of atoms is defined by setting Δℐ = { | () ∈ } ∪ {(, ′) | (, ′) ∈ }, ℐ = { | () ∈ } for all ∈ and ℐ = {(, ′) | (, ′) ∈ } for all ∈ .
Description Logic ℒℐ. An ℒℐ concept is defined in the following way: ::= | | ⊤ | ¬ | ⊓ | ⊔ |≥ . | ∀., where ∈ , ∈ , ≥ 1 and ∈ + . An ℒℐ TBox is a set of axioms of the form ⊑ , for and ℒℐ concepts. We use ≡ as a shorthand for ⊑ and ⊑ . An interpretation ℐ is a model of if for all ⊑ ∈ we have ℐ ⊆ ℐ , where ℐ is recursively defined as: (¬)ℐ := Δℐ ∖ ℐ , ( ⊓ ′)ℐ := ℐ ∩ ′ℐ , ( ⊔ ′)ℐ := ℐ ∪ ′ℐ , (≥ .)ℐ := { ∈ Δℐ | |{′ ∈ Δℐ | (, ′) ∈ ℐ , ′ ∈ ℐ }| ≥ } and (∀.)ℐ := { ∈ Δℐ | (, ′) ∈ ℐ → ′ ∈ ℐ }. A concept is satisfiable w.r.t. a TBox if there exists a model ℐ of such that ℐ ̸= ∅. Recursive Shape Constraint Language (SHACL). Let be a countably infinite set of shape names, disjoint from , and . We define shape expressions, following [13], but adding recursion, in the following way
::= | | | ⊤ | ¬ | ∧ | ≥ . | eq(, ) | disj(, ) | closed(), where ∈ , ∈ , ∈ , ≥ 1, a finite subset of + and a regular expression given by ::= | * | ∘ | ∪ , ⊤ℐ, = ℐ, = { ∈ Δℐ | () ∈ } ℐ, = {ℐ } (¬ )ℐ, = Δℐ ∖ ( )ℐ, ℐ, = ℐ ( ∧ ′)ℐ, = ( )ℐ, ∩ ( ′)ℐ, (≥ . )ℐ, = { ∈ Δℐ | |{′ ∈ Δℐ | (, ′) ∈ ℐ , ′ ∈ ℐ,}| ≥ } (eq(, ))ℐ, = { ∈ Δℐ | {′ ∈ Δℐ | (, ′) ∈ ℐ } = {′ ∈ Δℐ | (, ′) ∈ ℐ }} (disj(, ))ℐ, = { ∈ Δℐ | {′ ∈ Δℐ | (, ′) ∈ ℐ } ∩ {′ ∈ Δℐ | (, ′) ∈ ℐ } = ∅} (closed())ℐ, = { ∈ Δℐ | { ∈ + ∖ | (, ′) ∈ ℐ } = ∅} for ∈ + . Here, (* )ℐ corresponds to the transitive closure of ℐ , ( ∘ ′)ℐ := {(, ′) | (, ) ∈ ℐ , (, ′) ∈ ′ℐ }, and ( ∪ ′)ℐ := ℐ ∪ ′ℐ . We use ′ as a shorthand for ∘ ′, and + for * . We set ∨ ′ := ¬(¬ ∧ ¬ ′) and ∀. := ¬ ≥ 1 .¬ . A shape constraint is an expression of the form ← , for ∈ and a shape expression. With , we indicate a set of shape constraints. For each ← , let be the head of the constraint. In each , we assume each shape name only appears as the head of one constraint - this does not influence expressivity as ‘ ∨’ may be used.
A shape atom is an expression of the form (), for ∈ and ∈ . A shape assignment is a set of shape atoms. Given an interpretation ℐ and a shape assignment , we say a individual ∈ validates a shape expression , whenever ∈ ( )ℐ, , where ( )ℐ, is recursively defined in Table 1. Given some , we say validates ∈ , if validates for all ← ∈ . Let be a set of targets of the form (), which we call atomic targets, or (), for ∈ , ∈ and ∈ . A pair (, ) is called a shapes graph. In this paper, we consider the supported model semantics; given an interpretation ℐ, we say ℐ validates (, ) when there exists a shape assignment such that if ← ∈ , we find ℐ, = ( )ℐ, and for all () ∈ , we find validates , and for all () ∈ , all individuals in ℐ validate . Diferent semantics require diferent constraints for the shape assignments. For readability, we will write validates (, ), for a set of atoms to mean that the canonical interpretation ℐ validates (, ).
Satisfiability: Given a SHACL fragment ℒ , for each shapes graph (, ) expressible in ℒ , decide whether there exists an interpretation ℐ that validates (, ).
Finite Satisfiability: Given a SHACL fragment ℒ , for each shapes graph (, ) expressible in ℒ , decide whether there exists a finite interpretation ℐ that validates (, ).
We also study the following property, which guarantees that these problems coincide: Finite Model Property: A SHACL fragment ℒ has the finite model property if for every shapes graph (, ) expressible in ℒ , we find that if (, ) is satisfiable, then (, ) is finitely satisfiable.
Clearly, having the finite model property extends to less expressive fragments, whereas the opposite, not having the property, spreads to subsuming fragments. Similarly, for (finite) satisfiability, membership of a complexity class spreads to less expressive fragments, and hardness to the more expressive ones. In case a fragment has the finite model property, the membership results for general satisfiability extend to the finite setting.
The above presented problems are not the only ones one might consider: in [
Lemma 1. For each shapes graph (, ) there exists a shapes graph (′, ′) such that ′ only consists of atomic targets and for each model ℐ we have ℐ validates (, ) if ℐ validates (′, ′). Proof. Assume that for some concept name ∈ , () ∈ . It sufices to replace each occurrence of in by ( ∧ ), and remove () from . In this way, we enforce that each node with an -label, essential in the validation of another constraint, also validates .
Proposition 1. In recursive SHACL, the problems of deciding SHACL satisfiability and constraint satisfiability are mutually reducible.
Proof. We use ‘ ↔ ′ as a shorthand for ( → ) ∧ ( → ), and ‘ → ′ for ¬ ∨ . Given a shapes graph (, ), such that all targets in are atomic. We distinguish two cases.
In case the considered SHACL fragment does not contain nominals, satisfiability of (, ) is equivalent to satisfiability of all (, ) separately, where := {() ∈ }, for all ∈ such that appears in . Furthermore, note we may replace multiple targets using the same by a single target () for some fresh shape name , given we add ← ⋀︀′()∈ ′ to the set of constraints. Thus, we further assume that = {()}.
The next step is to encode all constraints within a single one: satisfiability of (, {()}) can be reduced to satisfiability of ({^ ← ^}, {^()}), for a fresh shape name ^, and ^ defined in the following way: ^ := ∧ ∀( l )* .
∈
⋀︁ ′← ∈ (′ ↔ ), where ⊆ + contains all roles appearing in any constraint in .
In the case the SHACL fragment does contain nominals, the above described reduction to singleelement targets may no longer be sound. Instead, we use the nominals in the newly defined constraint in the following way: satisfiability of (, ) may be reduced to satisfiability of ({^ ← ^}, {^()}) for each ∈ appearing in , such that ^ := ∀( l )* . ⋀︁ ( → ) ∧ ∈ ()∈
⋀︁ ( ↔ ), ← ∈ where ⊆ + contains all roles appearing in any constraint in .
Names for fragments of SHACL. Let ℒ be the fragment of SHACL such that shape expressions are of the form:
::= | | ⊤ | ¬ | ∧ | ∨ | ∃. | ∀., for ∈ . Let ∃. be a shorthand for ≥ 1 . . Partly following the naming convention of Description Logics, we identify the SHACL fragments in the way presented in Table 1. We write ℒ to denote the SHACL fragment by extending ℒ with the features described by some ⊆ { , ℐ, ℱ , , , ℰ , }. With the superscript ℒe , we denote that the feature eq(, ′), for {, ′} ⊆ is added to the fragment ℒ. Similarly, ℒd corresponds to adding the feature disj(, ′), also for {, ′} ⊆ . In case the fragment ℒ contains the letter ℐ, {, ′} ⊆ +
Note that adding closed() does not increase the expressivity of ℒ. Introducing ≥ 1 . does increase expressivity of ℒ in the supported model semantics, but not in, among others, the leastifxed point semantics [14].
Lemma 2. For each shapes graph (, ) expressible in ℒ extended with expressions of the form closed(), there exists a constraint set ′ expressible in ℒ such that (, ) is (finitely) satisfiable if (′, ) is (finitely) satisfiable.
Proof. Since we are in the restricted context of SHACL satisfiability, that is, roles not mentioned in the constraints are irrelevant, we may replace each occurrence of ‘closed()’ by ‘d∈ ¬∃.⊤’, where := { ∈ ∖ | appears in }, to construct ′. Nominals Inverses Functionality Unqualified number restriction Qualified number restriction Qualified regular path counting Unqualified regular path counting ≥ .⊤
Syntax
Symbol − ≤ 1 .⊤ ≥ .⊤ ≥ . ≥ . ℐ ℱ ℰ
Most of the results in this work are based on the tight connection between SHACL and DLs. In this section, we look at their connection and provide a translation for satisfiability purposes. vice versa. can reduce axioms of the form ⊤ ≡
to ≡ Translation.
We note that for ℒ and more expressive DLs, it is immediate that we can restrict the logic to equivalence axioms only, without afecting its expressivity. That is, ⊑ may be replaced by ⊤ ≡ ¬
⊔ . In these cases, we may also assume without loss of generality that one side of the equivalence is a concept name: it is always possible to introduce a fresh concept name as middle ground. Furthermore, we note that when considering satisfiability of a concept name w.r.t. a TBox , we ⨆︀ ∈ ∀.( ⊓ ), where ⊆ + contains all As we set ← we are considering.
⨆︀ roles appearing in . In this case, we find that is satisfiable w.r.t. if ⊓ is satisfiable w.r.t. ( ∪ { ≡ axioms of the form ≡ , for ∈ ∖ ⊤
. Moreover, we assume that each considered TBox contains for each ∈ at most one concept , possibly making use of ‘⊔’, such that ≡ ∈ . ∈ ∀.( ⊓ )}) ∖ {⊤ ≡ }. That is, in this paper, it will be suficient to consider ∈ implies ()ℐ, = ( )ℐ,, this aligns well with the semantics of recursive SHACL Let us define two translations: , a function translating any ℒℐ concept into a shape expression, and , a function in the opposite direction, translating any shape expression expressible in ℒℐ into an ℒℐ concept. These functions are recursively defined in Table 2, where ∈ is a fresh shape name introduced for every concept name ∈ , and is a fresh concept name for each ∈ . Note that fragments are preserved: an ℒ shape expression translates into an ℒ concept, and validates (, ) given by = {() | ∈ ℐ } and Proposition 2. Let be an ℒℐ TBox such that all axioms are of the form ≡ , and such that no pair { ≡ , ≡
′}, for ̸= ′ is contained in . Then, ℐ is a model of such that ℐ ̸= ∅ if ℐ = { ← () ∧ | ≡ ∈ } ∪ { ← | ≡ ̸∈ }.
Proposition 3. Let (, ) be any ℒℐ shapes graph such that only contains atomic targets. Then ℐ validates (, ), because of the shape assignment , if ℐ′ is a model of { ≡ ( ) | ← ∈ }, such that if () ∈ , then ∈ ℐ ′ . Here, ℐ′ has domain Δℐ = Δℐ′ , and is further defined as: for all ∈ ∖ { | ∈ }, ℐ = ℐ′ and for all ∈ { | ∈ }, ℐ ′ = { ∈ | () ∈ }.
Note that correctness of both propositions is based on the fact that shape and concept names can be considered as very similar, namely as unary labels for individuals, in the setting of determining (finite) satisfiability.
Joint Satisfiability of SHACL and OWL. As envisioned in the W3C SHACL specification [ 15,
Section 1.5] and argued in [
Joint Satisfiability: Given a SHACL fragment ℒ and OWL fragment ℒ′, for each shapes graph (, ) expressible in ℒ and each TBox expressible in ℒ′, decide whether there exists an interpretation ℐ that validates (, ) and is a model of .
Finite Joint Satisfiability: Given a SHACL fragment ℒ and OWL fragment ℒ′, for each shapes graph (, ) expressible in ℒ and each TBox expressible in ℒ′, decide whether there exists a ifnite interpretation ℐ that validates (, ) and is a model of .
Given the above presented translation, it follows that the complexity of deciding (finite) joint satisfiability of SHACL in presence of OWL corresponds to the complexity of deciding (finite) satisfiability in the least-expressive description logic capturing the expressivity of both the translated SHACL fragment, as the OWL fragment.
The following propositions are well-known results in the Description Logic community. These results extend to our setting, using a translation as described in the previous section.
Proposition 4 (for instance [18, 19, 20]). ℒℐ and ℒ have the finite model property, ℒℐℱ does not.
Proposition 5 ([20, 21], and their references). Deciding (finite) satisfiability in ℒ, and ℒℐ is ExpTime-complete. ℒ, ℒℐ, Proposition 6. Deciding (finite) satisfiability in
ℒℐℱ and ℒℐ is NExpTime-complete.
The lower bound for ℒℐℱ follows from constructing a torus of finite size [ 22]; the upper bound from translating ℒℐ into the two-variable fragment of first-order logic with counting quantifiers 2 [23], in which (finite) satisfiability is NExpTime-complete [24].
Proposition 7. ℒℰ and ℒ do not have the finite model property.
Proof. Consider the following constraints, with the target (0, 0):
← ∀ +. =1 +.⊤ ∧ ∀( ∪ )* .( ∧ ) ← ← ¬ ≥ =1 .⊤∧ =1 .⊤∧ =1 ( ∪ ).⊤
1 .⊤ ∨ ∀+.¬ ≥ 1 .⊤
Here, =1 . is a shorthand for ≥ 1 . ∧ ≤ 1 . . Clearly, a way to satisfy the above constraints is in a simple grid on the natural numbers with a diagonal, where true in (0, 0) and and validated everywhere. Here the interpretation of is {(, ), ( + 1, + 1) | ∈ N}, for it is {((, ), (, + 1)) | {, } ⊆ N}, and for the set {((, ), ( + 1, )) | {, } ⊆ N}.
Assume for contradiction there exists a finite model. As must hold in and every individual reachable by , there exists 0, . . . , such that 0 is reachable by * from (0, 0) and {(0, 1), . . . , (− 1, ), (, 0)} is contained in the interpretation of . Note that because of having to validate =1 .⊤∧ =1 ( ∪ ).⊤ in every individual reachable by or , it can be concluded that the set of individuals {0, . . . , } reachable by from any individual in {0, . . . , } must also contain a loop in the interpretation of . Clearly, this generalises to: every individual reachable by + from any individual in {0, . . . , } has a +-path leading to itself. As every individual appearing in a loop of ’s cannot have an outgoing -edge, because of the constraint ← ¬ ≥ 1 .⊤ ∨ ∀+.¬ ≥ 1 .⊤, it follows that every individual reachable by + from any individual in {0, . . . , } cannot have an outgoing -edge. As all individuals in {0, . . . , } are reachable by + from (0, 0), we cannot validate the first conjunct of in (0, 0). This is the contradiction which concludes the proof.
Note the above proof produces a grid, which means only a few more rules need to be introduced to reduce the undecidable domino problem [25] to ℒℰ . It is easy to check this is possible, making the satisfiability problem undecidable. This result is already known for diferent sublogics of ℒℰ , which is discussed in the remainder of this section.
More Fine-Grained Analysis. In the following, we will restrict the expressivity of the regular expressions used in ≥ .⊤ and ≥ . . That is, with ℒ () or ℒ() , for any combination of the role constructs * , ∘ and ∪, we denote the SHACL fragment allowing regular expressions build from only the role constructs in in number restrictions. That is, ℒ (* , ∘ , ∪) = ℒℰ and ℒ(* , ∘ , ∪) = ℒ . We note that the translation presented in Section 4 naturally extends to also capture * , ∘ and ∪ in the number restrictions. Again, we can rely on the vast DL literature: the derived complexity results are the following.
This is a direct consequence of Theorem 6 in [26].
Proof. We can adapt the undecidability proof of unrestricted ℋ in [27] in the following way. That is, instead of using the hierarchy and the given axioms, we consider the following shape expressions. ← ¬ ← ¬ ← ¬ ← ¬ ∧ ¬ ∧ ¬ ∧ ∃1. ∧ ∃1. ∧ ≤ 3 (1 ∪ 1)* .⊤ ∧ ¬ ∧ ¬ ∧ ∃2. ∧ ∃1. ∧ ≤ 3 (2 ∪ 1)* .⊤ ∧ ¬ ∧ ¬ ∧ ∃1. ∧ ∃2. ∧ ≤ 3 (1 ∪ 2)* .⊤ ∧ ¬ ∧ ¬ ∧ ∃2. ∧ ∃2. ∧ ≤ 3 (2 ∪ 2)* .⊤ Note that satisfiability of () corresponds to existence of a grid. Now it is easy to check we can encode a domino tiling problem like in [28]. Thus, the undecidability of the domino problem transfers to this logic, which concludes our proof.
ℒ(∪) is ExpTime-complete. This result is subsumed by Recall we introduced the superscripts ℒd and ℒe to denote the addition of the features disj(, ′) and eq(, ′), respectively. Following the naming convention introduced in the previous section, for any combination of the role constructs * , ∘ and ∪, let ℒ()d , resp. ℒ()e , be the SHACL fragment allowing regular expressions build from only the role constructs in in the disjointness, resp. equality feature, and in number restrictions, in case or is contained in ℒ. That is, recursive SHACL as introduced in the preliminaries, and for satisfiability purposes, corresponds to ℒℐ(* , ∘ , ∪)d,e .
We start with a positive result: adding disjointness does not increase complexity, although the finite model property is easily lost.
Proposition 10. Deciding satisfiability in ℒℐ(* , ∘ , ∪)d is ExpTime-complete, and this fragment does not have the finite model property. In fact, ℒ(* , ∘ )d already lacks this property.
Proof. The upper bound follows from Theorem 4.8 in [29]. To see this, note that disj(, ) is equivalent to the expression ∀( ∩ ).⊥. As the amount of nestings of ‘∩’ in this expression is bounded by a constant, namely 1, the tighter upper bound of ExpTime can be derived.
For the lack of finite model property, consider the following shapes graph (, ):
disj(+, ) ∧ ∃.} and set = {()}. Clearly, the infinite chain of ’s, in which every individual is labelled with an is an infinite model. In fact, it must be possible to homomorphically map this chain into any interpretation that validates (, ). As disj(+, ) has to be true in each individual on the chain, it sufices to check that each approach to loop this chain breaks the disjointness.
Even though equality and disjointness might appear to be duals, this belief is quickly crashed: equality is much harder and easily leads to undecidability.
Proposition 11. Deciding satisfiability in ℒ(∘ )e is undecidable and ℒ(* , ∘ )e does not have the ifnite model property.
Proof. The undecidability result directly follows from results for Description Logics with role value maps [30]. An easy way to also see why the equality feature leads to undecidability is the following constraint set, which encodes a grid.
←
eq(, ) ∧ eq(, ) ∧ ∃. ∧ ∃. ∧ ∀. ∧ ∀. For the lack of finite model property, consider the following shapes graph (, ):
eq(* , ) ∧ ¬eq(+, ) ∧ ∃.}, and set = {()}. Clearly, the infinite chain of ’s, with the reflexive and transitive closure of , in which every individual is labelled with an is an infinite model. In fact, it must be possible to homomorphically map this chain into any interpretation that validates (, ). As eq(* , ) ∧ ¬eq(+, ) has to be true in each individual on the chain, it sufices to check that each approach to loop this chain breaks successful validation.
It looks much better when solely allowing ‘∪’ in the equality and disjointness axioms: (finite) satisfiability in ℒ(∪)d,e is ExpTime-complete. In fact, this holds for much stronger fragments. Proposition 12. Deciding satisfiability in ℒℐ(∪)d,e, and (finite) satisfiability in ℒ(∪)d,e and ℒℐ(∪)d,e is ExpTime-complete, and the latter two fragments have the finite model property. Proof. Note that for a union of roles, eq(, ) may be reduced to ∀(( ∖ ) ∪ ( ∖ )).⊥, where ∖ ′ := ℐ ∖ ′ℐ , and disj(, ) to ∀( ∩ ).⊥. Thus, in case only ‘∪’ is allowed, the equality and disjointness features reduce to simple roles, which means the above fragments can be reduced to the description logics ℐ, , resp. ℐ. For all these logics, satisfiability is known to be decidable in ExpTime [31]. Furthermore, , and ℐ have the finite model property [32].
We note that the results described in this paper do not provide a complete picture of all known decidability results in the DL setting.
We looked at the tight connection between Description Logics and SHACL. In this way, we derived many new complexity results for deciding (finite) satisfiability in SHACL. Specifically, for the general satisfiability problem the picture looks quite complete: as far as the author knows, only some small fragments remain unclear, like ℒ(* , ∪)e, or ℒ(* )d,e. However, when looking at finite satisfiability, the status is quite the opposite: a lot of work remains to be done. Specifically in the setting of SHACL, one of the standard tools for managing concrete data sets, the latter case is of uttermost importance.
Another direction for future work is to look at diferent semantics: in this paper, we considered (finite) satisfiability under the supported model semantics. However, there are more possibilities to consider: for instance the stable-model, or well-founded semantics. As far as the author knows there are no known complexity results regarding satisfiability or containment for any semantics other than the supported model semantics, leaving a major gap. Specifically, as researching complexity of satisfiability and containment problems is essential for determining which semantics are suitable in optimised SHACL-based solutions.
I would like to thank Magdalena Ortiz and Bartosz Bednarczyk for their support in this project, and the anonymous reviewers for their feedback.
The project leading to this application has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 101034440.
of Lecture Notes in Computer Science, Springer, 2020, pp. 366–383. URL: https://doi.org/10.1007/ 978-3-030-62419-4_21. doi:10.1007/978-3-030-62419-4\_21. [12] B. Bogaerts, M. Jakubowski, J. V. den Bussche, SHACL: A description logic in disguise, in: G. Gottlob, D. Inclezan, M. Maratea (Eds.), Logic Programming and Nonmonotonic Reasoning - 16th International Conference, LPNMR 2022, Genova, Italy, September 5-9, 2022, Proceedings, volume 13416 of Lecture Notes in Computer Science, Springer, 2022, pp. 75–88. URL: https://doi.org/ 10.1007/978-3-031-15707-3_7. doi:10.1007/978-3-031-15707-3\_7. [13] B. Bogaerts, M. Jakubowski, J. V. den Bussche, Expressiveness of SHACL features and extensions for full equality and disjointness tests, Log. Methods Comput. Sci. 20 (2024). URL: https://doi.org/ 10.46298/lmcs-20(1:16)2024. doi:10.46298/LMCS-20(1:16)2024. [14] A. Oudshoorn, M. Ortiz, M. Simkus, Reasoning with the core chase: the case of SHACL validation over ELHI knowledge bases, in: L. Giordano, J. C. Jung, A. Ozaki (Eds.), Proceedings of the 37th International Workshop on Description Logics (DL 2024), Bergen, Norway, June 18-21, 2024, volume 3739 of CEUR Workshop Proceedings, CEUR-WS.org, 2024. URL: https://ceur-ws.org/ Vol-3739/paper-7.pdf. [15] W3C, Shape constraint language (SHACL), Technical Report. (2017). https://www.w3.org/TR/shacl. [16] M. Krötzsch, OWL 2 profiles: An introduction to lightweight ontology languages, in: T. Eiter, T. Krennwallner (Eds.), Reasoning Web. Semantic Technologies for Advanced Query Answering 8th International Summer School 2012, Vienna, Austria, September 3-8, 2012. Proceedings, volume 7487 of Lecture Notes in Computer Science, Springer, 2012, pp. 112–183. URL: https://doi.org/10. 1007/978-3-642-33158-9_4. doi:10.1007/978-3-642-33158-9_4. [17] O. Savkovic, E. Kharlamov, S. Lamparter, Validation of SHACL constraints over KGs with OWL 2 QL ontologies via rewriting, in: P. Hitzler, M. Fernández, K. Janowicz, A. Zaveri, A. J. G. Gray, V. López, A. Haller, K. Hammar (Eds.), The Semantic Web - 16th International Conference, ESWC 2019, Portorož, Slovenia, June 2-6, 2019, Proceedings, volume 11503 of Lecture Notes in Computer Science, Springer, 2019, pp. 314–329. URL: https://doi.org/10.1007/978-3-030-21348-0_21. doi:10.1007/978-3-030-21348-0\_21. [18] S. Rudolph, Foundations of description logics, in: A. Polleres, C. d’Amato, M. Arenas, S. Handschuh, P. Kroner, S. Ossowski, P. F. Patel-Schneider (Eds.), Reasoning Web. Semantic Technologies for the Web of Data - 7th International Summer School 2011, Galway, Ireland, August 23-27, 2011, Tutorial Lectures, volume 6848 of Lecture Notes in Computer Science, Springer, 2011, pp. 76–136.
URL: https://doi.org/10.1007/978-3-642-23032-5_2. doi:10.1007/978-3-642-23032-5\_2. [19] C. Lutz, C. Areces, I. Horrocks, U. Sattler, Keys, nominals, and concrete domains, J. Artif. Intell.
Res. 23 (2005) 667–726. URL: https://doi.org/10.1613/jair.1542. doi:10.1613/JAIR.1542. [20] F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, P. F. Patel-Schneider (Eds.), The Description
Logic Handbook: Theory, Implementation, and Applications, Cambridge University Press, 2003. [21] C. Lutz, U. Sattler, L. Tendera, The complexity of finite model reasoning in description logics, Inf.
Comput. 199 (2005) 132–171. URL: https://doi.org/10.1016/j.ic.2004.11.002. doi:10.1016/J.IC. 2004.11.002. [22] S. Tobies, The complexity of reasoning with cardinality restrictions and nominals in expressive description logics, J. Artif. Intell. Res. 12 (2000) 199–217. URL: https://doi.org/10.1613/jair.705. doi:10.1613/JAIR.705. [23] S. Tobies, Complexity results and practical algorithms for logics in knowledge representation, Ph.D. thesis, RWTH Aachen University, Germany, 2001. URL: http://sylvester.bth.rwth-aachen.de/ dissertationen/2001/082/01_082.pdf. [24] I. Pratt-Hartmann, Complexity of the two-variable fragment with counting quantifiers, J.
Log. Lang. Inf. 14 (2005) 369–395. URL: https://doi.org/10.1007/s10849-005-5791-1. doi:10.1007/ S10849-005-5791-1. [25] R. Berger, The undecidability of the domino problem, 66, American Mathematical Soc., 1966. [26] F. Baader, U. Sattler, Expressive number restrictions in description logics, J. Log. Comput. 9 (1999) 319–350. URL: https://doi.org/10.1093/logcom/9.3.319. doi:10.1093/LOGCOM/9.3.319. [27] I. Horrocks, U. Sattler, S. Tobies, Practical reasoning for very expressive description logics, Log. J.
IGPL 8 (2000) 239–263. URL: https://doi.org/10.1093/jigpal/8.3.239. doi:10.1093/JIGPAL/8.3. 239. [28] F. Baader, U. Sattler, Number restrictions on complex roles in description logics: A preliminary report., in: KR, 1996, pp. 328–339. [29] S. Göller, M. Lohrey, C. Lutz, PDL with intersection and converse: satisfiability and infinite-state model checking, J. Symb. Log. 74 (2009) 279–314. URL: https://doi.org/10.2178/jsl/1231082313. doi:10.2178/JSL/1231082313. [30] M. Schmidt-Schauß, Subsumption in KL-ONE is undecidable, in: R. J. Brachman, H. J. Levesque, R. Reiter (Eds.), Proceedings of the 1st International Conference on Principles of Knowledge Representation and Reasoning (KR’89). Toronto, Canada, May 15-18 1989, Morgan Kaufmann, 1989, pp. 421–431. [31] D. Calvanese, T. Eiter, M. Ortiz, Regular path queries in expressive description logics with nominals, in: C. Boutilier (Ed.), IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009, 2009, pp. 714–720. URL: http://ijcai.org/Proceedings/09/Papers/124.pdf. [32] B. Bednarczyk, E. Kieronski, Finite entailment of local queries in the Z family of description logics, in: Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022, AAAI Press, 2022, pp. 5487–5494. URL: https://doi.org/10.1609/aaai.v36i5.20487. doi:10. 1609/AAAI.V36I5.20487.