Tableau — Lazy-Unfolding Algorithm for ALC

A pedagogical Python implementation of the tableau consistency algorithm for ALC knowledge bases, using lazy unfolding for acyclic TBoxes.

Requirements

Python 3.10 or newer. No runtime dependencies. pytest is needed only to run the test suite.

python3 -m venv .venv
source .venv/bin/activate
pip install pytest          # optional, for tests only

Knowledge base format

A .kb file has two sections separated by comments:

# TBox
Donkey ≡ Animal ⊓ ∀hasParent.Donkey
⊤ ⊑ ¬Donkey ⊔ ¬Horse

# ABox
ben:Mule
(ben,carl):hasParent

Symbols: ⊤ ⊥ ¬ ⊓ ⊔ ∃ ∀ . ⊑ ≡

Operator precedence (tightest first): ¬, ∃r. / ∀r., ⊓, ⊔

Assertions:

• Concept assertion: individual:Concept
• Role assertion: (subject,object):role

Running the algorithm

Automatic — runs the full proof tree and prints the result:

python main.py examples/donkey-horse.kb

Interactive — step through rule applications one at a time:

python main.py --interactive examples/donkey-horse.kb

In interactive mode, enter a rule index to apply that rule, a to finish automatically from the current state, or q to quit.

Python API

from tableau import (
    KnowledgeBase, TableauState,
    applicable_rules, apply,
    build_proof, is_consistent,
    display_state, display_rules, display_step, display_trace, display_result,
    prefer_deterministic,
)

# Load a knowledge base
kb = KnowledgeBase.from_file("examples/donkey-horse.kb")
print(kb)                              # write it back to text

# Create the initial tableau state
state = TableauState.from_kb(kb)

# --- Step-by-step ---
rules = applicable_rules(state)        # list what can fire
print(display_rules(state))            # show them with indices
rule = rules[0]                        # pick one (or use a heuristic)
next_states = apply(state, rule)       # get successor state(s)
print(display_step(rule, state, next_states))

# --- Full automatic ---
proof = build_proof(state, heuristic=prefer_deterministic)
print(display_trace(proof))
print(display_result(proof))

Plugging in a custom heuristic

A heuristic is any callable (state, rules) -> rule:

import random

def random_choice(state, rules):
    return random.choice(rules)

proof = build_proof(state, heuristic=random_choice)

Built-in heuristics: prefer_deterministic (default), first_applicable, prefer_branching.

Tableau rules

The implementation follows Baader, Horrocks, Lutz & Sattler (2017), Introduction to Description Logic, Cambridge University Press, §2.3.

Preprocessing

Before the search starts, every ABox assertion is converted to Negation Normal Form (NNF): negations are pushed inward until they rest only on atomic concept names, using the standard equivalences

¬(C ⊓ D) ↝  ¬C ⊔ ¬D        ¬(C ⊔ D) ↝  ¬C ⊓ ¬D
¬(∃r.C)  ↝  ∀r.¬C           ¬(∀r.C)  ↝  ∃r.¬C
¬¬C      ↝  C                ¬⊤       ↝  ⊥        ¬⊥ ↝ ⊤

The algorithm maintains the ABox in NNF throughout, so negations only ever appear on atomic concepts in a running proof.

Clash

A state is clashing (inconsistent) if it contains, for some individual a:

• a:⊥, or
• both a:C and a:¬C for any concept C.

Structural rules (no TBox)

Rule	Condition	Adds
⊓-rule	a:(C⊓D) in ABox	a:C, a:D
⊔-rule	a:(C⊔D) in ABox	branch: a:C | a:D
∃-rule	a:∃r.C in ABox, no r-successor of a already typed C	fresh b; (a,b):r, b:C
∀-rule	a:∀r.C and (a,b):r in ABox	b:C

TBox unfolding rules (lazy unfolding)

Concept names are expanded only when they actually appear in the ABox — hence lazy. The TBox must be acyclic and definitional (each concept name defined at most once; no general concept inclusions).

Rule	Condition	Adds
⊑-rule	a:A in ABox, A ⊑ C in TBox	a:C
≡-rule (positive)	a:A in ABox, A ≡ C in TBox	a:C
≡-rule (negative)	a:¬A in ABox, A ≡ C in TBox	a:NNF(¬C)

The negative ≡-rule converts ¬C to NNF before adding it, keeping the ABox representation invariant.

Termination and completeness

Because the TBox is acyclic (definitions form a DAG), every unfolding step strictly replaces a concept name with a structurally simpler concept, so the rules cannot fire forever. The rule set is sound and complete for ALC consistency with acyclic definitional TBoxes.

Acyclicity

The lazy-unfolding algorithm is only guaranteed to terminate on acyclic TBoxes. A TBox is acyclic when no concept name directly or transitively appears in its own definition.

from tableau import KnowledgeBase, is_acyclic

kb = KnowledgeBase.from_file("examples/donkey-horse.kb")
kb.is_acyclic()   # False — Donkey ≡ Animal ⊓ ∀hasParent.Donkey is cyclic

kb2 = KnowledgeBase.from_file("examples/forall-chain.kb")
kb2.is_acyclic()  # True

is_acyclic builds a dependency graph (edge A → B when B appears in A's definition) and checks it for directed cycles using DFS. The standalone function works directly on a TBox list:

from tableau import is_acyclic, concept_names_used
from tableau.syntax import AtomicConcept, Equivalence, Universal

A = AtomicConcept("A")
tbox = [Equivalence(A, Universal("r", A))]
is_acyclic(tbox)        # False — A depends on itself
concept_names_used(Universal("r", A))  # frozenset({"A"})

Benchmarking heuristics

examples/benchmark.py generates random acyclic KBs and compares every registered heuristic by counting total rule applications across the proof tree. Fewer rules = more efficient search.

python examples/benchmark.py                          # 20 KBs, random seed
python examples/benchmark.py --seed 42                # reproducible run
python examples/benchmark.py --num-kbs 100 --seed 7 --verbose

Sample output (30 KBs, seed 42):

Knowledge bases generated : 30  (generator seed=42)
Consistent                : 21/30
Heuristics differ         : 23/30  (rule count varies)

Heuristic                Total    Avg/KB
──────────────────────────────────────────
prefer_deterministic      1019     33.97  ◀ fewest
first_applicable          1019     33.97
random(seed=42)           1976     65.87
prefer_branching          2831     94.37

To add your own heuristic, write a function with the signature (state, rules) -> rule and add it to the HEURISTICS dict in benchmark.py.

Python API for metrics

from tableau import KBGenerator, GeneratorConfig, compare_heuristics, count_rule_applications
from tableau import prefer_deterministic, make_random

gen = KBGenerator(GeneratorConfig(seed=42))
kb  = gen.generate()

results = compare_heuristics(kb, {
    "deterministic": prefer_deterministic,
    "random_42":     make_random(seed=42),
})
for r in results:
    print(r.heuristic_name, r.consistent, r.rule_applications)

The --seed flag seeds both the KB generator and the random heuristic so every run is fully reproducible.

Running the tests

pytest

Cross-validation against HermiT

The hermit test suite checks that our algorithm agrees with HermiT on every KB it can handle. HermiT is invoked as a subprocess (java -jar HermiT.jar); the JAR is located automatically via owlready2's bundled copy, and the java executable via jdk4py (both in the dev extras — no separate JDK required).

The random-seed tests are embarrassingly parallel. Running with -n auto distributes them across all CPU cores so the entire suite finishes in roughly two rounds of parallel JVM processes instead of running sequentially.

Run the cross-validation suite (sequential):

pytest -m hermit --hermit -v

Run in parallel across all available cores (recommended):

pytest -m hermit --hermit -v -n auto

Cyclic KBs (such as donkey-horse.kb) are validated against HermiT but skipped for our algorithm, because the lazy-unfolding algorithm is not guaranteed to terminate on cyclic TBoxes.

Example files

File	Expected result
examples/donkey-horse.kb	inconsistent
examples/disjunctive-tbox.kb	consistent
examples/forall-chain.kb	consistent
examples/exists-clash.kb	inconsistent

Development

Install the dev extras (includes pytest, ruff, mypy, owlready2, pytest-xdist):

pip install -e ".[dev]"

Lint and format (Ruff — fast, replaces flake8 + isort + pyupgrade):

ruff check --fix .
ruff format .

Type check (mypy):

mypy tableau

Full test suite with coverage:

pytest --cov=tableau --cov-report=term-missing

Git hooks (pre-commit — runs ruff and mypy automatically on every commit):

pip install pre-commit
pre-commit install