Logic on MARS: Ontologies for Generalised Property Graphs

1 Introduction

The representation of human knowledge in its variety and complexity is a central topic of AI. Recently, graph-based representation formats have led to huge advances in the field of data modelling. So-called Knowledge Graphs (KGs) are now widely used to capture heterogeneous, multi-faceted knowledge from different sources in a coherent way. Large KGs are deployed in companies such as Google and Facebook, in online communities such as Freebase [Bollacker et al., 2008] and Wikidata [Vrandečić and Krötzsch, 2014], and in research projects such as YAGO2 [Hoffart et al., 2013].

There is no standard definition of what constitutes a KG, and the formats used in practice vary. The basis of KGs typically are directed graphs with labelled nodes and edges. What distinguishes them from plain graphs is their enriched structure that includes additional annotations to provide contextual information for every edge or node. Examples include provenance (source information) and temporal validity, but there can be many other types of annotations.

A popular data model for such KGs is the Property Graph model, used by the Neo4J graph database [Rodriguez and Neubauer, 2010] and various other database applications [Rudolf et al., 2013]. It allows sets of attribute-value pairs to be associated with the nodes and edges in a directed graph. For example, we can express that Liz Taylor married Richard Burton 1964 in Montreal, and that the marriage ended in 1974 by annotating the fact (or edge) spouse"taylor; burton" with the annotation fstart : 1964 ; loc : Montreal; end : 1974g.Wewrite the annotated fact as spouse"taylor; burton"@fstart : 1964 ; loc : Montreal; end : 1974g. Such graphs are also known as attributed graphs. This model is fundamentally different from annotated logics, e.g., using semiring annotations [Green et al., 2007; Straccia et al., 2010] or requiring functional annotations like aRDF [Udrea et al., 2010], since the same edge may occur with several, distinct annotations (e.g., Taylor was also married to Burton from 1975 to 1976). Wikidata's custom data model supports attributed statements too, but goes beyond Property Graph by allowing attributes with multiple values. Wikidata includes, e.g., the fact castMember"Sesame_Street; Frank_Oz" with annotation frole : Cookie_Monster; role : Grover; role : Bertg.1 We call such generalised Property Graphs multi-attributed graphs.

In spite of the huge practical significance of these data models and the obvious potential of KGs for AI, there is practically no support for using such data in knowledge representation. The popular ontology language OWL focusses on labelled directed graphs as defined by RDF [OWL Working Group, 2009]. Rule languages as in logic programming support predicates of higher arities, but bounded arity relations cannot encode arbitrary sets of attribute-value pairs either. Indeed, we might want to express schema knowledge as sketched by the following rule:

which states that spouse is a symmetric relation, where the inverse statement has the same start and end dates, and location. To the best of our knowledge, this cannot be encoded in any modern ontology language. Yet there are many more complex relationships that one might want to express. In fact, even the underlying data model of a multi-attributed graph lacks proper formalisation. Property Graph and Wikidata are highly implementation bound and have no formal specification. Other approaches, e.g., YAGO2 annotated triples, lack generality.

1https://www.wikidata.org/wiki/Q155629 (retr. 2017-02-17)

In this paper, we therefore propose a new, formal data model for generalised Property Graphs, called multi-attributed relational structure (MARS), and we develop a logical language, called multi-attributed predicate logic (MAPL), for modelling knowledge over such structures. Our main contributions are as follows:

• we provide a logical foundation for knowledge modelling over Property Graphs,
• we study the expressive power of MAPL and show that it has no sound and complete deduction calculus,
• we identify two expressive features of MAPL that are useful for modelling,
• we suggest a rule-based fragment of MAPL, called MARPL, for which reasoning is decidable, and
• we give a reasoning procedure for MARPL.

For reasoning in MARPL, we obtain an ExpTime complexity bound, which we show to be tight even if only the underlying facts (corresponding to the input KG) are allowed to vary. This unusually high data complexity illustrates the added power of our approach as compared to traditional rule languages such as Datalog. Under a reasonable assumption (bounding the size of annotations), data complexity drops back to polynomial time.

For now, we treat the annotations as opaque; we do not aim at providing specialty reasoning services for certain datatypes such as time, numbers, coordinates, or provenance information. As each datatype suggests different bodies of related work, we refrain from going into detail.

Our presentation is self-contained, but some proofs are omitted for reasons of space. Readers may consult an extended report if further details are desired [Marx et al., 2017].

2 Multi-Attributed Relational Structures

We now formalise our notion of a generalised Property Graph, and we use it as the basis for the model theory of a suitably enhanced predicate logic.

We consider a finite set P of predicates, where each p 2 P has an associated arity ar"p" � 0. If not otherwise stated, we assume this signature to be fixed and refrain from mentioning it. For the following definition, let Pfin "S" be the set of all finite subsets of set S.

Definition 1. A multi-attributed relational structure (MARS) M consists of a non-empty set � M of domain elements and, for each n-ary predicate p 2 P, an "n + 1"-ary relation p M � "� M " n � Pfin � � M � � M � .

In other words, a MARS behaves like a relational structure (i.e., hypergraph) over a domain � M , where each relation tuple (i.e., hyperedge) is annotated with a finite binary relation over � M . We view this relation as a set of attribute-value pairs. There might be multiple values for each attribute, justifying our terminology. Also note that the same relational tuple may occur with different attribute-value collections within a single MARS. Thus MARS generalise Property Graphs, where attributes are functional and relations are unary and binary. The unary relations can be used to assign attribute-value collections to nodes.

To represent schematic knowledge on (generalised) Property Graphs, we introduce logical formulae with an additional set-valued parameter for each predicate, representing attribute-value pairs. In addition to the set of predicates P, such logical expressions are based on a set C of constant symbols, a set V of object variables and a set U of set variables.

Definition 2. An object term is a symbol t 2 C [ V. A set term is either a variable U 2 U or an expression of the form fa1 : b1; : : : ; an : bng for n � 0, where ai; bi are object terms for all i 2 f1 ; : : : ; ng.

The formulae of multi-attributed predicate logic (MAPL) are defined as follows. A relational atom is an expression p"t1; : : : ; tn"@S where p 2 P is an n-ary predicate, t1; : : : ; tn are object terms, and S is a set term. A set atom is an expression "a : b" 2 S, where a; b are object terms and S is a set term. An atom is a relational atom or set atom. The set of MAPL formulae is inductively defined to contain all atoms and all formulae of the form '1 ^ '2, :', 9x:' and 9U:', where '"i" are MAPL formulae, x 2 V and U 2 U. We define the shortcuts _, !, and 8 in the usual way.

Example 1. (1) is a MAPL formula that works on spouse statements with start, loc, and end attributes. It does not apply to marriages missing loc, but the location may not be known for all spouse statements. To support optional attributes, we first define a shortcut '»X;Y…, where X and Y might be arbitrary set variables, to be the following formula:

The formula �»X;Y… = '»X;Y… ^ 8W: 8x; y:"'»X;W… ^ "x : y" 2 Y" ! "x : y" 2 W then expresses that Y is the least set that contains the same start, loc, and end values as X, i.e., Y does not contain any other attributes. Using this conditional copying of attributes, we can improve (1):

The semantics of MAPL formulae is defined in the natural way by using MARS as the basis for the model theory, i.e., by switching from standard relational structures to MARS in logical interpretations. We first define our interpretation of (object and set) terms. We make a unique name assumption (UNA), since this is more natural for working with large knowledge graphs (which are similar to databases). The UNA is particularly useful when formulating meaningful conditions on finite annotations, as discussed in Section 3.

Definition 3. A MAPL interpretation I is a MARS, which in addition maps each constant c 2 C injectively to an element c I 2 � I (UNA). A MAPL variable assignment for I is a function Z that maps object variables x 2 V to elements Z"x" 2 � I and set variables U 2 U to finite binary relations Z"U" 2 Pfin � � I �� I � .

For an object term t, we define t I;Z B t I if t 2 C and t I;Z B Z"t" if t 2 V. For a set variable U 2 U, we define U I;Z B Z"U" . For a set term S = fa1 : b1; : : : ; an : bng, we define S I;Z B fha I;Z 1 ; b I;Z 1 i; : : : ; ha I;Z n ; b I;Z n ig.

Definition 4. An interpretation I and a variable assignment Z for I may satisfy a formula ', written I;Z j= '. This is defined recursively as follows:

• I;Z j= p"t1; : : : ; tn"@S if ht I;Z 1 ; : : : ; t I;Z n ; S I;Z i 2 p I ,
• I;Z j= "a : b" 2 S if ha I;Z ; b I;Z i 2 S I;Z ,
• I;Z j= "'1 ^ '2" if I;Z j= '1 and I;Z j= '2,
• I;Z j= :' if I;Z6 j= ' I ,
• I;Z j= 9x:' if there is � 2 � I such that I;Zjx7 !� j= ',
• I;Z j= 9U:' if there is R 2 Pfin � � I �� I � such that I; ZjU7 !R j= ',

where ZjX7 !V denotes the assignment Z modified to map X to V. We may omit Z for formulae without free variables (sentences), writing I j= '; in this case, I is a model of '.

As usual, we say that a variable-free MAPL formula is satisfiable if it has a model. A variable-free formula ' entails , written ' j= , if all models of ' are also models of . We extend all of these notions to sets of formulae as usual.

Unfortunately, as the next theorem shows, MAPL is already too powerful for practical applications. Recall that weak second-order logic (WSO) is a second-order logic that allows set quantifiers to range over finite sets only [Leivant, 1994]. In spite of this restriction, there is no sound and complete calculus for WSO, even without built-in equality.

Theorem1. Satisfiability of a sentence of weak second-order logic can be polynomially reduced to satisfiability of a MAPL sentence. In particular, satisfiability for MAPL is not semidecidable (and therefore not decidable).

Proof. MAPL uses the same connectives as WSO, but further restricts second-order quantification to binary predicate variables. We translate WSO formulae ' into equisatisfiable MAPL formulae 'MAPL. For a k-ary second-order variable X, let X1; : : : ; Xk be fresh set variables. If ' = p"t1; : : : ; tn" is a first-order atom, then 'MAPL B p"t1; : : : ; tn"@fg. If ' = X"t1; : : : ; tk" is a second-order atom, then

If ' = 9X: for a second-order variable X, then 'MAPL B 9X1; : : : ; Xk : MAPL. If ' = 9x: for a first-order variable x, then 'MAPL B 9x: MAPL. Likewise, ": "MAPL B : MAPL and " ^ 0 "MAPL B MAPL ^ 0 MAPL . �

3 Towards a Decidable Fragment of MAPL

Theorem 1 shows that MAPL is hardly suitable as an ontology language, since automated, fully unsupervised processing can access logically entailed information only in incomplete ways. Our goal is to identify a decidable fragment of MAPL that is suitable for speaking about Property Graphs and related structures. In this section, we introduce several practically useful expressive features that MAPL can provide, and that will play an important role in the definition of this fragment.

An important class of formulae are those that can express conditions on attribute-value sets, which we call specifiers. For example, we will allow formulae such as »start : �; loc : Montreal…"U" to state that U is an annotation that contains zero or more values for attribute start, the value Montreal for attribute loc, and no other attributes. We show that this and many other specifiers can be expressed in MAPL.

Definition 5. A closed specifier is an expression of the form »a1 : b1; : : : ; an : bn… where n � 0, ai are object terms, and bi are either object terms or one of the special symbols � and +. For interpretation I and variable assignment Z, define:

• »a : b… I;Z B ffa : bg I;Z g if b < f�; +g,
• »a : �… I;Z as the set of all finite binary relations of form fha I;Z ; �1i; : : : ; ha I;Z ; �'ig with ' � 0 and �i 2 � I ,
• »a : +… I;Z as the set of all finite binary relations of form fha I;Z ; �1i; : : : ; ha I;Z ; �'ig with ' � 1 and �i 2 � I ,
• »a1 : b1; : : : ; an : bn… I;Z B n - n i=1 Si j Si 2 »ai : bi… I;Z o .

Example 2. Consider � B »start : �; loc : Montreal…, the closed specifier from the motivating example above. Then given any interpretation I, we have floc : Montrealg I 2 � I and fstart : 1964 ; loc : Montrealg I 2 � I , but fstart : 1964 ; loc : Montreal; end : 1974g I < � I .

Closed specifiers allow us to describe annotations that use only certain "expected" attributes, which is useful in the open, schema-less world of knowledge graphs, where attributes may be reused in different contexts. However, it is also useful to consider open specifiers, which characterise the set of all supersets of a given annotation:

Definition 6. An open specifier is an expression of the form � = ba1 : b1; : : : ; an : bnc where n � 0, ai are object terms, and bi are either object terms or one of the special symbols � and +. Given an interpretation I and a variable assignment Z, we define � I;Z to be the set � S 2 Pfin � � I �� I � j S � T for some T 2 ¯� I;Z � where ¯� is the corresponding closed specifier »a1 : b1;: : :; an : bn….

Example 3. The open specifier bstart : +; loc : Montrealc characterises annotations that have at least one value for start and a loc attribute with value Montreal, e.g., for any interpretationI, we have fstart : 1964 ; loc : Montreal; end : 1974g I 2 bstart : +; loc : Montrealc I .

It is natural to define set operations on specifiers. For example, the union bloc : Montrealc [ bloc : Perthc describes annotations with (at least) one of two possible values for loc.

Definition 7. A specifier � is a term built from open and closed specifiers using the (binary) operators \; [ , and n . The semantics are extended in the natural way, e.g., "�1 \�2" I;Z B � I;Z 1 \ � I;Z 2 . A specifier atom is an expression �"S", where � is a specifier and S is a set variable.

Example 4. Note that specifiers may use object variables. The following specifier defines annotations that give at least a start date x and a location y, but no end date:

We may treat arbitrary specifiers as syntactic sugar:

Theorem 2. For every specifier �, there is a MAPL formula '�»U… with a set variable U such that, for all interpretations I, variable assignments Z, and relations R 2 Pfin � � I � � I � , we have R 2 � I;Z iff I; ZjU7 !R j= '�.

Example 5. Along the lines of Example 4, we can define the current spouse of a person:

This is an important pattern that, in spite of the use of start and end times in our example, is fundamentally different from typical patterns in logics with temporal validity annotations.

Specifiers can express conditions on attribute-value sets. For ontological modelling, it is further useful to construct new attribute-value sets that are used to annotate newly derived facts. For instance, we have constructed a set V with optional parts in Example 1. We want enough power to define interesting types of functions, which compute new annotation sets by evaluating conditions on their input.

Definition 8. Let F denote a set of function symbols. A function definition hF; S; Ci consists of a symbol F 2 F, a signature S that is a list of distinct variables from V[U, and a set C of conditionals of the following form:

where n � 0, all 'i are MAPL set atoms or specifier atoms, m � 1, and all aj; bj are object terms. The part left of ) is the precondition and the part right of ) is the action. We require: (a) all set variables in the precondition must occur in the signature S; and (b) all variables in the action occur either in the precondition or in the signature S.

A function term for hF; S; Ci is an expression F"t", where t is a list of MAPL terms of length j t j = jSj, so that ti is an object term if Si is an object variable, and a set term otherwise. For an interpretation I and variable assignment Z, we define F"t" I;Z to be the least set of attribute-value pairs such that, for each conditional of form (6) in C and all variable assignments Z 0 satisfying Z 0 "Si" = t I;Z i for all i 2 f1 ; : : : ; jSjg, if I;Z 0 j= '1 ^ : : : ^ 'n then ha I;Z 0 j ; b I;Z 0 j i 2 F"t" I;Z for all j 2 f1 ; : : : ; mg. We consider the empty conjunction to be vacuously satisfied in case n = 0.

In words, the set F"t " I; Z simply contains all attribute-value pairs that are entailed by some conditional of F.

Example 6. Making a copy of optional attribute-value pairs as realised by the formula �»X;Y… in Example 1 can be expressed with a function definition hCopy; hUi; Ci with C consisting of the following conditionals:

bstart : z1c"U" ) insert"start : z1" bloc : z2c"U" ) insert"loc : z2" bend : z3c"U" ) insert"end : z3"

Example 7. We can define binary functions that compute set operations on two annotations sets U and V. Union is captured with two conditionals bx : yc"U" ) insert"x : y" and bx : yc"V" ) insert"x : y". Intersection can be expressed by one conditonal bx : yc"U"; bx : yc"V" ) insert"x : y". Set difference is defined using a single conditional

bx : yc"U"; � bc n bx : y c � "V" ) insert"x : y":

Arguably, such operations on annotations are essential when defining ontological relations on knowledge graphs. The next result confirms that this can be captured in MAPL.

Theorem 3. For every function definition hF; S; Ci and corresponding function term F"t", there is a MAPL formula 'F"t"»U… with a set variable U such that, for all interpretations I, variable assignments Z, and relations R 2 Pfin � � I � � I � , we have I; ZjU7 !R j= 'F"t" iff R = F"t" I;Z .

Theorem 3 allows us to use function terms for annotations within MAPL theories. A relational atom of the form p"a1; : : : ; an"@F"t" can be considered as an abbreviation for 9U:p"a1; : : : ; an"@U ^ 'F"t"»U…, and similarly for set atoms.

Example 8. With the function definition hCopy; hUi; Ci of Example 6, formula (3) of Example 1 can be written as

8x; y: 8U:spouse"x; y"@U ! spouse"y; x"@Copy"U" (7)

4 MAPL Rules

We now introduce a rule-based fragment of MAPL, where rules are allowed to contain arbitrary specifiers. While still giving us high expressivity, this is sufficient to obtain decidability for fact entailment.

Definition 9. A MAPL rule is a MAPL formula of the form 8U: 8x:"' ! ", where ' is a conjunction of MAPL atoms and specifier atoms; is a relational MAPL atom that may use a function term; and U and x are lists of all set and object variables, respectively, that occur in ' or . We further require that every set variable or set term fa1 : b1; : : : ; a' : b' g containing object variables must occur in some relational atom in ', and that all variables in occur in '.

We will tacitly omit the universal quantifiers, and call ' body and head of the rule. A fact is a rule where the body ' is an empty conjunction (interpreted as true).

An ontology of multi-attributed rule-based predicate logic (MARPL) consists of a finite set P of MAPL rules together with a finite set F of function definitions that includes exactly one definition for every function symbol used in P.

Previous examples such as (1) and (7) have already used rule-shaped formulae. Example 8 therefore showed a MARPL ontology. A slightly more complex example is given next.

Example 9. MAPL rules allow for elaborate inferences, where we can enrich annotations by information from other statements. The following rule can, for example, infer from a spouse statement and a matching dateOfDeath statement that the marriage must have ended on the day of the death:2

where the function definition hEndedByDeath; hU;V; zi; Ci with the following conditionals is present:

2This simplified example is inspired by actual usage on Wikidata, where one may indeed find spouse statements that are annotated with an end cause death.

Given the facts spouse"todd; taylor"@fstart : 1957-02-02g and dateOfDeath"todd; 1958-03-22"@fg, by using the above rule, we can infer spouse"taylor; todd"@fstart : 1957-02-02; end : 1958-03-22; endCause : Deathg, explaining the end of one of Taylor's marriages.

While specifiers and function definitions are syntactic sugar for MAPL, they add true expressive power to MARPL. Indeed, although MARPL rules use only universal second-order quantifiers explicitly, they are not in the fragment of universal second-order logic (USO), since specifiers and function definitions introduce hidden second-order existentials.

Nevertheless, MARPL is not truly a higher-order logic. For the following statement, we consider first-order logic with equality � (FO�) under the unique name assumption (UNA): Theorem4. EveryMARPL ontology hP ; Fi can be translated into a set of FO� sentences M2FO"P ; F", and every variablefree MAPL atom ' into a FO� sentence M2FO"'", such that hP ; Fi j= ' iff M2FO"P ; F" j= M2FO"'" under the UNA.

The translation M2FO is based on the representation of MARS in standard first-order relational structures. For a given MARS predicate symbol p of arity n, we introduce a new "n + 1"-ary first-order predicate symbol ¯ p. Moreover, we use an auxiliary predicate in of arity ar"in" = 3. We can now encode aMARS tuple h�1; : : : ; �n; Si 2 p I , where S is a binary relation fh�1; �1i; : : : ; h�m; �mig, using tuples h�1; : : : ; �n; �i 2 ¯ p I and h�1; �1; �i 2 in I ; : : : ; h�m; �m; �i 2 in I . That is, we introduce an auxiliary domain element � to represent the set S. Translated formulae accordingly use first-order variables to represent sets, e.g.,a MAPL atom "a : b" 2 U turns into in"a; b; u", where u is a first-order variable that is specific to U. We simply use lower-case variants of set variables to indicate this switch. As rules are safe and MARPL does not admit counting quantifiers, this mixing of object and set variables is unproblematic. A variable-free relational MAPL atom ' = p"t1; : : : ; tn"@fa1 : b1; : : : ; am : bmg therefore becomes

The translation of MARPL rules uses similar formulae to capture relational and specifier atoms. For every function definition hF; S; Ci, we introduce a fresh "jSj + 1"-ary predicate symbol ¯F. Let s be the signature of F with all set variables replaced by first-order variables. For every conditional '1; : : : ; 'n ) insert"a1 : b1; : : : ; am : bm" in C, we add a rule

where ¯ 'i denotes the first-order translation of the atom 'i. In combination with the translated MARPL rules, this yields the required translation M2FO"P ; F".

This shows that MARPL reasoning is semidecidable. We show in Section 5 that it is decidable in ExpTime, which is the best result that one could expect considering the ExpTimehardness of Datalog. Yet, surprisingly, this bound is tight for data complexity, which is much lower (PTime) for Datalog.

Theorem 5. Deciding fact entailment for MARPL ontologies is ExpTime-hard, even when restricting to classes of ontologies where only the set of facts is allowed to vary.

Our proof is based on an interesting reduction from the word problem of polynomially space-bounded Alternating Turing Machines, where we use attribute-value sets to represent ATM configurations. The key idea is to compute accepting configurations backwards starting from the final configuration. The structure of the polynomial tape can be given in annotations that are part of the input facts. Function definitions can then perform most of the computation needed to determine possible predecessor configurations. The ATM accepts if the initial configuration can be derived in this way.

5 Reasoning withMARPL

We are interested in reasoning with MARPL. A natural reasoning task in this context is fact entailment: given a MARPL ontology hP ; Fi and a variable-free relational MAPL atom ' , we wish to decide if hP ; Fi j= ' holds. More general query answering can be reduced to this task. We have already established the semi-decidability of reasoning in MARPL. We now present a decision procedure that, informally speaking, proceeds as follows:

• We consider all annotations of previously derived facts as fixed and final ("immutable"). This makes it easy to evaluate atoms, including all specifier atoms, whether or not they require negation.
• When applying an ontological rule, we create a new annotation as computed from its defining function. This is a finite "initialisation" process that creates new sets.
• We eagerly eliminate duplicates, i.e., relational atoms that agree on the first-order atom and annotation after initialisation.

Exhaustive rule application along these lines yields an algorithm that can be applied directly on MARPL ontologies to compute the least MARS that satisfies them.

Definition 10. A ground (MAPL) substitution � is a partial mapping from object and set variables to constants and variable-free set terms, respectively. Given a term or formula ', we write '� for the term or formula obtained by replacing each variable � in ' with �"�", whenever this is defined.

Definition 11. The MARS chase procedure takes a MARPL ontology hP ; Fi and constructs a finite interpretation I as follows. The domain of I is the finite set of constants c 2 C in hP ; Fi; and such constants are interpreted as c I B c. We initialise p I B ; for every predicate p, and repeat the following steps until no more changes occur:

• (A) Let ' ! p"t1; : : : ; tn"@� 2 P be a rule and let � be a ground substitution such that I j= '� but I 6 j= p"t1; : : : ; tn"@��.
• (B) If � is a set term or a set variable, set T B S�. Note that � is ground, because � is either a variable-free set term or appears in '. Otherwise, if � = F"�1; : : : ; �'", set T B F"�1�; : : : ; �'�".

The result I of this procedure is denoted I"P ; F".

We start out with a finite set of constants, so there are only finitely many finite sets over this set of constants. Hence, there are only finitely many facts that can be derived, so the algorithm terminates after finitely many steps.

The next result shows that I"P ; F" plays the role of a least model for MARPL, similar to the least model of Datalog. While MARPL specifiers introduce a form of negation, the saturation of Definition 11 remains monotone, since specifiers refer to annotations of previously derived ground atoms, whereas rule applications can only derive new ground atoms but never modify existing ones. This mechanism can also be understood as a form of local stratification of negation.

Theorem 6. For any MARPL ontology hP ; Fi, we have hP ; Fi j= � iff I"P ; F" j= � for any variable-free atom �.

Proof. Clearly, the MARS chase terminates after finitely many steps and the resulting interpretation I"P ; F" is finite.

Further note that the MARS chase is monotone in the sense that I"P ; F" can be considered as a set of ground facts, where each rule application may add new facts but not modify or delete previously derived ones.

For soundness, we show by induction that I"P ; F" j= � implies J j= � for every model J of hP ; Fi, and every ground fact � . Clearly, any fact in P holds in J. Consider now an applicable rule ' ! 2 P. Then there is aground substitution � such that I"P ; F" j= '� . Hence, by the induction hypothesis, J j= '� . Any fact added to I"P ; F" by applying ' ! must also be present in J, since all variables in appear in ' (and are therefore mapped to constants by � ) and J j= ' ! .

For completeness, we show that I"P ; F" is indeed a model of hP ; Fi. Assume to the contrary that some rule ' ! 2 P does not hold in I"P ; F", i.e., for some variable assignment Z, we have I"P ; F";Z j= ' , but I"P ; F"; Z 6 j= . Then ' ! is an applicable rule, and its application results in at least one fact being added to I"P ; F" in (A) - contradiction. �

With k constants, one can define 2 k 2 distinct annotations. If the maximal arity of predicates in an ontology is a, there are at most jPj � k a � 2 k 2 MAPL facts. This yields an upper bound for the number of iterations in the MAPL chase, and thus a matching upper bound for Theorem 5. Note that individual rule applications can also be done in this bound: we can find the required match (A), and compute the new fact (C) in NP.

Theorem 7. Deciding fact entailment for MARPL ontologies is in ExpTime.

Our estimation for the upper bound also reveals that the hardness for data complexity is related to the size of annotations, which occurs in the exponent in 2 k 2 . We can obtain lower bounds by restricting to cases where k is bounded by a constant. A MARPL ontology hP ; Fi belongs toMARPLk for k � 0 iff for any entailed fact hP ; Fi j= p"t1; : : : ; tn"@S, the number of attribute-value pairs in S is at most k.

Theorem 8. For any k � 0, deciding fact entailment for MARPLk ontologies is in PTime with respect to data complexity, i.e., when considering rules except facts to be fixed.

Note that, while data complexity generally allows us to vary the set of facts while keeping other rules fixed, not all sets of facts may lead to an ontology in MARPLk . Theorem 8 states that we recover the low data complexity of Datalog if annotation sizes are bounded. This insight is practically relevant since typical Property Graphs do not use very large annotations, but it is not easy to invoke Theorem 8 directly: reasoning is necessary to determine if an ontology (with a given set of facts) is in MARPLk . However, one can find simpler syntactic conditions, e.g., for ontologies without function definitions:

Theorem 9. An ontology hP ; ;i is in MARPLk for every k greater or equal to the largest set term in (facts or rules of) P.

6 Discussion and Outlook

We presented a first approach towards ontological modelling on Property Graphs and related data formats. Our rule-based formalism MARPL captures key expressive features of our general, second-order logic framework while ensuring approachable reasoning complexity based on practical bottomup algorithms. Combined complexity agrees with other popular rule languages, such as Datalog, but it may seem problematic that worst-case reasoning time may grow exponentially in the size of the data (which is usually large). However, our hardness proof requires attribute-value sets to grow arbitrarily large, which we think is not to be expected in practical applications. Typical applications rather have bounded-size annotations, for which data complexity drops to PTime.

Nevertheless, our ExpTime data complexity (and even more so the non-semidecidability of our overall framework) underlines that our work is fundamentally different from other scenarios studied in AI. Indeed, we are not aware of any closely related work. Attributed graphs are supported by several database management systems, but even basic "integrity constraints are poorly studied in graph databases" [Angles, 2012]. Somewhat related to our work are recursive graph query languages over advanced graph models, such as SNQL [Martín et al., 2011], GraphQL [He and Singh, 2008], G-Log [Paredaens et al., 1995], and GraphLog [Consens and Mendelzon, 1989]. As MARPL extends Datalog, it subsumes Datalog fragments such as GraphLog, but other algebras sport incomparable expressivity such as the computation of aggregates in SNQL. Maybe closest to the spirit of our work, Moustafa et al. proposed an extension of Datalog where set-valued parameters represent edge attributes for social network analysis [2011].

None of these works are truly concerned with knowledge representation or AI, and indeed it seems that this community has largely ignored enriched graph models so far. Our proposal can offer a first bridge between these hitherto disconnected areas. It now remains to explore how the wealth of insights obtained for other ontology languages can be applied to this new field. Language design, expressive extensions, deduction methods, and implementations all are worthwhile areas of future study with a huge potential for applications.

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).