rustdl

A sound OWL 2 DL (SROIQ) reasoner in Rust. Konclude-style hybrid: a consequence-based saturation engine handles the EL-ish fragment, a tableau + hypertableau wedge handles the rest of SROIQ, and an orchestrator picks per query. Parsing and the OWL model come from horned-owl.

Status

A working classifier, consistency checker, and instance reasoner for SROIQ(D) with first-class data properties.

• Sound. Every reported subsumption is a genuine entailment.
• Consistent. Consistency via a consequence-based ABox-saturation pre-check plus the tableau.
• Completeness. On the EL/Horn fragment with no timeout the hierarchy is complete by construction; beyond it the classifier trusts the wedge's Sat verdicts — empirically near-complete on the measured corpus, not provably complete.
• Proofs. A step-level, rule-by-rule proof tree for any entailment — a checkable certificate of soundness on the EL/Horn fragment.
• Explain. A minimal responsible-axiom set for any entailment, narrowable to the responsible fragment.
• Repair. Root-cause diagnosis of unsatisfiability plus minimal, verified fixes.
• Report. A self-contained HTML report bundling the explanations, diagnosis, and repairs.

Coverage

Supported (sound; complete on the EL/Horn fragment where the guarantee holds — see completeness note):

• SROIQ object-property reasoning — role hierarchies; transitive, symmetric, asymmetric, irreflexive, functional, inverse-functional; inverse roles; role chains (longer chains decomposed to 2-leg cascades).
• Class expressions — intersection, union, complement, nominals ({a}), existential / universal restrictions, qualified cardinality (≥n R.C, ≤n R.C).
• DisjointClasses, EquivalentClasses, DisjointUnion.
• ABox — ClassAssertion, ObjectPropertyAssertion, NegativeObjectPropertyAssertion, SameIndividual, DifferentIndividuals; consistency via an ABox-saturation pre-check + clash-pattern checks.
• Data properties are first-class (default-on) — data-property axioms lower to the object fragment; concrete domains cover integer / float / decimal / date / dateTime / string value-membership, faceted ranges, DataOneOf, flat DataUnionOf / DataIntersectionOf / DataComplementOf, and bounded data cardinality.

Inferred queries beyond classification (reasoner API + CLI --json + Python): object/data property hierarchy, property values, same / different individuals, disjointness, and complex (anonymous Manchester) class-expression satisfiability / entailment / instances — all sound, each reporting an incomplete flag.

Sound under-approximation (dropped and reported, never an error): any axiom the conversion can't represent — the narrow datatype tail (nested composite ranges like DataComplementOf(DataUnionOf(…)), ∀ / range / cardinality over a union or complement, unparseable / cross-datatype literals), plus HasKey, SWRL rules, and other unsupported constructs. Reasoning proceeds over the supported fragment; the dropped axioms are surfaced as a count-by-kind diagnostic (dropped_axioms, a dropped block in --json, a stderr warning). Positives depending on them may be missed, never falsely asserted.

Crates

owl-dl-core (IR + normalization), owl-dl-saturation (EL closure), owl-dl-tableau (SROIQ tableau + hypertableau wedge), owl-dl-datatypes (concrete domains), owl-dl-reasoner (orchestrator + public API), owl-dl-verify (diagnostic-only: an independent finite-model check of the EL closure, pure-EL only, not wired into any reasoning path), owl-dl-cli (rustdl binary), owl-dl-bench (corpus/benchmark harness), owl-dl-py (Python bindings). xtask holds build automation.

Quickstart

Python

pip install rustdl          # Python 3.10+, prebuilt ABI3 wheels

import rustdl

# classify — input format (OFN / OWX / RDF-XML / Manchester .omn) is auto-detected.
# Bounded by default: per_pair_timeout_ms=100, global_timeout_ms=60000 (ms).
result = rustdl.classify("ontology.ofn")
print(f"{len(result.classes)} classes, {len(result.unsatisfiable)} unsatisfiable")
result.complete                                                # False if a timeout cut any pair
result.is_subclass("http://ex.org/Sub", "http://ex.org/Sup")   # -> bool
result.direct_subsumers("http://ex.org/Sub")                   # -> list[str]

# Tune the budgets (ms) — each cut pair defaults to "not subsumed" (sound); 0 disables a bound:
rustdl.classify("ontology.ofn", per_pair_timeout_ms=25, global_timeout_ms=30000)
rustdl.classify("ontology.ofn", per_pair_timeout_ms=0, global_timeout_ms=0)   # unbounded = complete

rustdl.is_consistent("ontology.ofn")   # -> bool
rustdl.debug("ontology.ofn")           # consistency + root/derived unsat + justifications + repairs

# justify one entailment, or many against the same ontology (prepare once, reuse):
rustdl.justify("ontology.ofn", ["unsat", "http://ex.org/Bad"])   # -> list[str] (Manchester)
onto = rustdl.prepare("ontology.ofn")            # parse + per-ontology justification state
onto.justify(["subclass", sub, sup])             # same result, without re-deriving it
onto.justify_all(["unsat", cls], max=10)         # up to `max` minimal justifications

prepare pays the per-ontology setup once — use it whenever you justify more than one entailment of the same ontology (the returned object is single-threaded: use it from the thread that created it).

More surface — inferred property assertions, subproperty axioms, existential successors, justify/repair — in the end-to-end QA tutorial.

Rust

cargo add rustdl   # in-process library — no JVM, no subprocess

The rustdl crate is an umbrella that re-exports owl-dl-reasoner's API and the exact horned-owl it is built against, so one dependency suffices. Depending on owl-dl-reasoner directly also works, but then pin horned-owl@1.4 explicitly: it requires ^1.4, while a bare cargo add horned-owl resolves the latest major (3.x), which Cargo installs alongside 1.4 — and the SetOntology<RcStr> built with 3.x is a different type from the one classify accepts, so the example below fails with a type mismatch.

use rustdl::classify;
use rustdl::horned_owl::io::ParserConfiguration;
use rustdl::horned_owl::io::ofn::reader::read as read_ofn;
use rustdl::horned_owl::model::RcStr;
use rustdl::horned_owl::ontology::set::SetOntology;

let src = std::fs::read_to_string("ontology.ofn")?;
let (onto, _): (SetOntology<RcStr>, _) =
    read_ofn(&mut std::io::Cursor::new(src), ParserConfiguration::default())?;

let h = classify(&onto)?;                          // full class hierarchy
println!("{} classes", h.classes().len());
h.is_subclass("http://ex.org/Sub", "http://ex.org/Sup");   // -> bool
for parent in h.direct_subsumers("http://ex.org/Sub") {
    println!("{parent}");
}

Bounded variants (classify_with_budget, classify_with_timeout) and consistency / instance queries live in the same crate; see cargo run -p owl-dl-reasoner --example embed_classify. For the command-line tool instead, see CLI.

Build & test

cargo build --workspace --release     # Rust 1.88+, edition 2024
cargo fmt --all -- --check
cargo clippy --workspace --all-targets --all-features -- -D warnings
cargo test --workspace

CLI

Prebuilt binaries for Linux (x86-64/aarch64, musl-static), macOS (aarch64) and Windows (x86-64) are attached to every release — that is the supported way to get rustdl.

cargo install owl-dl-cli no longer works, on purpose. All five versions 0.1.0–0.3.0 were yanked on 2026-09-04, so the command now fails with error: could not find owl-dl-cli in registry crates-io with version * instead of silently installing the 0.3.0 from 2026-06-05 — a binary predating every soundness and completeness fix since June. The crate is deliberately unpublished going forward (it depends on a [patch.crates-io] fork of horned-owl, so a crates.io build would not compile), and it was frozen at 0.3.0 while the project reached 0.4.26.

A loud failure is the point: the warning that used to live here only reached people who read it, and cargo install owl-dl-cli is precisely what someone types instead. All five had to go, not just 0.3.0 — yanking only the newest would have made cargo install fall back to 0.2.2, which is older. Yanks are reversible (cargo yank --undo) and nothing depended on the crate (0 reverse dependencies).

Get the CLI from the release binaries. The six published crates — the five libraries plus rustdl — ARE current.

To build from source instead:

cargo install --git https://github.com/MaastrichtU-IDS/rustdl owl-dl-cli   # builds the `rustdl` binary

rustdl classify  ontology.ofn               # full class hierarchy (default)
rustdl classify  ontology.ofn --pair-timeout-ms 25 --global-timeout-ms 60000  # bounded run
rustdl consistent ontology.ofn
rustdl subclass  ontology.ofn <sub> <sup>
rustdl instances ontology.ofn <class>
rustdl realize   ontology.ofn [--properties] # per-individual types (+ inferred object & data property assertions)

# inferred queries (each also available as `--json` and in the Python API):
rustdl disjoint          ontology.ofn                  # disjoint classes + disjoint object/data properties
rustdl individuals       ontology.ofn                  # inferred same / different individuals
rustdl property-hierarchy ontology.ofn                 # inferred object/data property hierarchy
rustdl property-values   ontology.ofn                  # inferred object/data property values
rustdl sat-expr          ontology.ofn '<CE>'           # satisfiability of a Manchester class expression
rustdl subclass-expr     ontology.ofn '<sub>' '<sup>'  # is SubClassOf(ce1, ce2) entailed
rustdl instances-expr    ontology.ofn '<CE>'           # instances of a Manchester class expression

rustdl justify   ontology.ofn <query…>      # minimal responsible-axiom set (why it holds)
rustdl justify --laconic ontology.ofn <query…>  # pinpoint the responsible PART of each axiom
rustdl repair    ontology.ofn <query…>      # minimal axiom removals to break an entailment
rustdl prove     ontology.ofn <sub> <sup>   # step-level DL proof tree
rustdl diagnose  ontology.ofn               # root vs derived unsatisfiable classes (where to start fixing)
rustdl report    ontology.ofn -o report.html # self-contained HTML debugging report
rustdl explain   ontology.ofn <sub> <sup>   # which engine answered (saturation vs tableau)
rustdl verify-el ontology.ofn [--json]      # diagnostic: build a finite model from the EL closure and
                                             # check the axioms it handles against it, via code
                                             # independent of the saturator

verify-el is a diagnostic, not a reasoning path — it is not wired into classify, consistent, or realize. It only runs on ontologies in the pure-EL fragment (exits 3, Unresolved, on anything else). Its independence is of CODE, not of input: the model it checks against is built from the saturator's own closure, and only 13 of the 25 Axiom variants have a check at all — everything else contributes an Unresolved row rather than a verdict. It exits 0 (Verified) when the model built from rustdl's own EL saturation closure satisfies every axiom it can check. A 2 (Violated) means the model built from the reported closure fails an axiom — a strong lead, not a proof: the model builder is itself an under-approximation in places, and every known imprecision found so far points toward a spurious violation, never toward a false all-clear (three reproduced cases in docs/known-limitations/verify-two-expansion-paths-split-a-witness.md). Exit 3 (Unresolved) covers several distinct routes, not just one: the model builder itself refusing outright (a bound tripped, or a construct outside the checker's covered fragment), a check-time axiom/concept shape the evaluator does not yet handle, content axioms silently dropped at conversion (before this checker ever saw them), or a Verified check result downgraded because of either of the last two — never treated as a clean Verified. 1 is an I/O/parse error.

Bounded classification — sound under-approximation (every reported subsumption still holds; pairs not decided in time default to "not subsumed", never a false one):

• --pair-timeout-ms N — cap each pairwise tableau probe (default 1000; 0 = unbounded). Good for pathological SROIQ where a few pairs never terminate.
• --global-timeout-ms N — bound the reasoning wall for the whole classify (0 = unbounded): each probe is cut at the smaller of the per-pair and global budgets, so total probing can't grow with the pair count. The fixed saturation + preprocessing overhead (seconds to tens of seconds on very large ontologies) is not deadline-gated, so the wall floor isn't zero.
• --saturation-only — skip the tableau entirely and report only the EL closure.

Any run that hits a bound prints a prominent INCOMPLETE warning to stderr. Diagnostics: RUSTDL_TRACE=1 (one stderr line per search/branch decision); RUSTDL_COUNTERS=1 with --features counters (per-rule call counts).

Protégé plugin

rustdl runs as a Protégé Desktop reasoner.

Install: download rustdl-protege-<version>.jar from the latest release, drop it into Protégé's plugins/ directory, and restart. Choose rustdl under Reasoner ▸, then Reasoner ▸ Start reasoner.

Computes (v1): consistency, the inferred class hierarchy, unsatisfiable classes, and class assertions (types / instances). Property hierarchies & values, same/different individuals, disjointness, and complex-class-expression queries return empty for now.

Config (JVM system property, else env var): -Drustdl.bin=… / RUSTDL_BIN for a specific binary; -Drustdl.timeout.seconds=… / RUSTDL_TIMEOUT_SECONDS (default 600) for the per-call timeout.

Requires Protégé 5.6.x (Java 11+). Build-from-source and the full contract: protege/README.md, docs/protege-plugin.md.

Licensing

Dual-licensed Apache-2.0 OR MIT. horned-owl is LGPL-3.0; binaries that statically link it inherit LGPL-3.0 obligations for that portion (see NOTICE). Contributions are accepted under the same dual license; no separate CLA.