Kiabora

Kiabora is dedicated to the analysis of a set of existential rules. It can check if this set belongs to a known decidable class of rules (i.e., a class of rules for which conjunctive query answering is decidable) either directly, or by means of its Graph of Rule Dependencies (GRD). Kiabora analyzes the properties of the strongly connected components in the GRD, which allows to determine decidability properties of the whole rule set with respect to decidability, as well as the kind of paradigm (forward or backward chaining, or a mix of both) that ensures decidability.

The analysis is divided into two steps. The first step determines the rule classes of the entire rule set, or of part of it (a strongly connected component of the GRD for instance), while the second step combines these classes in an attempt to ensure finite query answering.

Rule classes

Kiabora considers the main decidable rule classes currently known.
Overview of the rule classes processed by Kiabora.

Determining rule classes

Rule classes are partially ordered by syntactic inclusion (a child is a specialization of its parents). If a test returns success for a rule class, all of its ancestors are noted as being successful without performing any other test.

Only the rule classes selected by the user are considered by the analyzer, therefore the second analysis step may fail even if the tool would be able to find a solution by using other rule classes.

Furthermore, the different tests may be performed on each rule independently or on a set of rules. Indeed, the analyzer first checks all local properties on each rule, then it computes the Graph of Rule Dependencies and checks all global properties on each strongly connected component of the GRD. Finally, it checks all global properties on the entire rule set.

Combining rule classes

Provided that each strongly connected component of the GRD belongs to a known decidable class, the second analysis step consists of combining abstract rule classes (i.e., finite expansion set (fes), finite unification set (fus) and (greedy) bounded treewidth set ((g)bts)) to which the strongly connected components belong, in order to find a way of ensuring finite query answering.

Indeed, a sufficient property for decidability is that no rule from a strongly connected component processed as fes or bts depends on a rule from another strongly connected component processed as fus or bts. In short: FES* |> BTS |> FUS*
where A |> B means "A precedes B", i.e., no rule in (a subset processed as) A depends on a rule in (another subset processed as) B.

Associated publications

Example

Here is a little example to give an insight of what Kiabora can do.

Input file in Datalog+ (Dlgp) format:

Dlgp is the format used in Graal tools. It extends the usual Datalog syntax. Rules have the form 

Head:-Body.
and variables begin with an uppercase letter

p(X,Z) :- p(X,Y), p(Y,Z).
p(Y,X), q(X,Y,X) :- p(X,Y).
q(X,Z,T) :- r(X,Y).
r(Z,T) :- q(X,Y,Z).
s(Z,Z,Z) :- p(X,X), r(Y,U), s(T,Y,X).
s(Z,X,Y) :- s(X,X,X), s(Y,Y,Y).

Output (with all options turned on):

Displays the rule set. Note that unlabeled rules get a label of the form [_Ri] starting with i = 0.

====== Structures ======
== Rule Base ==
[_R0] p(X, Z) :- p(X, Y), p(Y, Z).
[_R1] p(Y, X), q(X, Y, X) :- p(X, Y).
[_R2] q(X, Z, T) :- r(X, Y).
[_R3] r(Z, T) :- q(X, Y, Z).
[_R4] s(Z, Z, Z) :- p(X, X), r(Y, U), s(T, Y, X).
[_R5] s(Z, X, Y) :- s(X, X, X), s(Y, Y, Y).

Displays the graph of rule dependencies (GRD). An edge from Ri to Rj means that Rj depends on Ri (i.e., there exists a fact base F such that an application of Ri to F triggers an application of Rj which effectively adds new atoms).
For advanced users: all the single-piece unifiers that support the dependencies can be displayed as well. For instance, there are two single-piece unifiers showing that R0 depends on itself. Since the same variable names are often used in different rules (or when displaying a unifier from a rule to itself), we use the following notation to distinguish between variables: S::<real_name> denotes a variable from the head of the triggering rule while T::<real_name> denotes a variable from the body of the triggered rule. 

== Graph of Rule Dependencies ==
_R0 -{T::X->S::X,T::Y->S::Z}{T::Y->S::X,T::Z->S::Z}-> _R0
_R0 -{T::X->S::X,T::Y->S::Z}-> _R1
_R0 -{T::X->S::X,S::X->S::Z}-> _R4
_R1 -{T::X->S::Y,T::Y->S::X}{T::Y->S::Y,T::Z->S::X}-> _R0
_R1 -{T::X->S::Y,T::Y->S::X}-> _R1
_R1 -{T::X->S::Y,S::Y->S::X}-> _R4
_R1 -{T::X->S::X,T::Y->S::Y,T::Z->S::X}-> _R3
_R2 -{T::X->S::X,T::Y->S::Z,T::Z->S::T}-> _R3
_R3 -{T::X->S::Z,T::Y->S::T}-> _R2
_R3 -{T::Y->S::Z,T::U->S::T}-> _R4
_R4 -{T::X->S::Z}{T::Y->S::Z}-> _R5
_R5 -{T::X->S::Y,T::Y->S::X,T::T->S::Z}-> _R4

Displays the strongly connected components (SCCs) of the GRD. 

== Strongly Connected Components in the GRD ==
C0 = {_R1, _R0}
C1 = {_R2, _R3}
C2 = {_R4, _R5}

Displays the graph of the SCCs. 

== Graph of Strongly Connected Components ==
C0 --> C1, C2
C1 --> C2
C2

Displays the predicate position graph. This option is not set by default. 

== Predicate Position Graph ==
~> indicates a special edge; positions range from 0 to the arity of the predicate
p[0] --> p[0]
p[1] --> p[1]
p[0] --> p[1]
p[0] --> q[0]
p[0] --> q[2]
p[1] --> p[0]
p[1] --> q[1]
r[0] --> q[0]
r[0] ~> q[1]
r[0] ~> q[2]
q[2] --> r[0]
q[2] ~> r[1]
s[0] --> s[1]
s[1] --> s[1]
s[2] --> s[1]
s[0] ~> s[0]
s[0] --> s[2]
s[1] ~> s[0]
s[1] --> s[2]
s[2] ~> s[0]
s[2] --> s[2]

Displays the rule properties of each rule. For abstract properties (fes,fus, (g)bts), a question mark indicates that Kiabora could not determine if the property is satisfied. 

====== Properties ======
== rule properties ==
+-------------------------------------------------------------------------------------------------------------------------------------------+
|  -   |  X   |  -   |  -   |  X   |  -   |  -   |  ?   |  -   |  X   |  X   |  -   |  X   |  X   |  X   |  -   |  X   |  X   |  X   |  X   | _R0
|  -   |  X   |  -   |  X   |  X   |  X   |  -   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  X   | _R1
|  X   |  X   |  -   |  -   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  -   |  X   |  X   |  X   |  X   |  X   | _R2
|  X   |  X   |  -   |  -   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  -   |  X   |  X   |  X   |  X   |  X   | _R3
|  -   |  X   |  X   |  X   |  X   |  X   |  -   |  X   |  -   |  X   |  X   |  -   |  X   |  X   |  -   |  -   |  X   |  X   |  X   |  X   | _R4
|  -   |  X   |  -   |  X   |  ?   |  -   |  -   |  X   |  -   |  X   |  X   |  -   |  ?   |  ?   |  -   |  X   |  -   |  -   |  -   |  X   | _R5
+-------------------------------------------------------------------------------------------------------------------------------------------+
| agrd | bts  | disc |  dr  | fes  |  fg  | fr1  | fus  |  g   | gbts | jfg  | lin  | mfa  | msa  |  rr  |  s   |  wa  | wfg  |  wg  |  ws  |
+-------------------------------------------------------------------------------------------------------------------------------------------+

Displays the properties of each SCC. These properties are then used in the combining step. 

== Strongly connected component properties ==
+-------------------------------------------------------------------------------------------------------------------------------------------+
|  -   |  X   |  -   |  -   |  X   |  -   |  -   |  ?   |  -   |  X   |  X   |  -   |  X   |  X   |  X   |  -   |  X   |  X   |  X   |  X   |  C0
|  -   |  X   |  -   |  -   |  ?   |  X   |  X   |  X   |  X   |  X   |  X   |  X   |  ?   |  ?   |  -   |  X   |  -   |  X   |  X   |  X   |  C1
|  -   |  ?   |  -   |  X   |  ?   |  -   |  -   |  X   |  -   |  ?   |  -   |  -   |  ?   |  ?   |  -   |  -   |  -   |  -   |  -   |  -   |  C2
+-------------------------------------------------------------------------------------------------------------------------------------------+
| agrd | bts  | disc |  dr  | fes  |  fg  | fr1  | fus  |  g   | gbts | jfg  | lin  | mfa  | msa  |  rr  |  s   |  wa  | wfg  |  wg  |  ws  |
+-------------------------------------------------------------------------------------------------------------------------------------------+

Displays the properties of the entire rule set.

== Entire rule base properties ==
+-------------------------------------------------------------------------------------------------------------------------------------------+
|  -   |  ?   |  -   |  -   |  ?   |  -   |  -   |  ?   |  -   |  ?   |  -   |  -   |  ?   |  ?   |  -   |  -   |  -   |  -   |  -   |  -   |
+-------------------------------------------------------------------------------------------------------------------------------------------+
| agrd | bts  | disc |  dr  | fes  |  fg  | fr1  | fus  |  g   | gbts | jfg  | lin  | mfa  | msa  |  rr  |  s   |  wa  | wfg  |  wg  |  ws  |
+-------------------------------------------------------------------------------------------------------------------------------------------+

Finally, Kiabora follows some combined approach in an attempt to ensure finite query answering. If successful, Kiabora outputs two solutions, which respectively maximize the number of SCCs processed in forward chaining (fes) or in backward chaining, i.e., query rewriting (fus). Note that in this example, no decidability property has been found for the whole rule set, however, finite query answering can be ensured by the combined approach. Trying to maximize fes or fus yields the same result. 

====== Combined Algorithms FES/FUS/BTS ======
Decidable combination found
== Priority FES ==
FES:
    C0
FUS:
    C1, C2
BTS:
== Priority FUS ==
FES:
    C0
FUS:
    C1, C2
BTS: