Datalog and DL Engines: RDFox, HermiT, Konclude

📍 Where we are: Part V · Reasoners in Practice — Chapter 16. EL Reasoners showed how ELK and CEL turn the six completion rules into industrial classifiers for the OWL 2 EL profile; now we widen the lens to the two great engine families of symbolic reasoning — rule materializers and tableau model-builders — and discover they are far closer kin than their reputations suggest.

The previous chapters built one reasoner — EL completion — and proved it correct. But that is one engine for one logic. Step back into any real deployment and you meet a whole zoo of tools with different names, different theories, and wildly different performance. This chapter draws the engine map: it sorts the major reasoners into two families, explains the three strategies they use to answer a query, and then delivers the chapter's punchline — that our from-scratch EL reasoner can be rewritten, line for line, as a plain Datalog program. Two reasoners we built independently are then forced to agree on the very same numbers.

The simple version

Imagine two clerks who both answer questions about a giant rulebook. The first clerk is a planner: the night before, she works out every consequence the rules could ever have and files them all in a huge cabinet, so any question in the morning is a one-second lookup. The second clerk is a detective: he ignores the cabinet and, for each specific question, tries hard to draw a world in which the answer is "no." If every attempt to draw that world collapses into a contradiction, he concludes the answer must be "yes." One precomputes everything up front; the other searches, question by question, for a counterexample. They work in completely different styles — and yet, for the questions our little academic ontology asks, they hand back exactly the same answers.

What this chapter covers

• The engine map — RDFox as an in-memory, parallel Datalog materializer, and HermiT and Konclude as tableau reasoners that decide full OWL 2 DL, with a table pinning each engine to its method and its sweet spot.
• Three strategies for one job — materialization, query rewriting, and tableau model construction: precompute everything, rewrite the question, or search for a model, and the trade-off each one accepts.
• The punchline — EL completion written out as six Datalog meta-rules over the predicates sco and rel: the completion rules CR1–CR4, the bottom rule, and the role chain, in disguise.
• From TBox to EDB — how the normalized axioms become plain database facts nf1 through nf4 and chain, with ⊓'s commutativity deliberately emitted both ways.
• The committed run — the five-wave least fixpoint [30, 53, 62, 71, 76, 76] climbing to 39 sco and 7 rel atoms, forced to agree with the from-scratch completion reasoner.
• What it means for the field — the boundary between a "DL reasoner" and a "rule engine" is a matter of encoding, not of kind.
• The unsolved part — engines differ enormously in real speed and coverage, so how do we compare them fairly?

The engine map: two families, one job

Every reasoner in this chapter answers the same underlying question — what does this knowledge base entail? — but they split into two families by how they answer it.

The first family is the rule / materialization engines. The flagship is RDFox, an in-memory, massively parallel Datalog engine [1]. Given a set of stored facts and a set of rules, RDFox computes the materialization — the least fixpoint of the immediate-consequence operator $T_P$, the exact climb of Volume 1's forward chaining — and keeps every derived fact in memory so that later queries are lookups, not searches. Its engineering contribution is doing that saturation in parallel across cores while keeping the answer identical to the single-threaded fixpoint, which lets it materialize datasets with hundreds of millions of triples. RDFox reasons over rules, which covers RDF Schema and the OWL 2 RL profile (the rule-expressible fragment of OWL) — but not, on its own, the parts of OWL that need genuine model search.

The second family is the tableau / model-building engines, and they exist precisely for those harder parts. HermiT [2] and Konclude [3] are complete reasoners for SROIQ, the description logic that underlies OWL 2 DL — the full-strength profile with negation, disjunction, cardinality, and inverse roles. They cannot materialize their way to an answer, because those constructors let a knowledge base have many possible models rather than one canonical least model. Instead they build one: to test a claim, a tableau reasoner tries to construct a concrete model that would make the claim false, and reports the claim proven exactly when every such attempt collapses. HermiT pioneered a hypertableau calculus that curbs the branching such search normally suffers; Konclude combines optimized tableau expansion with saturation and aggressive parallelism, and has been among the fastest OWL 2 DL reasoners in competition. Our companion module reasoners.py drives HermiT directly (reasoners.py lines 94–113, via sync_reasoner at line 99) to cross-check the from-scratch EL result against a production tableau reasoner.

Here is the map, with the EL-specialist ELK from the previous chapter included for orientation:

engine	family / method	logic decided	sweet spot
RDFox	in-memory parallel Datalog materialization	Datalog, RDFS, OWL 2 RL	huge fact sets; fast repeated queries after saturation
ELK	consequence-based completion	OWL 2 EL	very large TBoxes (SNOMED CT, the Gene Ontology)
HermiT	hypertableau model construction	SROIQ (OWL 2 DL)	full OWL 2 DL expressivity, correctness the priority
Konclude	optimized tableau + saturation, parallel	SROIQ (OWL 2 DL)	full OWL 2 DL, competition-grade speed

The rough rule of thumb: the more expressive the logic, the more you must search rather than saturate, and the more a tableau engine earns its keep; the larger and simpler the data, the more a materializer like RDFox wins.

Three strategies: precompute, rewrite, or search

Underneath those engines are exactly three ways to turn stored knowledge plus a query $Q$ into answers, and each accepts a different trade-off. Read the notation first: write $D$ for the stored base facts (the data), $\mathcal{T}$ for the rules or axioms (the theory), and $\mathrm{lfp}(T_P)$ for the materialized least fixpoint of the theory over the data — every fact that follows.

Materialization (RDFox) computes that fixpoint once and answers every query against it:

$$\text{answer}(Q) \;=\; Q\big(\mathrm{lfp}(T_P)\big).$$

You pay a large one-time cost and a large memory footprint, and you must re-run (or incrementally repair) the materialization whenever the data changes — but each query afterward is a cheap lookup. This is the winning strategy when data is huge, changes slowly, and is queried often.

Query rewriting (the strategy behind the OWL 2 QL profile) refuses to precompute anything. Instead it pushes the reasoning into the query: it rewrites $Q$ into a larger first-order query $Q^{\dagger}$ such that evaluating $Q^{\dagger}$ directly over the raw data gives the same answers reasoning would:

$$Q^{\dagger}(D) \;=\; Q\big(\mathrm{lfp}(T_P)\big).$$

Nothing is stored, nothing goes stale, and the base data can live in an ordinary SQL database — but the rewritten query can grow large, so this wins only for logics tame enough (like DL-Lite) to keep $Q^{\dagger}$ small.

Tableau model construction (HermiT, Konclude) neither materializes nor rewrites. To decide a subsumption $C \sqsubseteq D$ it tries to build a model of $C \sqcap \lnot D$ — an individual that is a $C$ but not a $D$ — expanding the model step by step. If every expansion reaches a clash (a contradiction such as an individual forced to be both $A$ and $\lnot A$), no such counter-model exists and the subsumption holds:

$$C \sqsubseteq D \quad\Longleftrightarrow\quad C \sqcap \lnot D \ \text{ is unsatisfiable (every tableau branch clashes).}$$

This is the only strategy that copes with full OWL 2 DL, because negation and disjunction force a genuine search over possible models — but that search is where the worst-case exponential cost of expressive description logics lives.

The punchline: EL completion is a Datalog program

Now the surprise that collapses the gap between the two families. The completion rules CR1–CR4, the bottom rule, and the role chain — the whole EL reasoner of the last two chapters — are not merely like a rule engine. They are a Datalog program, one you can write out and run. The companion file encodes them over just two derived predicates: sco(A, B), read "sub-concept-of," meaning $A \sqsubseteq B$ (i.e. $B \in S(A)$); and rel(r, A, B), meaning the pair $(A, B)$ sits in $R(r)$, i.e. $A \sqsubseteq \exists r.B$. Here is the entire rulebook (datalog.py lines 146–166):

EL_META_RULES = [
    # Initialisation: S(A) ⊇ {A, ⊤}.
    (("sco", "?a", "?a"), [("concept", "?a")]),
    (("sco", "?a", TOP), [("concept", "?a")]),
    # CR1: A' ∈ S(A), A' ⊑ B  ⟹  B ∈ S(A)
    (("sco", "?a", "?c"), [("sco", "?a", "?b"), ("nf1", "?b", "?c")]),
    # CR2: A1, A2 ∈ S(A), A1 ⊓ A2 ⊑ B  ⟹  B ∈ S(A)
    (("sco", "?a", "?c"),
     [("sco", "?a", "?b1"), ("sco", "?a", "?b2"), ("nf2", "?b1", "?b2", "?c")]),
    # CR3: A' ∈ S(A), A' ⊑ ∃r.B  ⟹  (A,B) ∈ R(r)
    (("rel", "?r", "?a", "?b"), [("sco", "?a", "?ap"), ("nf3", "?ap", "?r", "?b")]),
    # CR4: (A,B) ∈ R(r), B' ∈ S(B), ∃r.B' ⊑ C  ⟹  C ∈ S(A)
    (("sco", "?a", "?c"),
     [("rel", "?r", "?a", "?b"), ("sco", "?b", "?bp"), ("nf4", "?r", "?bp", "?c")]),
    # CR⊥: (A,B) ∈ R(r), ⊥ ∈ S(B)  ⟹  ⊥ ∈ S(A)
    (("sco", "?a", BOT), [("rel", "?r", "?a", "?b"), ("sco", "?b", BOT)]),
    # role chain: (A,B) ∈ R(r), (B,C) ∈ R(s), r ∘ s ⊑ t  ⟹  (A,C) ∈ R(t)
    (("rel", "?t", "?a", "?c"),
     [("rel", "?r", "?a", "?b"), ("rel", "?s", "?b", "?c"),
      ("chain", "?r", "?s", "?t")]),
]

Read it top to bottom against the completion rules you already know. The first two rules are the seed: for every basic concept ?a, sco(?a, ?a) and sco(?a, ⊤) — exactly $S(A) \supseteq \{A, \top\}$. Then the six meta-rules proper. The rule with head sco(?a, ?c) and body sco(?a, ?b), nf1(?b, ?c) is CR1: if $A$ is already an $A'$ and there is an axiom $A' \sqsubseteq B$, conclude $A \sqsubseteq B$ — plain transitivity, written as a Datalog join. CR2 joins two sco atoms against one nf2 fact to fire a conjunction axiom. CR3 reads a sco and an nf3 axiom and writes a role edge rel. CR4 — the subtle existential elimination — reads a rel edge and a sco on its target and writes a new sco back, exactly the flow of information from the edge ledger into the subsumer ledger. The bottom rule propagates ⊥ backward across a rel edge, and the last rule composes two rel edges through a chain axiom into a third. There is no new machinery here: this is the same monotone operator, expressed as rules whose only terms are constants (concept names, ⊤, ⊥) and ?-prefixed variables. A Datalog engine is all it takes.

The two engine families and the identity that joins them: a materializer saturates rules, a tableau reasoner searches for a model, and between them the six EL completion rules run as a Datalog program that climbs to 39 sco and 7 rel atoms and agrees with the from-scratch reasoner. Original diagram by the authors, created with AI assistance.

From TBox to EDB: axioms become database facts

A Datalog program is only half a reasoner; it needs data to run over. In database terms the stored input facts are the EDB (the extensional database) and the derived facts are the IDB (the intensional database). Here the EDB is the normalized TBox itself, re-expressed as flat facts. The encoder normalizes the axioms and then emits one EDB fact per normal-form axiom (datalog.py lines 169–191):

def tbox_to_edb(tbox=None):
    """Encode a (normalized) TBox as Datalog EDB facts the meta-rules read."""
    if tbox is None:
        tbox = onto.TBOX
    normalized, _fresh = elc.normalize(tbox)
    edb = set()
    for name in elc._concept_names(normalized):
        edb.add(("concept", name))
    for ax in normalized:
        if ax[0] == "nf1":
            edb.add(("nf1", ax[1], ax[2]))
        elif ax[0] == "nf2":
            conj = ax[1]
            assert len(conj) == 2, "this encoding assumes binary conjunctions"
            edb.add(("nf2", conj[0], conj[1], ax[2]))
            edb.add(("nf2", conj[1], conj[0], ax[2]))   # ⊓ is commutative
        elif ax[0] == "nf3":
            edb.add(("nf3", ax[1], ax[2], ax[3]))
        elif ax[0] == "nf4":
            edb.add(("nf4", ax[1], ax[2], ax[3]))
        elif ax[0] == "chain":
            edb.add(("chain", ax[1][0], ax[1][1], ax[2]))
    return edb

Each branch is a straight transcription of a normal form into a stored tuple. The one detail worth pausing on is the pair of nf2 emissions. Conjunction is unordered — $A_1 \sqcap A_2$ is the same concept as $A_2 \sqcap A_1$ — but the Datalog rule CR2 matches its two conjuncts positionally against nf2(?b1, ?b2, ?c). To guarantee CR2 fires no matter which of the two sco atoms the join happens to bind first, the encoder stores the axiom both ways, (conj[0], conj[1], ...) and (conj[1], conj[0], ...). It is a one-line reminder that a faithful rule encoding must respect the semantics of the original operator, not just its surface syntax. The full predicate scheme is small:

predicate	kind	meaning	source
concept(A)	EDB	$A$ is a basic concept name	every name in the normalized axioms
nf1(A, B)	EDB	$A \sqsubseteq B$	an NF1 axiom
nf2(A₁, A₂, B)	EDB	$A_1 \sqcap A_2 \sqsubseteq B$	an NF2 axiom (stored both orders)
nf3(A, r, B)	EDB	$A \sqsubseteq \exists r.B$	an NF3 axiom
nf4(r, B, A)	EDB	$\exists r.B \sqsubseteq A$	an NF4 axiom
chain(r, s, t)	EDB	$r \circ s \sqsubseteq t$	a role-chain axiom
sco(A, B)	IDB	derived $A \sqsubseteq B$	the six meta-rules
rel(r, A, B)	IDB	derived $(A, B) \in R(r)$	the six meta-rules

Feed that EDB and those rules to the identical least-fixpoint loop the academic-world Horn program used — least_fixpoint (datalog.py lines 103–114), the same Kleene climb, unchanged — and the classification falls out.

The committed run: two reasoners forced to agree

Running the program prints the second half of python3 datalog.py, and this is its real, committed output:

Part B — EL completion as Datalog
  least fixpoint in 5 waves; sizes: [30, 53, 62, 71, 76, 76]
  39 sco (subsumption) atoms, 7 rel (role) atoms
  named-concept subsumptions: 8
  agrees with el_completion.py: True

Read [30, 53, 62, 71, 76, 76] as the ascending chain of atom counts, one per wave, exactly like Volume 1's [23, 41, 47, 47]. The climb starts at 30 — the size of the EDB, the encoded TBox before any rule fires — and settles at 76, where the final $76 = 76$ is the wave that changes nothing and so certifies the fixpoint. The arithmetic closes with no remainder: the 30 EDB facts plus the 39 derived sco atoms plus the 7 derived rel atoms give exactly $30 + 39 + 7 = 76$. Those 39 sco and 7 rel atoms are the same $|S| = 39$, $|R| = 7$ the completion engine reported — reached here by a generic rule loop that knows nothing about description logic.

The last line is the payoff. The program pulls the named-concept subsumptions out of the sco atoms and compares them, entry for entry, with the classification the hand-written completion reasoner produces (datalog.py lines 235–238):

    dl_subs = datalog_subsumptions(model, only=set(onto.CONCEPTS))
    el_subs = elc.classify()["subsumptions"]
    print(f"  named-concept subsumptions: {len(dl_subs)}")
    print(f"  agrees with el_completion.py: {dl_subs == el_subs}")

agrees with el_completion.py: True is two independent from-scratch reasoners — one written as a bespoke completion loop, one as a generic Datalog engine over an encoded TBox — landing on the identical 8 subsumptions. Neither could quietly drift, because the equality dl_subs == el_subs would turn True into False the instant they diverged. The wave counts differ (5 here versus 3 in the completion engine) because the two loops schedule the same rule firings differently, but the fixpoint — the meaning — is one and the same set.

What this shows about the field

The identity above is not a party trick; it is a statement about the shape of symbolic reasoning. An EL description-logic reasoner and a Datalog rule engine are, for this logic, the same computation — the least fixpoint of a monotone operator — dressed in different vocabularies. What looked like two disciplines (ontology reasoning on one side, database rule evaluation on the other) turns out to share an engine. That is why a materializer like RDFox can serve as an OWL 2 EL and OWL 2 RL reasoner outright, and why so much of the practical Semantic Web runs on rule engines rather than tableau provers: for the tractable profiles, the boundary between a "DL reasoner" and a "rule engine" is a matter of encoding, not of kind.

The boundary is real only where it must be. The moment a logic admits genuine disjunction or negation — the SROIQ of OWL 2 DL — a single least model no longer captures the meaning, materialization is not enough, and you truly need the model search that HermiT and Konclude perform. The families are complementary, not rivals: use the fixpoint whenever the logic lets you, and pay for the search only when the expressive power demands it. Our companion pins both ends of that spectrum to one world — the same academic ontology is classified by a from-scratch fixpoint, re-classified by a from-scratch Datalog program, and cross-checked against HermiT through reasoners.py, which asserts entry-for-entry agreement (reasoners.py lines 150–152).

The unsolved part

If a rule engine and a tableau reasoner can compute the same thing, an obvious practical question follows: which engine should you actually use, and how would you know? This turns out to be genuinely hard to answer well. Reasoner performance is notoriously workload-dependent: an engine that classifies a huge but shallow biomedical ontology in seconds may stall for hours on a small ontology that happens to trigger expensive disjunctive branching, and the reverse can hold too. Worst-case complexity — polynomial for EL, exponential-and-worse for SROIQ — tells you almost nothing about the case you have, because real ontologies rarely resemble the pathological instances that witness the worst case. Two engines can each be "the fastest reasoner" on different, equally reasonable inputs. So there is no single number, and no theorem, that ranks these engines once and for all. The only honest way to compare them is to fix a shared, representative collection of ontologies and queries, run every engine on all of them under the same conditions, and measure — which is to say, to build a benchmark. That is precisely the subject of the next chapter.

Why it matters

For neuro-symbolic AI, the "encoding, not kind" result is more than tidy. It says the target a learned reasoner must hit — an ontology's exact set of entailments — can be reached by pure rule application, a computation that is uniform, monotone, and, as later volumes show, differentiable. A neural system that learns to fire soft versions of these six meta-rules over sco and rel atoms is, in principle, learning to imitate a real description-logic reasoner, because for EL those two things coincide. And knowing that the exact answer is the same whether computed by completion or by Datalog materialization gives you an unambiguous ground truth: between those two from-scratch reasoners, the identical 39 sco atoms and 7 rel atoms, and — cross-checked against a tableau engine, which verifies only the named-concept results — the 8 subsumptions and two unsatisfiable concepts that HermiT independently confirms. A learned or approximate reasoner is right exactly when it reproduces that fixpoint and wrong exactly when it does not — no interpretation required.

Key terms

• Materialization — precomputing and storing the least fixpoint $\mathrm{lfp}(T_P)$ of a rule set over the data, so queries become lookups; RDFox's strategy.
• Query rewriting — pushing reasoning into the query by rewriting $Q$ into $Q^{\dagger}$ that returns the reasoned answers when run over the raw data; the OWL 2 QL strategy.
• Tableau / model construction — deciding $C \sqsubseteq D$ by trying to build a model of $C \sqcap \lnot D$ and reporting entailment when every branch clashes; the strategy of HermiT and Konclude for OWL 2 DL.
• RDFox — an in-memory, parallel Datalog materialization engine for RDFS and OWL 2 RL over very large fact sets.
• HermiT / Konclude — complete tableau reasoners for SROIQ, the description logic behind OWL 2 DL.
• EDB / IDB — the extensional (stored) versus intensional (derived) database; here nf1–nf4, chain, concept are EDB and sco, rel are IDB.
• sco(A, B) / rel(r, A, B) — the two Datalog predicates encoding $A \sqsubseteq B$ (i.e. $B \in S(A)$) and $(A, B) \in R(r)$.
• EL_META_RULES — the eight-rule Datalog program (two seeding rules plus the six completion rules) whose least fixpoint reproduces EL classification exactly.
• Encoding, not kind — for the tractable profiles, a DL reasoner and a rule engine are the same fixpoint computation in different clothes.

Where this leads

We have two engine families that can, for the tractable logics, compute the very same answers — and no principled way yet to say which is faster or more capable on a given job. The next chapter, Reasoning Benchmarks, builds the missing yardstick: the standard ontology suites, query workloads, and timing protocols the community uses to compare RDFox, HermiT, Konclude, ELK, and the rest on equal footing — turning "it depends" into numbers you can defend, and closing Part V's tour of reasoners in practice.