The Complexity of Reasoning: Why Profiles Exist

📍 Where we are: Part II · Description Logic — Chapter 7. OWL 2 Profiles sorted the standard ontology language into the EL, QL, and RL sublanguages; this chapter explains the force behind that sorting — the single expressivity-versus-cost curve that every profile is a deliberately chosen point on.

The three profiles from the previous chapter are not marketing tiers. Each is engineered to sit at a precise spot on one curve that trades what a language can say against what it costs to reason in it. This chapter draws that curve, names the milestones along it, and shows — on the academic world's own completion run — what "cheap" looks like when you watch it happen.

The simple version

Imagine shopping for a camera. A phone camera is instant and fits your pocket, but it cannot capture everything. A full studio rig can photograph anything, but it is heavy, slow, and needs an expert to run. Description logics work the same way. A small, fast language answers every question in a blink but can only express so much. A maximally expressive language can describe almost any situation, but a single question may take longer than the age of the universe to answer — and the very fullest language may never answer at all. The OWL 2 profiles are the camera line-up: each one is a chosen bargain of how much saying-power you will trade for a guaranteed fast reply.

What this chapter covers

• A crash course in complexity — what "decidable," "PTIME," "ExpTime," and "undecidable" mean, in one plain paragraph each, assuming no prior complexity theory.
• The trade-off thesis — every constructor you add (negation, disjunction, cardinality) buys expressive power and costs worst-case time; a table places the DL and OWL flavours on the cost curve.
• Why EL stays polynomial — its completion algorithm iterates a monotone fixpoint over a fact set that can never outgrow the square of the vocabulary; we watch it settle in 3 rounds on the academic world.
• Why expressive logics blow up — disjunction and negation force case splits, turning polynomial fact-adding into an exponentially branching search.
• The undecidability wall — full first-order logic can encode a computation that never halts, so no algorithm can always answer.
• Combined versus data complexity — why QL is the profile for querying gigantic ABoxes even though EL classifies a TBox faster.

A crash course in complexity: four words you need

Reasoning either terminates with the right answer or it does not, and if it does, it is either quick enough to run or not. Four words pin down those cases; here is each, from scratch.

Decidable. A yes/no problem is decidable if there exists a single algorithm that, on every possible input, is guaranteed to halt and return the correct answer. "Is $A \sqsubseteq B$ entailed by this TBox?" is decidable in every description logic we study: you can write a procedure that always finishes and never lies. Decidability says nothing about speed — only that the machine always stops.

PTIME (polynomial time). An algorithm runs in polynomial time if the number of steps it takes is bounded by a polynomial in the input size $n$ — something like $n$, $n^2$, or $n^3$, never $n$ appearing in an exponent. This is the practical meaning of tractable: double the input and the running time grows by a fixed factor, not by squaring the whole workload. Problems in $\mathrm{PTIME}$ scale to real data.

ExpTime (exponential time). An algorithm runs in exponential time if its step count is bounded by $2^{p(n)}$ for some polynomial $p$. Now adding a single symbol to the input can double the work. Exponential functions climb a wall almost immediately — at $n = 40$ the count is already in the trillions. N2ExpTime ("nondeterministic doubly exponential time") is worse still, roughly $2^{2^{p(n)}}$: exponentiating an already-exponential number. When a problem is called $\mathrm{ExpTime}$-complete, that is not merely an upper bound — the problem is provably as hard as anything in the class, so no cleverer algorithm can escape the wall in the worst case [1].

Undecidable. A problem is undecidable if no algorithm decides it for all inputs — not a slow one, not any one. You can sometimes build a semi-decider that answers "yes" correctly whenever the answer is yes but may run forever when it is no. Entailment in full first-order logic is the canonical example: there is no machine that always halts with the right verdict.

The trade-off: every constructor has a price

Here is the thesis in one line. Expressivity and complexity trade off against each other. Each concept constructor a logic admits — conjunction ⊓, existential ∃, disjunction ⊔, negation ¬, number restrictions, inverse roles, nominals — lets you say more, and each one also gives a reasoner more ways to branch, which shows up as worst-case time. The EL family that our companion implements keeps only ⊓ and ∃ (plus ⊥, role chains, and the ABox in EL++), and that frugality is exactly why its subsumption problem stays in $\mathrm{PTIME}$ [2]. Pile the missing constructors back on and the cost climbs step by step, from polynomial to exponential to doubly exponential to the undecidability cliff.

Logic / OWL 2 profile	Constructors it adds	Subsumption (with a general TBox)
EL, EL++ / OWL 2 EL	⊓, ∃, ⊥, role chains	$\mathrm{PTIME}$-complete
DL-Lite / OWL 2 QL	limited ∃, inverse roles	tractable on the TBox; query answering is first-order rewritable
OWL 2 RL	Horn-shaped rule axioms	$\mathrm{PTIME}$-complete (instance checking)
ALC	¬, ⊔, ∀	$\mathrm{ExpTime}$-complete
SHIQ	+ transitive roles, role hierarchy, inverses, number restrictions	$\mathrm{ExpTime}$-complete
SROIQ / OWL 2 DL	+ nominals, complex role inclusions	$\mathrm{N2ExpTime}$-complete
First-order logic	full quantification, arbitrary predicates	undecidable

The jump from EL to ALC is the price of a single idea — the ability to write ¬ and ⊔ — and it is the difference between $\mathrm{PTIME}$ and $\mathrm{ExpTime}$ [3]. Read the whole table as a staircase: the profiles were carved out precisely so a modeller can choose the step whose guarantee they need.

The expressivity-versus-cost curve the OWL 2 profiles are chosen points on: polynomial EL near the origin, a doubly exponential wall at SROIQ, and the decidability cliff where full first-order logic runs off the map. Original diagram by the authors, created with AI assistance.

Why EL stays polynomial: a fixpoint that cannot explode

The EL reasoner in el_completion.py is the same shape as Volume 1's forward-chaining engine — a monotone fixpoint: seed a set of facts, fire a fixed set of rules that only ever add facts, and stop when a full pass adds nothing. Here the facts are subsumptions. The algorithm maintains two tables (docstring, el_completion.py lines 20–21): $S(A)$, the set of concept names $A$ is known to be subsumed by, and $R(r)$, the set of pairs $(A, B)$ with $A$ known to satisfy $\exists r.B$. The completion rules CR1–CR4, the bottom rule, and the role-chain rule saturate these tables until a fixpoint (complete, lines 177–261).

The whole polynomial guarantee comes from one bound. Let $N$ be the number of concept names. Then $S(A)$ is a subset of the names, so $|S(A)| \le N$, and $R(r)$ is a subset of pairs of names, so $|R(r)| \le N^2$. Summing over the vocabulary,

$$|S| \;=\; \sum_{A} |S(A)| \;\le\; N^2, \qquad |R| \;=\; \sum_{r} |R(r)| \;\le\; |\text{roles}| \cdot N^2 .$$

Because the completion rules never delete anything, each round either adds at least one new fact or the loop exits, so the number of rounds is bounded by the total number of facts there could ever be — at most $N^2 + |\text{roles}| \cdot N^2$, a polynomial. Each round does a polynomial amount of scanning. A polynomial number of polynomial-cost rounds is still polynomial, and so subsumption in EL is in $\mathrm{PTIME}$ — sound and complete for EL++, and fast enough to classify SNOMED CT and the Gene Ontology, whose hundreds of thousands of concepts would be hopeless in any exponential logic (docstring, lines 38–40) [2].

The monotone, branch-free heart is only ten lines — note that every rule adds to $S$ and flips changed; nothing is ever retracted, so there is no backtracking to pay for (el_completion.py lines 210–219):

    rounds = [sizes()]
    changed = True
    while changed:
        changed = False

        # CR1: A' ∈ S(A), A' ⊑ B  ⟹  B ∈ S(A)
        for _, a_prime, b in nf1:
            for A in names:
                if a_prime in S[A] and b not in S[A]:
                    S[A].add(b); changed = True

Run the module and the polynomial behaviour becomes a printout. The bookkeeping function sizes (lines 205–208) records $|S|$ and $|R|$ after every pass, and the trace shows the climb reaching its ceiling and stopping:

normalization: 14 axioms → 16 normal-form axioms, introducing 2 fresh names ['_N1', '_N2']
  by normal form: {'chain': 1, 'nf1': 6, 'nf2': 2, 'nf3': 3, 'nf4': 4}

saturation reached a fixpoint in 3 rounds
  round : |S| |R|  (derived subsumers, derived role pairs)
      0 :  23   0
      1 :  34   7
      2 :  39   7
      3 :  39   7

Read the middle column as a monotonically growing fact set: because rules only add, the set $S$ at each round contains the previous round's, $S_0 \subseteq S_1 \subseteq S_2 \subseteq S_3$, so its counts can only rise, $|S| = 23 \le 34 \le 39 \le 39$. The academic world has just twelve concept names — the eight declared names that occur in the axioms, the two fresh names normalization introduces, and ⊤ and ⊥ (_concept_names, lines 160–174). Each starts knowing only that it is subsumed by itself and by ⊤ (S = {a: {a, TOP} ...}, line 187), which is why the trace opens at exactly $|S| = 23 = 2 \times 12 - 1$ (⊤ needs no second entry). The theoretical ceiling is $N^2 = 144$ subsumers; the fixpoint lands at $39$, far below it, after 3 rounds. The last round, $39 \to 39$ and $7 \to 7$, is the engine proving to itself it is finished — the changed flag stays false and the loop halts. Three rounds for fourteen axioms is not a magic constant; it is the shape of the guarantee — the count of facts can only rise, and it can never rise past a polynomial ceiling.

Why expressive logics blow up: disjunction makes you guess

EL's completion never branches because EL has nothing to branch on. Its constructors, ⊓ and ∃, are deterministic: if a concept is $C \sqcap D$, it is both a $C$ and a $D$ — no choice. The moment you add disjunction ⊔ (and, through negation ¬ pushed inward, its inevitable companion), you introduce genuine choice. To test whether an individual can be a $C \sqcup D$, a reasoner must consider two worlds — one where it is a $C$, one where it is a $D$ — because the two can lead to different contradictions. This is the tableau method: build a candidate model by branching on every disjunction and backtracking when a branch closes on a clash such as $C$ and ¬$C$ together.

Branching is where the cost lives. A concept expression with $k$ independent disjunctions forces a search tree with up to

$$2^{k}$$

leaves, and $k$ grows with the size of the TBox. Polynomial fact-adding has become exponential search: EL's "add every consequence once" turns into ALC's "try every combination of choices." That is the mechanism behind the table's jump — subsumption with a general TBox is $\mathrm{ExpTime}$-complete for ALC and stays exponential as you add inverse roles and number restrictions in SHIQ, then reaches $\mathrm{N2ExpTime}$-complete for SROIQ, the logic under OWL 2 DL, once nominals and complex role inclusions interact [1]. Reasoners such as HermiT and Konclude implement heavily optimized tableau (and hypertableau) search precisely because, for the full language, no polynomial escape exists. The academic world's two unsatisfiable concepts are caught in EL with no branching at all: TenuredStudent by the conjunction rule CR2 firing on Professor ⊓ Student ⊑ ⊥ (el_completion.py lines 221–225), since S(TenuredStudent) already holds both Professor and Student, and TenuredStudentAdvisor by the bottom rule CR⊥ propagating ⊥ back along advises (lines 240–244), since its only advises-edge points at the now-unsatisfiable TenuredStudent — but both derivations only because we expressed disjointness with ⊥ rather than with the negation an expressive logic would let us write.

The undecidability wall: some questions have no algorithm

Keep adding power and eventually you fall off the cliff the dashed line marks. Full first-order logic — arbitrary predicates, unrestricted ∀ and ∃, nesting without limit — is expressive enough to describe the step-by-step run of an arbitrary computing machine. Because you can encode "this machine eventually halts" as a first-order entailment, an algorithm that always decided entailment would also solve the halting problem, which provably cannot be solved. So first-order entailment is undecidable: the best you get is a semi-decider that confirms genuine entailments but may run forever on non-entailments.

Description logics are, deliberately, fragments of first-order logic chosen to stay on the safe side of that cliff — every DL in the table above is decidable. The wall returns in Part IV, where existential rules (rules whose head asserts that something exists) generalize the ontology's role axioms. Firing such a rule invents a fresh individual that can trigger the rule again, so the forward-chaining process — the chase — can climb forever, minting an endless tower of anonymous witnesses. General existential rules inherit first-order logic's undecidability, and the study of which restricted shapes claw decidability back is a Part IV subject. The lesson to carry now is blunt: past a certain expressive power, "just wait for the answer" stops being a plan, because for some inputs the answer never comes.

Two rulers: combined complexity versus data complexity

There is a subtlety the single curve hides, and it is the whole reason OWL 2 QL exists alongside EL. Complexity can be measured two ways. Combined complexity counts the entire input — TBox, ABox, and query all together. Data complexity counts only the ABox (the data), holding the TBox and query fixed as constants. The distinction matters because real deployments have a modest schema — thousands of TBox axioms — and an astronomical ABox — billions of assertions. At that scale the data dominates, so data complexity is the honest ruler for querying.

Now the two profiles diverge. EL classifies a TBox in $\mathrm{PTIME}$ and reasons over a rich schema, but answering a conjunctive query against its ABox has $\mathrm{PTIME}$-complete data complexity: you cannot hand the work to an ordinary relational database — you must run a bespoke saturation over all the data. QL (the DL-Lite family) sacrifices schema expressivity to win the query game outright: any query plus a QL TBox can be rewritten into a single first-order (SQL-style) query that is evaluated directly against the raw ABox in a standard database. Its data complexity sits in $\mathrm{AC}^0$, strictly below $\mathrm{PTIME}$ — this is first-order rewritability [3]. So the choice is not "which profile is faster" but "which problem are you optimizing": EL for classifying a large, expressive TBox; QL for querying a colossal ABox through a database. Two rulers, two winners, one reason the standard ships more than one profile.

The unsolved part

The $\mathrm{PTIME}$ badge on EL is a worst-case promise, and a worst case is not a program. The bound says only that some algorithm finishes in polynomial time; it does not, by itself, hand you the algorithm, and a naive one can still scan the whole vocabulary on every rule of every round, which is polynomial but wasteful. The gap between "polynomial in principle" and "milliseconds on SNOMED CT in practice" is filled by engineering the completion the theory merely guarantees: indexing $S$ and $R$ so a rule touches only the facts that changed, ordering rule application to avoid rescanning, and — first of all — reshaping every axiom into a handful of uniform patterns the rules can match in constant time. Our run already leaned on that last step: 14 axioms → 16 normal-form axioms is the preprocessing that let CR1 fire with a single set-membership test. Whether the polynomial promise is actually cashed depends entirely on that machinery, and it is what Part III builds next.

Why it matters

Neuro-symbolic systems put a reasoner in a loop with a learner, often calling it thousands of times during training or inference. A reasoning step that is polynomial is a component you can afford to invoke repeatedly; one that is exponential is a bottleneck that can dominate the entire system; one that is undecidable can hang it indefinitely. Knowing where a logic sits on this curve is therefore a systems decision, not a theoretical footnote. It also reframes what "more expressive" costs: every extra constructor a hybrid model wants — to encode a richer prior, a softer rule, a cardinality constraint — is a move rightward on the curve, toward a slower or even unanswerable reasoning core. The profiles are the map of that trade, and reading them fluently is how you pick a symbolic engine a learning system can actually run against in real time.

Key terms

• Decidable — a problem some single algorithm always halts on with the correct answer; every description logic in this chapter is decidable, full first-order logic is not.
• PTIME (polynomial time) — step count bounded by a polynomial $n^k$ in the input size; the practical meaning of tractable, and where EL subsumption lives.
• ExpTime / N2ExpTime — step counts bounded by $2^{p(n)}$ and $2^{2^{p(n)}}$; the walls that ALC and SROIQ subsumption respectively run into.
• Undecidable — no algorithm decides it for all inputs; first-order entailment, and general existential rules via the non-terminating chase, are the canonical cases.
• -complete — as hard as anything in a complexity class, so the bound cannot be beaten in the worst case (e.g. EL is $\mathrm{PTIME}$-complete, SROIQ is $\mathrm{N2ExpTime}$-complete).
• Monotone completion fixpoint — EL's reasoning as a fact set that only grows, bounded by $N^2$ subsumers over $N$ names, reached here in 3 rounds; no branching, no backtracking.
• Tableau branching — the case split disjunction and negation force, giving up to $2^k$ search branches and turning polynomial saturation into exponential search.
• Combined vs data complexity — cost measured over the whole input versus over the ABox alone; the reason QL beats EL for querying huge data despite EL classifying richer schemas.
• First-order rewritability — QL's property that a query plus TBox becomes one SQL query over the raw ABox, giving $\mathrm{AC}^0$ data complexity.

Where this leads

The curve explains why EL is cheap; it does not yet show how the cheap algorithm is built. The completion rules CR1–CR4 could only fire in constant time because every axiom had already been beaten into one of exactly four uniform shapes — the step that quietly turned 14 axioms into 16 normal-form axioms before saturation began. The next chapter, Normalization, opens Part III by making that preprocessing precise: the four EL normal forms, the fresh-name trick that names compound subconcepts away, and the proof that the rewrite is a conservative extension preserving every subsumption. It is the groundwork that lets Part III assemble the polynomial reasoner this chapter only promised.