Many approaches to query answering in Description Logics (DLs) adopt the certain answer semantics, which is natural for standard query languages without negation, but falls short when negation is involved. Since negation plays a crucial role in many applications, alternative semantics are needed. Core universal models are increasingly accepted as a means to give a semantics to queries with negation. In this paper, we consider the problem of evaluating (possibly recursive) SHACL expressions over the core universal model of an ℰℒℋℐ KB. SHACL, recently proposed as a standard constraint language for RDF data, is a natural and powerful query language, and the fragment we consider adds regular path navigation to semi-positive monadic Datalog with acyclic rule bodies. We first propose a construction of a finite representation of the core universal model, based on a novel calculus for ℰℒℋℐ that gives up the data-independence to avoid the best-case exponential behaviour of similar approaches, and which we believe can lead towards an eficient implementation. Then we leverage this finite representation to reduce validation in the presence of ontologies to plain SHACL validation, similarly to previous algorithms but avoiding their best-case exponential behaviour. Our algorithms yield tight data- and combined-complexity bounds for the studied SHACL validation problem, which coincide with plain consistency testing in ℰℒℋℐ.
Evaluating queries over description logic (DL) knowledge bases has been the subject of huge research
eforts over almost two decades. Here, the certain answer semantics has played a prominent role in
elegantly handling information incompleteness for large classes of queries: answering a query consists
of computing the intersection of query answers over all models of the input knowledge base (KB). This
problem can easily become computationally very costly for expressive DLs, and it is provably more
expensive than standard reasoning in most of the popular extensions of ℒ [
The universal model property is closely related to the notion of a chase procedure known from
databases, originally studied for reasoning about integrity constraints [
Unfortunately, the situation is very diferent when queries involve negation as failure, which allows
us to query about the absence of information, e.g., to ask for objects that do not (provably) have
some property. Such queries are highly desirable in KR and have been advocated in several papers
[
The first major contribution of this paper is a method for computing a finite representation of a (possibly infinite)core universal model of an ℰ ℒℋℐ KB. This method includes a data-aware version of a consequence-based calculus for ℰ ℒℋℐ. Specifically, we define a collection of reasoning rules that incrementally builds a finite representation of a core universal model for a given input ABox. Unlike previous consequence-based inference procedures for ℰ ℒℋℐ, are the rules in our calculus aware of input data. This avoids the main drawback of the previous approaches: data-independent computations easily lead to best-case exponential behavior.
After presenting our calculus, we use it to address a timely and challenging problem: validation of (possibly recursive) SHACL in the presence of ontologies. SHACL is a recently introduced W3C recommendation for writing constraints over RDF data [16]. It has also been formalised in logic and has connections to DLs [17, 18, 19, 20]. The SHACL standard envisions SHACL validation performed in the presence of ontologies but does not describe how this should be realised. SHACL is closely related to DLs and typical formalisms studied in the setting of ontology-mediated queries. We concentrate on semi-positive SHACL shapes, which allow for negation of ontology predicates, but not of shape names. This fragment can be seen as semi-positive monadic Datalog queries with acyclic rule bodies and regular path expressions, and it already raises the issues with the certain answer semantics discussed above.
Following our previous work [15], we use a core universal model of the data and ontology for validation. This leads us to our second contribution: an algorithm for evaluating SHACL expressions over the finite representation of a core universal model of an ℰ ℒℋℐ KB. This procedure is based on the rewriting from [15], but unlike that work, the algorithm presented here is not best-case exponential, potentially paving the way towards implementation. Moreover, we show that checking if a given ℰ ℒℋℐ KB validates a shapes graph is ExpTime-complete and PTime-complete in combined and data complexity, respectively. These bounds are the best we could hope for, since they coincide with the complexity of consistency testing in ℰ ℒℋℐ.
Let , , and be infinite sets of concept names, individual names, and role names, respectively. Let + := ∪ {⊤} and + := {, − | ∈ } denote roles. For every ∈ , let (− )− = . For each set of roles ⊆ + , set − := {− | ∈ + }. Let be an infinite set of blank nodes disjoint from . Call () and (, ) atoms, for each ∈ , ∈ + and {, } ⊆ ∪ . We let Δ denote the domain of , i.e. the elements of ∪ that appear in . In case Δ ⊆ , we call an ABox. In the rest of this paper, we assume that for all ABoxes , if (, ) ∈ , then − (, ) ∈ too. For a tuple ⃗ = (1, . . . , ) and 1 ≤ ≤ , we let (⃗) = be its -th projection. Morphisms. Let and ′ be sets of atoms. A homomorphism from to ′ is a function ℎ : Δ → Δ′ such that for all {, } ⊆ ∪ , all ∈ and all ∈ , (i) if ∈ Δ ∩ , then ℎ() = , (ii) if () ∈ , then (ℎ()) ∈ ′, and (iii) if {(, ), − (, )} ∩ ̸= {}, then {(ℎ(), ℎ()), − (ℎ(), ℎ())} ∩ ′ ̸= {}. A homomorphism is called strong when (ii) and (iii) are strengthened to “() ∈ if (ℎ()) ∈ ′” and “{(, ), − (, )} ∩ ̸= {} if {(ℎ(), ℎ()), − (ℎ(), ℎ())} ∩ ′ ̸= {}”, respectively. An embedding is a strong injective homomorphism, an isomorphism is a surjective embedding and an endomorphism of is a homomorphism from to itself. A set of atoms is a core when all its endomorphisms are embeddings. The core of a set of atoms is a set of atoms ℬ ⊆ , such that (i) there exists an endomorphism ℎ from to ℬ, (ii) ℬ is the restriction to the image of ℎ, and (iii) ℬ is a core.We write →−− coℬre . Each finite set of atoms has a core that is unique up to isomorphism [21].
The Description logic ℰ ℒℋℐ. We are considering a normalised version of ℰ ℒℋℐ, i.e., the axioms we consider have one of the following normal forms.
1 ⊓ . . . ⊓ ⊑ 1 ⊑ ∃.2 ∃.1 ⊑ ⊑ ′ Here, {1, . . . , } ⊆ + , ∈ + ∪ {⊥} and {, ′} ⊆ + . An ℰ ℒℋℐ TBox is a set of such axioms. An (ℰ ℒℋℐ) knowledge base ( , ) consists of an ABox and an ℰ ℒℋℐ TBox . As usual, we use first-order interpretations to define the semantics. Note that any set of atoms can be viewed as an interpretation with domain Δ.
Building the chase. The function , for each ∈ ∪ , that translates concepts into a set of atoms is inductively defined in the following way: (⊤) := {}, () := {()}, (∃.) := {(, ), − (, ), ()} for some fresh variable and ( ⊓ ′) := () ∪ (′). We say is an applicable match for an axiom ⊑ ∈ in a set of atoms , when there exists a homomorphism ℎ from () to , such that ℎ() = and there is no homomorphism from () to such that ℎ() = . We use the notation (, ⊑ ) ∈ m∃( , ) when is of the form ∃. for some ∈ + , ∈ + , and the notation (, ⊑ ) ∈ m( , ) when ∈ . Similarly, (, ) is an applicable match for ⊑ ′ ∈ in a set of atoms , when (, ) ∈ and ′(, ) ̸∈ . In that case, we write ((, ), ⊑ ′) ∈ m( , ). , Definition 1. For an ℰ ℒℋℐ TBox , a set ⊆ ∪ and ABoxes , ′, we let →−− ′ if ′ = ∪
⋃︁ (,⊑)∈m∃( ,),∈ () ∪
⋃︁ (,⊑)∈m( ,) () ∪
⋃︁ ((,),⊑′)∈m( ,) ′(, ).
When = ∪ , we drop the .
Note that the restricts the set of nodes for which we consider applicable existential matches. We use the notation (→)′ to denote that there exists an such that (→)′ and for all ′′ such that ′ → ′′ we find ′ = ′′, for each binary relation →. With ∘ we denote the concatenation of two binary relations, that is, → ∘ → ′ ℬ if there exists ′ such that → ′ and ′ →′ ℬ, for each pair of binary relations → and →′.
Core chase. In the core chase, all applicable matches are fired simultaneously, followed by a core
check. This procedure is repeated until it terminates (which is not guaranteed): given a knowledge
core )ℬ
base , , the core chase is the unique, up to isomorphism, structure ℬ such that →(− ∘ →−−
[
In this section, we present our first major contribution: computing a finite representation of a core universal model for a given ℰ ℒℋℐ KB. In a nutshell, the good successor configuration tells us for each configuration of a node and its immediate ‘neighbourhood’, the precise configuration of blank nodes that should be introduced as immediate successors.
In contrast to DL-Liteℛ, in ℰ ℒℋℐ the relevant context is not only the incoming roles , but also the concepts satisfied at the already existing neighbours. For simplicity, we focus on describing the good successors of the blank nodes introduced during the chase, which have a unique predecessor in the forest-like structure. For describing the successor configurations, we use types and successor types. A type ∈ ℱ is defined as an element of (+ ) × (+ ) × (+ ), and a successor type ∈ is an element of (+ ) × (+ ). A type describes a pair of nodes and the roles between them, while a successor type describes a set of roles leading to one node. A pair (, {1, . . . , }) in the good configuration means that a node that is connected to its predecessor as described by , and needs successors as prescribed by 1, · · · , , see Figure 1. Furthermore, we define the inverse function inv : (+ )× (+ ) → (+ )× (+ ) on successor types by setting inv () := ( 2(), ( 1())− ). (Recall that 1 and 2 are the first and second projection of a tuple, respectively, as defined in the preliminaries.)
Defining the successors of all types that may occur in the chase for any possible ABox would necessarily lead to a strictly exponential behaviour. While exponentiality is in general unavoidable, as standard reasoning tasks are ExpTime complete, we want to avoid it for as many instances as possible. Hence in the following we build the good successor configuration carefully, to avoid bestcase exponential behaviour. We start from the input ABox , and extend it to satisfy all applicable axioms, but we restrict the satisfaction of existential axioms to only create blank nodes that are directly neighbouring the ABox. We call this structure 1. The freshly introduced blank nodes in 1 have exactly one predecessor and can thus be described by a type. We take exactly those types as initial live types, and compute the pre-good configuration of successors that each live type needs. In each step of the computation we add to the live types the new successor types. It might happen that we encounter a so-called loop computation: the created successors may propagate some concept back to the current node, This information is saved in a relation as the pair of the type and the implied concept, and the pre-good successor pairs are updated with this information. Unlike DL-Liteℛ, derived information in ℰ ℒℋℐcan propagate through the model, and in particular, afect the concepts satisfied by ABox individuals. Thus the information from the loop computation must be used to update also the extended ABox, from which we retrieve fresh, updated live types for the next round of building pre-good successors. This continues in rounds until the process terminates.
Definition 2. Given an ℰ ℒℋℐ knowledge base ( , ). Let 1 be the unique (up to isomorphism) set of atoms such that →−(−− , )∘ →−− core 1. Let be the following set of types, for each ≥ 1 := { ∈ ℱ | ∈ , ∈ , ∈ + , 1() = { ∈ | () ∈ } ∪ {⊤}, 2() = { ∈ + | (, ) ∈ }, 3() = { ∈ | () ∈ } ∪ {⊤}}.
Construct the pre-good successor relation, psucc ⊆ ℱ × (), initially set to (, {}) ∈ psucc for all ∈ , and the loop computation relation, ⊆ ℱ × , initially empty, for each ≥ 1 by applying the following rules exhaustively. 1. If {(, 1), . . . , (, )} ⊆ and 1 ⊓ · · · ⊓
⊑ ∈ , then update by adding (, ); 2. If (, ) ∈ psucc and 1 ⊓ · · · ⊓ ⊑ ∈ such that there exists 1 ≤ ≤ , with ⊆ 2( ), but ̸∈ 2( ), then update the entry (, ) in psucc to (, {1, . . . , ( 1( ), 2( ) ∪ {}), . . . , }); 3. If (, ) ∈ psucc and ∃. ⊑ ∈ such that there exists 1 ≤ ≤ ∈ 2( ), but ̸∈ 1(), then update by adding (, ); , with ∈ 1( ) and 4. If (, ) ∈ psucc and ∃. ⊑ ∈ such that there exists 1 ≤ ≤ , with − ∈ 1( ) and ∈ 1() ∪ {′ | (, ′) ∈ }, but ̸∈ 2( ), then update the entry (, ) in psucc to (, {1, . . . , ( 1( ), 2( ) ∪ {}), . . . , }); (∃. ), = { ∈ Δ | ∃′ : (, ′) ∈ ∧ ′ ∈ ,}
, = { | () ∈ } 5. If (, ) ∈ psucc and ⊑ ′ ∈ such that there exists 1 ≤ ≤ , with ∈ 1( ), but ′ ̸∈ 1( ), or − ∈ 1( ), but ′− ̸∈ 1( ) then update the entry (, ) in psucc to (, {1, . . . , ( 1( ) ∪ {′}, 2( )), . . . , }); 6. If {(, ), (′, ′)} ⊆ psucc such that there exists 1 ≤ ≤ , with 1() = 3(′), 1( )− = 2(′) and 2( ) = 1(′), then update psucc() to (, {1, . . . , ( 1( ), 2( ) ∪ {′ | (′, ′) ∈ }), . . . , }); 7. If (, ) ∈ psucc and ⊑ ∃. ∈ such that ∈ 1(), and ̸∈ 2() or ̸∈ 3(), and for all 1 ≤ ≤ , ̸∈ 1( ) or ̸∈ 2( ), then update the entry (, ) in psucc to (, ∪ {({}, {⊤, })}); 8. If (, ) ∈ psucc and there exists 1 ≤ , ≤ such that ̸= , 1( ) ⊆ 1() and 2( ) ⊆ 2(), then update the entry (, ) in psucc to (, ∖ { }); 9. If (, ) ∈ psucc, then for each 1 ≤ ≤ , such that ((inv ( ), 1()), ′) ̸∈ psucc, for any ′, add ((inv ( ), 1(), {}) to psucc; where we use the notation , , ′ as a shorthand for {1, . . . , }, {1, . . . , }, resp. {′1, . . . , ′′ }. Now, let ℬ be the smallest set of atoms such that ⊆ ℬ and, if (, ) ∈ and there exists ∈ , ∈ such that 1() ⊆ { ∈ | () ∈ ℬ} ∪ {⊤}, 2() ⊆ { ∈ + | (, ) ∈ ℬ} and 3() ⊆ { ∈ | () ∈ ℬ} ∪ {⊤}, then () ∈ ℬ. Define +1 as the unique (up to isomorphism) set of atoms such that ℬ→−(−− , )∘ →−− core +1. + for .
Proposition 1. There exists an ≥ 1 such that = +1. We use the notation
First, note that by construction, ⊆ +1. Furthermore, the amount of blank nodes neighbouring a node in the data, such that they do not subsume each other, is restricted by the amount of existential axioms in .
We can now define the good successor configuration as the limit of psucc, and the set ℱ , of live types as the types occurring in it.
Definition 3. Given an ℰ ℒℋℐ knowledge base ( , ). Let ≥ 1 be the smallest such that = +1. Set succ , = psucc and let ℱ , ⊆ ℱ be such that ∈ ℱ , if there exists such that (, ) ∈ succ ,.
In the good successor configuration, we only add successors that are directly required by the axioms and whose set of roles can be summarised by one role that implies all others. This will be useful later. We denote by cl () ⊆ + the smallest set such that ∈ cl () and if ′ ∈ cl () and ′ ⊑ ′′ ∈ or ′− ⊑ ′′− ∈ , then ′′ ∈ cl ().
Proposition 2. Given an ℰ ℒℋℐ knowledge base ( , ). If succ ,(, ), then for each ∈ there exists a ⊑ ∃. ∈ such that ∈ 1(), cl () = 1() and ∈ 2().
When computing the good successor configuration, we are computing all loops, that is, all implications that may propagate back during the chase. In a nutshell, using the good successors is analogous to doing the chase with the closure of under semantic consequences |= ⊑ . Proposition 3. Let * := { ⊑ | |= ⊑ }, and let ℬ be the unique (up to isomorphism) set of atoms such that →−−−(− * , )∘ →−− coℬre . Then + ∼= ℬ.
The proof relies on the fact that all relevant loop computations are covered in the construction of the good successor configuration. As we consider live types, all possible configurations in the anonymous parts are considered and all inferred loops are saved in the loop computation list.
The good successor configuration allows us to easily build the desired universal core model.
We introduce some additional notation. Let be a set of atoms. For ⊆ ∪ , we define the set () of neighbours of . We also define the type type() of a blank node ∈ with |()| = 1, where ∈ ().
() := ⋃︁ { ∈ ∪ | (, ) ∈ ∨ (, ) ∈ , ∈ } ∈ type() := ({ ∈ | () ∈ } ∪ {⊤}, { ∈ + | (, ) ∈ },
{ ∈ | () ∈ } ∪ {⊤}) + and adding successors according to succ ,.
We can now build the model, starting from Definition 4. Given an ℰ ℒℋℐ knowledge base ( , ), define the core universal model core( , ) as the union of the sequence 1, 2, . . ., that is recursively defined in the following way + • 1 := ; • +1 is constructed from by adding, for each ∈ such that | ()| = 1 and succ ,(type (), ) holds for some , the following atoms for each ∈ , with a fresh ∈ for each ∈ – {(, ), − (, )} ⊆ +1 for each ∈ 1(); – () ∈ +1 for each ∈ 2().
Note that we can see each entry in the sequence 1, 2, . . . as layers such that the freshly added blank nodes in have distance to the ABox.
We can now show that ( , ) is a model, that it is a core, and that it is universal. Proposition 4. For all ℰ ℒℋℐ knowledge bases ( , ), ( , ) is a model of ( , ).
The proof is based on the idea that all axioms that we consider are all in normal form. Thus, the rules for the pre-good successor relation sufice to ensure that all axioms are satisfied in the part outside of the ABox . Closer to the data, the result follows from Proposition 3.
Proposition 5. For all ℰ ℒℋℐ knowledge bases ( , ), ( , ) is a core.
Proof. A set of atoms has a core cover when there exist finite sets of atoms ℬ1 ⊆ ℬ 2 ⊆ . . . with = ⋃︀≥ 1 ℬ, such that for all ℬ, each homomorphism ℎ : Δℬ → Δ is an embedding.
From [22], Theorem 16, we learn that each set of atoms that has a core cover is a core. Thus, it sufices to show that ℬ = is a core cover for ℬ = ⋃︁ = core( , ).
≥ 1 It is immediate that for each , the identity mapping ℎ : Δ → Δcore( ,) given by ↦→ is an embedding. By induction on it is shown that each homomorphism from to core( , ) is equal to the identity mapping.
• = 1. By definition 1 = + , which is by construction a core. Note that for all endormorphisms on cores it holds that if one node is mapped to itself, all nodes have to be mapped to themselves. + Furthermore, note that each ∈ Δcore( ,) ∖ Δ does not have a neighbour in the ABox, so the + + to core( , ) is contained in + . As all nodes in Δ ∩ image of each homomorphism from have to be mapped to themselves, we can conclude the required.
• = + 1. Let us consider some ∈ Δ+1 ∖ Δ . By induction hypothesis, we know that for all homomorphisms ℎ : Δ+1 → Δcore , ℎ(′) = ′ for all ′ ∈ Δ . Moreover, we know there exists ∈ Δ with succ ,(type (), ) such that there exists ∈ that led to the introduction of , i.e., +1 () = {}. So, for each homomorphism ℎ : Δ+1 → Δcore( ,), we find ℎ() ∈ ( ,)(). By construction, the neighbourhood of exists of (i) such that () = {}, however, ℎ() = would mean that the preconditions of introducing a new successor type in rule 7 in Definition 2 were not applied properly, and (ii) ′ such that there exists ′ ∈ with ̸= ′ that led to the introduction of ′, however, ℎ() = ′ would mean that rule 8 of Definition 2 was not properly applied. Thus, we must conclude that ℎ() = for all ∈ Δ+1 , which concludes this induction.
Proposition 6. For all ℰ ℒℋℐ knowledge bases ( , ), ( , ) is universal.
The idea of the proof is that we only introduce new successors if there exists an applicable existential axiom, and that all information in core( , ) is a direct consequence of the applicable axioms and will be derived in every model.
Finally, we show that if the core chase terminates, it results in core( , ).
Theorem 1. Given an ℰ ℒℋℐ knowledge base ( , ) such that ℬ is the unique, up to isomorphism, structure such that →(− ∘ →−− core )ℬ, then ℬ ∼= core( , ).
Proof. First, note that both ℬ, by definition, and core( , ), by Proposition 5 are cores. Therefore, as ℬ
is finite, it sufices to show that there exists homomorphisms in both directions. Note that core( , )
is a model by Proposition 4. As ℬ is a universal model, [
The authors of [22] show that the stable chase does not always yield a universal model for existential rules, but it is unclear whether the same result holds for the restriction to ℰ ℒℋℐ. If the stable chase for ℰ ℒℋℐ is universal, then Theorem 1 can be extended to the stable chase.
The core chase construction described in [
We now consider the problem of SHACL validation in the presence of ℰ ℒℋℐ ontologies.
First we introduce the fragment of SHACL we consider, which we call semi-positive SHACL. Like in [15], we follow the formalisation of SHACL in [17]. Let be an infinite set of shape names, disjoint from , , + and + . A shape expression is built in the following way
::= | ¬ | | ¬ | ∧ | ∃. | , for ∈ , ∈ , ∈ and a regular path expression such that ::= | ∪ | ∘ | * , for ∈ + , where "∪" is the standard union of relations, "∘ " concatenation as described in the preliminaries and "* " the Kleene star. A constraint is an expression of the form ← , for ∈ and a shape expression. A shapes graph (, ) is a pair consisting of a set of constraints and a set of targets . Targets are of the form (), where ∈ and ∈ . Given a set of atoms , a shape assignment is a set of shape atoms of the form (), for ∈ , ∈ Δ. Given a shape expressions , a shape assignment , and a set of atoms , define , ⊆ Δ inductively as in Figure 2, where (, ′) ∈ if there exists 1 · . . . · in the language defined by and {1(, 1), . . . , (− 1, ′)} ⊆ .
Just like in [15], we consider the least fixed point semantics for SHACL. We define an immediate consequence operator , that maps shape assignments to shape assignments: ,() := ∪ {() | ← ∈ , ∈ ( ),}. For a set of atoms and a shapes graph (, ), we say that validates (, ) when is contained in the least fixed point of ,. In the presence of a TBox , we define the semantics of validation using the core universal model. That is, we say that ( , ) validates (, ) in case core( , ) validates (, ).
Our goal is now to reduce validation in the presence of a TBox, to plain validation over a set of atoms. The following normal form for SHACL constraints will facilitate this goal.
Definition 5.
A SHACL constraint is in normal form if it has one of the following forms (NC1) ← (NC4) ← ¬
(NC2) ← ¬ (NC5) ←
(NC3) ← ′ ∧ ′′ (NC6) ← ∃ .′, where ∈ , ∈ + , {, ′, ′′} ⊆ and ∈ .
Proposition 7. Each set of semi-positive SHACL constraints can be translated in time polynomial in ||, into a set of semi-positive constraints ′ in normal form such that for all that do not use the freshly introduced shape names, and all and , we have that ( , ) validates (, ) if ( , ) validates (′, ).
Proof. With a similar construction as of Proposition 4.2 in [18], it is easy to see that each constraint can be translated in polynomial time into the a normal form consisting of (NC1) until (NC5) as above, and (NC6’) ← ∃ .′. To normalise ← ∃ .′, suppose ℳ = (, Σ, , Δ, ) is the nondeterministic ifnite automaton recognising . Take fresh shape names for each ∈ and add the following constraints ← ∧ , ← ∃ .′ if (, , ′) ∈ Δ and ← ′ ∧ ′. Note that this automaton can be constructed in polynomial time, which is a standard result in the literature, see for instance [24].
We are ready now to reduce validation to the case without a TBox. Given a TBox and a set of atoms , or more specifically, the succ , that represents a universal core model of ( , ). We transform a shapes graph (, ) into a new shapes graph ( ,, ) such that ( , ) validates (, ) if ′ validates ( ,, ), for some set of atoms ′ that can be easily obtained from and the construction of succ ,. Unlike the similar rewriting for DL-Liteℛ, the variant we introduce here does not work for every set of atoms : we can only guarantee soundness and completeness if the set of atoms is such that succ , represents the core universal model of ( , ). We compromise the data independence, but in this way, we avoid the best case exponentially of its predecessor [15].
We use a fresh concept name ̂︀ ∈ to decorate the outer layer of + , and define * := + ∪ {̂︀() | ∈ Δ+ ∩ }.The elements in our rewriting are triples (, , ) ⊆ ℱ , × ({∃. | ∈ + , ∈ }) × (): is a live type, a set of assumptions and a set of shape names. The starting set of our rewriting is such that (, , ) ∈ if • if ∃.′ ∈ , there exists ← ∃ .′ ∈ and ∈ 2(), and • ∈ if there exists ∃.′ ∈ such that ← ∃ .′ ∈ .
Our rewriting algorithm adds shape names to the heads . Specifically, we update (, , ) ∈ , to (, , ∪ {}) when any of the following holds: 1. ←
∈ , ∈ 1(), ̸∈ , or 2. ← ¬ 3. ← ¬ ∈ , ̸∈ 1(), ̸∈ , or ∈ , ̸∈ , or 4. ← 1 ∧ 2 ∈ , {1, 2} ⊆ , ̸∈ , or 5. ← ∃ .1 ∈ , and there exists (′, ′, ′) ∈ such that, for some ∈ with succ ,(, ), we have ′ = (inv (), 1()), 1 ∈ ′, − ∈ 2() and { | ∃. ∈ ′} ⊆ .
Let sat () be the result of exhaustively adding shape names as above. The triples in sat () are then translated into the set of constraints , in the following way.
If (, , ) ∈ sat (), then for each ∈ the following constraint is contained in , ←
⋀︁ ∈ 1() ∧ ∃.
⋀︁ ∈ 3() ∧
⋀︁ ∃.′∈ ∃.′ ∧ ̂︀, where ∈ 2() is such that for all ′ ∈ 2() we have ′ ∈ cl (). Note that the existence of is guaranteed by Proposition 2.
This gives us the desired rewriting. Its proof of correctness is analogous to the one in [15]. Theorem 2. Given an ℰ ℒℋℐ knowledge base ( , ) and (, ) a semi-positive SHACL shapes graph. Then it holds that ( , ) validates (, ) if * validates ( ,, ).
Since we are taking the input into account, we do not have to consider all possible types and is not best-case exponential. However, there are still ways to optimise the rewriting. The first and simplest optimisation is to restrict the form of the starting sets even more, that is, not all ∈ will ever interact with each other. So, let rel () ⊆ be defined as the smallest set such that ∈ rel (); if ′ ← ′′ ∧ ′′′ ∈ and {′, ′′, ′′′} ∩ rel () ̸= {}, then {′, ′′, ′′′} ∈ rel (); and if ′ ← ∃ .′′ ∈ and {′, ′′} ∩ rel () ̸= {}, then {′, ′′} ∈ rel (). The restriction is then that (, , ) is only considered to be in the starting set in case there exists ∈ such that ⊆ rel (). This optimisation is mostly useful for sets of constraints that relatively use a small amount of role names. Another more involved optimisation is based on the close correspondence between the SHACL fragment we are considering and ℰ ℒℋℐ in normalised form. We can translate the SHACL constraints into ℰ ℒℋℐ axioms, introducing for each existing concept name a fresh concept name to denote the absence of this concept name in succ ,. A similar algorithm to the one in Section 3 will then decorate the good successor configuration with all relevant shape names. We believe that the latter version may be better suited for implementation.
However, all these optimisations cannot avoid ExpTime-complexity in the worst case. The proof of the next claim is an easy generalisation of the one in [15]. To show PTime-completeness in data complexity the rewriting can be made data independent as in [15].
Theorem 3. In the presence of ℰ ℒℋℐ TBoxes, SHACL validation is ExpTime-complete in combined complexity and PTime-complete in data complexity. This holds also for positive constraints.
In this paper, we introduced a new, more eficient representation of a core universal model. We had shown in [15] that this can be done in a data-independent way; the construction there is for DL-Liteℛ, but a data-independent computation for ℰ ℒℋℐ would not be harder than the one we have presented here. Instead, by considering the exact configurations that appear in the data, we have chosen to focus solely on computing the relevant parts, highly reducing the number of good successor configurations and TBox subsumptions that need to be computed. Thus, this is a first step towards an eficient implementation of the core chase.
We further focus on one of many application areas of this technique: we use the alternative representation of a core universal model to reduce SHACL validation combined with ℰ ℒℋℐ TBoxes to plain SHACL validation. Also here, we could take all types for a data-independent rewriting, but restricting it to the live types allows us to avoid an exponential computation in many cases, as not all combinations of types and assumptions need to be considered. This means the proposed algorithm also brings us closer to implementing the combination of SHACL with ontologies. We are confident that the proposed techniques can most likely be optimised further, but leave this for future work. To keep the presentation simple we focused on semi-positive SHACL in this paper, but we note that the rewriting presented in the last section can be extended to SHACL with stratified negation following the ideas of [15].
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.
This work was also partially supported by the Austrian Science Fund (FWF) project P30873. in: Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, AAAI Press, 2022, pp. 5626–5633. [15] S. Ahmetaj, M. Ortiz, A. Oudshoorn, M. Šimkus, Reconciling shacl and ontologies: Semantics and validation via rewriting, in: ECAI 2023, IOS Press, 2023, pp. 27–35. [16] W3C, Shape constraint language (SHACL), Technical Report. (2017). https://www.w3.org/TR/shacl. [17] J. Corman, J. L. Reutter, O. Savkovic, Semantics and validation of recursive SHACL, in: D. Vrandecic, K. Bontcheva, M. C. Suárez-Figueroa, V. Presutti, I. Celino, M. Sabou, L. Kafee, E. Simperl (Eds.), The Semantic Web - ISWC 2018 - 17th International Semantic Web Conference, Monterey, CA, USA, October 8-12, 2018, Proceedings, Part I, volume 11136 of Lecture Notes in Computer Science, Springer, 2018, pp. 318–336. [18] M. Andresel, J. Corman, M. Ortiz, J. L. Reutter, O. Savkovic, M. Šimkus, Stable model semantics for recursive SHACL, in: Proc. of The Web Conference 2020, ACM, 2020, p. 1570–1580. [19] P. Pareti, G. Konstantinidis, F. Mogavero, Satisfiability and containment of recursive SHACL,
Journal of Web Semantics 74 (2022) 100721. [20] B. Bogaerts, M. Jakubowski, J. Van den Bussche, SHACL: A description logic in disguise, in:
Proc. of LPNMR 2022, volume 13416 of Lecture Notes in Computer Science, Springer, 2022, pp. 75–88. [21] P. Hell, J. Nesetril, The core of a graph, Discret. Math. 109 (1992) 117–126. [22] D. Carral, M. Krötzsch, M. Marx, A. Ozaki, S. Rudolph, Preserving constraints with the stable chase, in: B. Kimelfeld, Y. Amsterdamer (Eds.), 21st International Conference on Database Theory, ICDT 2018, March 26-29, 2018, Vienna, Austria, volume 98 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, pp. 12:1–12:19. [23] M. Krötzsch, Computing cores for existential rules with the standard chase and ASP, in: D. Calvanese, E. Erdem, M. Thielscher (Eds.), Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, Rhodes, Greece, September 12-18, 2020, 2020, pp. 603–613. [24] J. Hromkovic, S. Seibert, T. Wilke, Translating regular expressions into small -free nondeterministic finite automata, J. Comput. Syst. Sci. 62 (2001) 565–588.