Attributed Description Logics: Reasoning on Knowledge Graphs

1 Introduction

Description logics (DLs) can express complex schema information on graph-like models, while supporting incomplete information via the open world assumption. While OWL is often used in RDF-based knowledge graphs developed in academia, such as DBpedia [Bizer et al., 2009] and Bio2RDF [Belleau et al., 2008], it has almost no impact on other applications of graph-structured data. This might in part be due to a format mismatch. Like DLs, many knowledge graphs use directed, labelled graph models, but unlike DLs they often add (sets of) annotations to vertices and edges. For example, the fact that Lise Meitner received the Max Planck Medal can be described by an assertion awarded"meitner; planck_medal", but in practice we may also wish to record the year and the location. We may write this as follows:

awarded"meitner; planck_medal"@[year:1949; loc:berlin]:

Such annotated graph edges today are widespread in practice. Prominent representatives include Property Graph, the data model used in many graph databases [Rodriguez and Neubauer, 2010], and Wikidata, the knowledge graph used by Wikipedia [Vrandečić and Krötzsch, 2014]. One can encode annotated (multi-)graphs as directed graphs, e.g., using reification [Erxleben et al., 2014], but DLs cannot express much over such models. For example, one cannot say that the spouse relation is symmetric, where annotations are the same in both directions [Marx et al., 2017]. Other traditional KR formalisms are similarly challenged in this situation.

� This invited contribution to IJCAI 2018 summarises and discusses results of our previous ISWC 2017 paper "Attributed description logics: Ontologies for knowledge graphs" [Krötzsch et al., 2017].

In a recent work, we have therefore proposed to develop logics that support sets of attribute-value annotations natively [Marx et al., 2017]. The according generalisation of firstorder logic, called multi-attribute predicate logic (MAPL), is expressive enough to capture weak second-order logic, making reasoning non-semi-decidable. For that reason, we have developed the Datalog-like MAPL rule language (MARPL) as a decidable fragment.

In this paper, we explore the use of DLs as a basis for decidable, and even tractable, fragments of MAPL. The resulting family of attributed DLs allows statements such as spouse@X v spouse � @X to say that spouse is symmetric; spouse � denotes the inverse spouse relation. We introduce set variables (X in the example) to refer to annotations. References to variables are used to express constraints over annotations and to compare attribute values between them. A challenge is to add functionality of this type without giving up the nature of a DL, i.e., without sacrificing the variable-free notation of DLs in favour of rule languages. Another challenge is that these extensions may greatly increase the complexity of DLs.

We show that reasoning for attributed ELH, a DL close to OWL 2 EL, is ExpTime-complete, and identify syntactic constraints under which we recover the PTime-completeness of ELH. We also establish complexity results for the attributed variant of the prototypical DL ALCH: reasoning is 2ExpTime-complete in general, and ExpTime-complete under our syntactic constraints. Finally, we show that reasoning is N2ExpTime-complete for attributed SROIQ, the DL underlying OWL 2 DL. Additional proofs can be found in [Krötzsch et al., 2017].

2 Attributed Description Logics

We introduce attributed description logics by defining the syntax and semantics of attributed ALCH, denoted ALCH@. This allows us to illustrate the central ideas without having to deal with the full generality of SROIQ, which we introduce in Section 4. We note that fact entailment can be polynomially reduced to satisfiability checking in the DLs we study.

2.1 Syntax and Intuition

We first give the syntax and intuitive semantics of ALCH@; the semantics will be formalised thereafter.

Example 1 We start with a guiding example, which will be formally explained when we define ALCH@. Wikidata contains assertions of the form:

awarded"a_person; an_award"@[year : a_year; url : a_url]:

This motivates the following ALCH@ axiom.

The underlying DL axiom 9awarded:Award v 9known_for:> states that anybody who received an award is known for some achievement.

Attributed DLs are defined over the usual DL signature with sets of concept names NC, role names NR, and individual names NI. In OWL terminology, concepts correspond to classes, roles correspond to properties, and individual names correspond to individuals. We consider an additional set NV of (set) variables. Following the definition of multi-attributed predicate logic (MAPL, [Marx et al., 2017]), we define annotation sets as finite binary relations, understood as sets of attribute-value pairs. In particular, attributes refer to domain elements and are syntactically denoted by individual names. To describe annotation sets, we introduce specifiers. The set S of specifiers contains the following expressions:

• set variables X 2 NV;
• closed specifiers [a1 : v1; : : : ; an : vn]; and
• open specifiers ba1 : v1; : : : ; an : vnc,

where ai 2 NI and vi is either an individual name in NI or an expression of the form X:c, with X a set variable in NV and c an individual name in NI. Intuitively, closed specifiers define specific annotation sets whereas open specifiers merely provide lower bounds. A ground specifier is a specifier that does not contain expressions of the form X:c.

Example 2 The open specifier byear:X:yearc in Example 1 describes all those annotation sets that contain at least every attribute-value pair with attribute year that occurs in X.

The set R of ALCH@ role expressions contains all expressions r@S with r 2 NR and S 2 S. The set C of ALCH@ concept expressions is defined as follows.

An ALCH@ concept (or role) assertion is an expression A"a"@S (or r"a; b"@S), with A 2 NC (or r 2 NR), a; b 2 NI, and S 2 S a specifier that is not a set variable. An ALCH@ concept inclusion is an expression of the form

where S1; : : : ; Sn 2 S are specifiers, C; D 2 C are ALCH@ concept expressions, and X1; : : : ; Xn 2 NV are set variables occurring in C; D or in S1; : : : ; Sn. ALCH@ role inclusions are defined analogously, but with role expressions instead of the concept expressions. An ALCH@ ontology is a set of ALCH@ assertions, and role and concept inclusions.

Example 3 Let � be the concept inclusion (1) from Example 1. Using a specifier for X, we can restrict the applicability of this axiom, e.g., to prizes awarded by the Nobel Foundation:

To simplify notation, we omit the specifier bc (meaning "any annotation set") in role or concept expressions, as done for Award in Example 1. In this sense, any ALCH@ axiom is also an ALCH axiom. We also omit prefixes of the form X : bc, allowing X to be any annotation set, as done in (1).

We follow the usual DL notation for referring to other attributed DLs. In particular, ELH@ is the fragment of ALCH@ which disallows negation.

2.2 Formal Semantics

An interpretation I = h�I; �I i of attributed logic consists of a non-empty domain �I and a function �I . Individual names a 2 NI are interpreted as elements aI 2 �I . To interpret annotation sets, we use the set �I B f� � �I � �I j � is finiteg of all finite binary relations over �I . Now each concept name C 2 NC is interpreted as a set CI � �I ��I of elements with annotations, and each role name r 2 NR is interpreted as a set r I � �I � �I � �I of pairs of elements with annotations. Note that each element (pair of elements) may appear with multiple different annotations.

Expressions with free set variables are interpreted using variable assignments Z : NV ! �I . A specifier S 2 S is interpreted as a set SI;Z � �I of matching annotation sets. We set X I;Z B fZ"X"g for variables X 2 NV. The semantics of closed specifiers is defined as follows:

• (ii) [a : X:b] I;Z B ffhaI; �i j hbI; �i 2 Z"X"gg

SI;Z therefore is a singleton set for variables and closed specifiers. For open specifiers, however, we define ba1 : v1; : : : ; an : vnc I;Z to be the set

Now, given A 2 NC, r 2 NR, and S 2 S, we define:

Further DL expressions are defined as usual: >I;Z = �I , :CI;Z = �I n CI;Z , "C u D"I;Z = CI;Z \ DI;Z , and "9R:C"I;Z = f� j there is h�; �i 2 RI;Z with � 2 CI;Z g.

Now I satisfies an ALCH@ concept inclusion � of the form (2), written I j= �, if, for all variable assignments Z such that Z"Xi" 2 SI;Z i for all i 2 f1 ; : : : ; ng, we have CI;Z � DI;Z . Satisfaction of role inclusions is defined analogously. Moreover, I satisfies an ALCH@ concept assertion A"a"@S if haI; �i 2 AI for some � 2 SI (the latter is well-defined since S contains no variables), and likewise for role assertions. I satisfies an ontology if it satisfies all of its axioms. Based on this model theory, logical entailment is defined as usual.

Example 4 Consider the concept inclusion � of Example 1 and the following interpretation I over domain �I = fmeitner; planck_medal; 1949; year; nuclear_fissiong with

awardedI = fhmeitner; planck_medal;fhyear;1949igig; and

known_forI = fhmeitner; nuclear_fission; fhyear; 1949igig:

Then I j= �, i.e., I satisfies �.

3 Tractable Reasoning in Attributed ELH

We now introduce the two central reasoning techniques for attributed DLs: grounding eliminates set variables from an attributed ontology, and renaming constructs an equisatisfiable ontology in the underlying non-attributed DL.

Let KB be a ground ELH@ ontology, i.e., an ELH@ ontology that does not contain set variables. We translate KB into an ELH ontology KB y by replacing every concept expression A@S with A 2 NC and S 2 S occurring in KB by a fresh concept name AS, and similarly for role expressions r@S. To capture the interactions between specifiers such as [a : b] and bc, we extend KB y by concept and role inclusion axioms AS v AT and rS v rT , respectively, where AS and AT (or rS and rT , respectively) occur in KB y and T is an open specifier subsuming the (open or closed) specifier S, i.e., S contains all attribute-value pairs a : b in T.

Then KB y is polynomial in the size of KB, and together with the PTime-completeness of ELH [Baader et al., 2005], we obtain the following theorem.

Theorem 1 Let KB be a ground ELH@ ontology. Checking satisfiability of KB is PTime-complete.

For a general ELH@ ontology KB, the grounding ground"KB" is the ground ELH@ ontology consisting of all the assertions of KB, and, for each inclusion axiom X1 :S1; : : : ; Xn :Sn "C v D" by all possible ground instances C 0 v D 0 : concept expressions A@Xi are replaced by A@Ti, where Ti is some specifier subsumed by Si , and assignments a : Xi :b are replaced by all assignments a : c such that b : c occurs in Ti. Role inclusion axioms are treated analogously.

In general, there may be exponentially many ground instances of a single inclusion axiom. Yet, tractable reasoning in ELH@ is possible under further restrictions, as the next theorem shows.

Theorem 2 Let '; k 2 N, and let KB be an ELH@ ontology satisfying all of the following conditions:

• (A) each axiom of KB contains at most ' set variables,
• (B) each specifier occurring in KB contains at most k expressions of the form X:a, and,
• (C) if a specifier S contains an assignment a : X:b, no further assignment for the same attribute a occurs in S.

Then checking satisfiability of KB is PTime-complete.

Together, these conditions guarantee that the grounding ground"KB" remains polynomial in the size of KB. Indeed, relaxing any of the conditions immediately yields intractability.

Theorem 3 Let KB be an ELH@ ontology and consider conditions (A)-(C) of Theorem 2 with ' = 1 and k = 2. Then deciding satisfiability of KB is

1. ExpTime-complete if KB violates only condition (A),
2. ExpTime-complete if KB violates only condition (B), and
3. PSpace-hard if KB violates only condition (C).

It remains open whether the PSpace-bound in the third case is tight. Nevertheless, reasoning in this case is intractable.

The same pattern repeats for more expressive DLs: satisfiability of ground ontologies retains the complexity of the underlying non-attributed DL, and the grounding technique results in an exponentially larger ontology.

Theorem 4 Consider conditions (A)-(C) of Theorem 2. Checking satisfiability of an ALCH@ ontology KB is

1. ExpTime-complete if KB is ground,
2. ExpTime-complete if KB satisfies conditions (A)-(C), and
3. 2ExpTime-complete in general.

4 Attributed SROIQ

SROIQ extends ALCH with nominals fcg (concepts with just one individual), number restrictions 6n R:C and >n R:C (bounding the number of R-successors in C), inverse roles r � , and generalised role inclusions R � S v T (generalising transitivity). Since axioms such as fcg � Ac@bc can be used to introduce a concept name Ac for any nonimal c, we do not add annotations on nominals. This allows us to reuse the notion of interpretation fromALCH@. We lift the definitions of assertions, and of concept and role inclusions by extending them to include the new constructors. Furthermore, SROIQ@ allows complex role inclusion axioms of the following form:

where Ri; T 2 R are SROIQ@ role expressions, S1; : : : ; Sn 2 S are specifiers, and X1; : : : ; Xn 2 NV are set variables occurring in Ri; T; S1; : : : ; Sn. As before, a SROIQ@ ontology is a set consisting of SROIQ@ assertions, and of role and concept inclusion axioms. We extend the usual semantics [Horrocks et al., 2006] to SROIQ@ as for ALCH@ by accounting for annotations in the interpretation of concepts and roles.

Example 5 SROIQ can express multiplicities of relations, e.g., to state that an award with more than one recipient in one particular year is a shared award for this year:

>2awarded � @X:> v Shared_Award@byear : X:yearc:

The following example uses a nominal (without annotations, as explained above):

9awarded � @bconferred_by : nobel_foundation;

This can be viewed as an annotation-dependent range restriction axiom, in this case defining the range of awarded to be a singleton class.

SROIQ ensures decidability of reasoning by imposing two additional restrictions on ontologies - simplicity and regularity [Horrocks et al., 2006] - which we adapt to SROIQ@. Simple roles are defined as in SROIQ, ignoring all annotations. They are the only roles that may appear in the role expressions of number restrictions. A SROIQ@ ontology is regular if the set N � R = NR [ fr � j r 2 NRg can be ordered by a strict partial order � such that

1. the inclusion R1 � � � � � R' v T in each complex role inclusion axiom (4) is of one of the following forms:

where S 2 S, t 2 N � R , r 2 NR, and R1; : : : ; R' 2 R are of the form r1@S1; : : : ; r'@S' with ri � t for all 1 � i � '.

In addition to adopting the usual conditions from SROIQ for (inverted) role names, we also require that, whenever the same role name occurs on both sides of the inclusion, also the specifiers are the same in both cases. Regularity can be verified in polynomial time by computing a minimal relation � satisfying the conditions and then checking whether � is a strict partial order.

In regards to reasoning, the new features of SROIQ@ over ALCH@ lead to several difficulties. In the presence of nominals and number restrictions, equalities a � b of individuals may be entailed. In turn, this leads to equalities of annotation sets, e.g., A@bc : ac � A@bc : bc. Furthermore, nominals can be used to bound the overall size of the domain, e.g., by stating > v fag. This gives rise to further equalities, but, more importantly, it also affects the semantics of open specifiers (e.g., we then have A@ba : ac v A@[a : a]).

Our translation of SROIQ@ ontologies thus requires further axioms to handle these two effects. A naive translation, however, requires exponentially many auxiliary axioms to handle either of them, which would lead to an N3ExpTime upper bound even for ground SROIQ@. Instead, we use an auxiliary DL SROIQ�, which allows for a more concise translation. SROIQ� can in turn be reduced to C 2 , the twovariable fragment with counting [Pratt-Hartmann, 2005], in exponential time, which yields an N2ExpTime upper bound for ground SROIQ@. Even though the grounding of a SROIQ@ ontology still results in an exponentially larger ontology, this does not increase the complexity any further.

Besides standard SROIQ axioms, SROIQ� also supports concept inclusion of the form a � b ) C v D and role inclusions of the form a � b ) R1 � � � � � R' v T. An interpretation I satisfies such an axiom a � b ) � when either aI , bI or I j= �. In translating a ground SROIQ@ ontology KB into a SROIQ� ontology KB z , we proceed as before, but introduce names AS 2 NC and rS 2 NR for all possible open and closed specifiers over the individual names occurring in KB. Then, to handle equality, for every A 2 NC, we add axioms a � b ) AS v AT for all pairs S; T of distinct ground specifiers that are either both open or both closed, and where S and T are the same when replacing every occurrence of a by b. We add similar axioms for each role name r 2 NR.

To deal with the bounded domain size, we use an individual name z not occurring in KB as a canary: equalities of the form z � a allow us to detect the bounded domain case. We let N KB I be the set of all individual names in KB, and add, for each a; b; c 2 N KB I and all A 2 NC and all r 2 NR in KB, axioms

where S is a ground open specifier and T �c S means that T is a ground closed specifier subsuming S. Intuitively, (7) states that any fact rS"b; c" entails some fact of the form rT "b; c".

Together with the auxiliary axioms from the ALCH@ translation, we obtain KB z , an equisatisfiable SROIQ� ontology. The construction can be performed in exponential time.

The grounding technique does not increase the �-depth of the ontology KB, and the above translation of ground SROIQ@ ontologies into SROIQ� is polynomial in the number of possible ground annotation sets. Thus, we find that ground"KB" z is still only exponentially larger than KB, even for non-ground SROIQ@ ontologies. Together with the bounded �-depth, we thus obtain an N2ExpTime upper bound.

Theorem 5 Checking satisfiability of SROIQ@ ontologies is N2ExpTime-complete.

5 Discussion and Outlook

Current graph-based knowledge representation formalisms suffer from an inability to handle meta-data in the form of sets of attribute-value pairs. These limitations show up even when dealing with purely abstract data and are orthogonal to datatype support in the formalisms. Our family of attributed description logics approaches the problem in the context of DLs. We have presented a grounding-based decision procedure and identified the special cases of ground ontologies and structural restrictions on axioms, for which this overhead can be avoided. Those restrictions ensure tractability of attributed EL.

Related approaches. Our goal was to bring features of the recent attributed rule language MARPL to DLs [Marx et al., 2017]. In practice, further rule-like expressivity is probably needed, and DL-rule extensions should be considered. Our grounding approach naturally fits to DL-safe rules [Motik et al., 2005] and nominal schemas [Krötzsch et al., 2011], but many other DL-rule mergers exist. We are not aware of any other extension of DL to property graphs. However, DLR+ , a recent extension of DLR [Calvanese et al., 2008], extends DL to relational data models [Artale et al., 2017]. Our annotation sets can be encoded in DLR+ using auxiliary relations (just like in RDF), but it remains open how the expressive powers compare under such an encoding. Semiring semantics can also express certain "annotations" [Green et al., 2007], e.g., in annotated RDF [Straccia et al., 2010]. Many approaches could be re-phrased using semirings, but this yields neither a concrete syntax nor specific insights, e.g., on decidability and complexity.

Outlook. We are currently working on developing reasoning support for attributed logics. A variant of MARPL rules is used in ontological modelling for Wikidata; inferred facts are shown in the SQID data browser (https://tools.wmflabs.org/sqid/, [Marx and Krötzsch, 2017]). This rule language was extended with expressions of the form X:a, introduced herein. Future research will be necessary to design attributed logics with the right level of expressivity for such applications, and to develop general-purpose reasoning tools to fully support them.

Acknowledgements

This work is partly supported by the German Research Foundation (DFG) within the Cluster of Excellence "Center for Advancing Electronics Dresden" (cfaed), the Collaborative Research Center SFB 912 (HAEC), and in Emmy Noether grant KR 4381/1-1 (DIAMOND).