git:20261015.e10ac19 to git:20261015.28e403b

16 added, 4 removed. Audit A to A.

---

name: inference

description: Use when you need RDFS, OWL 2 RL, or Notation3/EYE-rule entailment over a sparq RDF graph — materialize the deductive closure (forward-chaining), query the entailed triples, maintain the closure incrementally under inserts/deletes, get derivation proof-trees (why()), or check OWL inconsistency; backed by the sparq-reason crate. For the COMPLETE OWL 2 EL class-subsumption lattice (which RL is sound-but-incomplete for), use the separate opt-in sparq-reason-el classifier (CR1-CR5 saturation). For OWL 2 QL certain-answer query rewriting (PerfectRef over DL-Lite_R, EXPERIMENTAL, fail-closed CQ-shape gate), use the separate opt-in sparq-reason-ql crate.

---

# sparq-inference

`sparq-reason` is sparq's **opt-in** reasoning crate: it forward-chains the deductive closure (RDFS, OWL 2 RL, or user-supplied Notation3 rules) over dictionary-encoded triples and **materializes** the entailed facts so querying stays exactly as fast as before. The core engine carries zero reasoning code/cost unless you depend on this crate. Reasoning works at the `[Id;3]` (RDFS/OWL) or `n3::Term` (N3) level; you wire the result back into a `sparq_core::Graph` to query it.

## Quickstart

Add the dep (native targets only — see Gotchas):

```toml

[dependencies]

sparq-core = "0.1"

sparq-reason = "0.1" # default features include `parallel`

```

Parse → materialize the RDFS closure in place → build a queryable graph (the canonical seam, exactly what the CLI does):

```rust

use sparq_core::Graph;

use sparq_reason::{materialize, Profile};

// 1. Parse to (Dict, triples) WITHOUT building indexes yet.

let (mut dict, mut triples) = Graph::parse_to_triples(turtle_text, "turtle")?;

let base = triples.len();

// 2. Expand `triples` in place with every entailed triple. Returns NEW triple count.

let added = materialize(Profile::Rdfs, &mut dict, &mut triples);

eprintln!("RDFS: {base} -> {} triples (+{added} entailed)", triples.len());

// 3. Build the indexed graph from the materialized closure and query as usual.

let g = Graph::from_parts(dict, triples);

# Ok::<(), String>(())

```

CLI equivalent (materialize and optionally dump the closure as N-Triples):

```bash

cargo run --release -p sparq-cli -- reason ontology.ttl turtle rdfs # rdfs | owl | n3

cargo run --release -p sparq-cli -- reason ontology.ttl turtle owl out.nt # write full closure

cargo run --release -p sparq-cli -- query data.ttl turtle 'SELECT ...' --reason rdfs # reason then query

# OWL 2 EL classification — the class hierarchy RL cannot reach (opt-in `el` feature). Complete

# for E1+E2 only: the CLI omits `cdomain`, so concrete-domain axioms land in `skipped_axioms`.

cargo run --release -p sparq-cli --features el -- classify ontology.ttl turtle lattice.nt

cargo run --release -p sparq-cli --features el -- query ontology.ttl turtle 'SELECT ...' --reason el

```

## Key APIs

Re-exported from the crate root (`sparq_reason::…`):

```rust

// Which regime to materialize. OwlRl includes RDFS. `D` is opt-in (`d-entail` feature).

pub enum Profile { Rdfs, OwlRl, /* #[cfg(d-entail)] */ D }

impl Profile { pub fn parse(s: &str) -> Option<Profile>; } // "rdfs" | "owl" | "owl-rl" | "d"

// Batch materialization (expand in place; returns NEW triples; idempotent).

pub fn materialize(profile: Profile, dict: &mut Dict, triples: &mut Vec<[Id;3]>) -> usize;

pub fn materialize_rdfs (dict: &mut Dict, triples: &mut Vec<[Id;3]>) -> usize;

pub fn materialize_owl_rl(dict: &mut Dict, triples: &mut Vec<[Id;3]>) -> usize;

// Opt-in `profile` feature: closure growth/time by stable rule group.

pub fn materialize_profiled(profile: Profile, dict: &mut Dict, triples: &mut Vec<[Id;3]>)

-> (usize, profile::Report);

// Pass `profile::Profiler::with_progress(callback)` to `materialize_profiled_with`

// when progress notifications are required.

// D-entailment (datatype / value-space) — opt-in `d-entail` feature, `sparq_reason::dtype`.

// rdfD1 datatype-typing under a recognized datatype map; CORRECT TYPED value equality

// ("1"^^xsd:integer ≡ "1.0"^^xsd:decimal — canonical decimal, NOT an f64 fast path).

// `materialize(Profile::D, …)` uses the STANDARD map; pass a custom map via:

#[cfg(feature = "d-entail")]

pub fn materialize_d(d: &Recognized, dict: &mut Dict, triples: &mut Vec<[Id;3]>) -> usize;

#[cfg(feature = "d-entail")]

pub fn d_value_eq(lex_a: &str, dt_a: &str, lex_b: &str, dt_b: &str) -> bool; // value-space eq

#[cfg(feature = "d-entail")]

pub struct Recognized; // Recognized::standard() / ::new(iris) / ::default() (string+langString)

// OWL inconsistency check (cax-dw / cls-com / eq-diff / cls-nothing clashes) — run AFTER OWL closure.

pub fn inconsistencies(dict: &Dict, triples: &[[Id;3]]) -> Vec<String>;

// Notation3 / EYE-style forward rules (`{ premise } => { conclusion }` + builtins).

pub fn reason_n3(dict: &mut Dict, src: &str) -> Result<Vec<[Id;3]>, String>;

pub fn reason_n3_proof(dict: &mut Dict, src: &str)

-> Result<(Vec<[Id;3]>, Vec<ProofStep>), String>; // EYE --proof analogue; each step also carries conclusion_key / premise_keys (N3 statement_keys, taken before list expansion + interning)

pub fn reason_n3_proof_run(dict: &mut Dict, src: &str) -> Result<N3ProofRun, String>; // { closure, closure_keys (every fact, asserted too), steps } — for explain::n3_proof_tree

pub fn reason_n3_terms(src: &str, base: Option<&str>) -> Result<N3Closure, String>; // term-level, no Dict

// N3Closure { facts, derived, n_rules, n_backward_rules, warnings: Vec<String> } — `warnings`

// carries the stratification diagnostic of an opted-in negation cycle (see below).

// Every N3 entry point STRATIFIES store-scoped negation automatically (GH #6201): a rule whose

// log:notIncludes / log:collectAllIn / log:forAllIn negates a predicate the same document

// derives runs after that predicate's fixpoint. Per-PREDICATE analysis (per CLASS for

// `rdf:type` with a constant class; a variable class overlaps every class), fail-closed by

// construction: a `{ … }` literal scope reads its own atoms; anything not pinned to one IRI

// predicate (variable premise/conclusion predicate, clause given by a variable, nested

// log:conclusion / log:supports closure) counts as EVERY predicate; list builtins depend on

// rdf:first/rdf:rest. Every negation/aggregation evaluation also passes ONE gate that refuses

// a store some search cut short (backward depth limit, containment budget, list-walk cap,

// a regex the engine cannot compile, import-cycle-unclosed nested closure, a log:semantics /

// log:parsedAsN3 document past the parser's nesting limit, a log:semantics / log:content IRI

// with no resolver or one that returns nothing, a date field that overflows, exact math:

// arithmetic past i128 — the value still falls back to f64; i128::MIN % -1 is 0; the flag is

// shared across nested closures, explicit strata and a query's data closure): the run errors

// unless SinglePass. A syntax error in a parsed document is a plain no-match, not a cut.

// A log:includes / log:notIncludes / log:supports PATTERN given through a variable is

// matched, with a { … } formula (or {}) as the scope, as the stored formula the variable

// is DIRECTLY bound to, as stored, only when that formula holds NO variable at any depth

// (blank nodes are its existentials), exactly as if written in the rule (GH #6936); its

// statements are charged to max_join_rows. Any other value (a formula holding a variable,

// so a chained binding is not followed; a non-formula value; an unbound variable), and

// EVERY bound pattern with the STORE as the scope, matches as the EMPTY pattern (includes

// holds, notIncludes fails), as before; full matching is

// https://github.com/sparq-org/sparq/issues/6943; write such a pattern in the rule. Each

// containment matches its blanks afresh (no witness carries over to the next one).

// time: builtins return exact integers (time:inSeconds both ways; a fraction or a

// value past i64 it would drop is a cut), and string:format's %f renders exact numbers

// from their digits. Every builtin and virtual relation declares

// what it reads from the store (`StoreRead`, exhaustive per registry entry); rules whose

// premise reads outside its joins (scopes, list walks over a stored list, virtual

// rdf:first/rest over a variable subject, a variable predicate, backward rules) re-run in

// full each round, and a stratum that a later negation/aggregation (or a caller: query,

// next explicit stratum) reads closes with a full naive round. A cycle through

// negation (e.g. `a ?c` concluded beside a negated `a :Flagged`, or a variable-predicate

// conclusion beside store-scoped negation) is an ERROR by

// default at every entry point, nested closures included; only the rules on/after the cycle

// are affected by an opt-in:

pub fn reason_n3_terms_with_cycles(src, base, resolver, cycles: NegationCycles)

-> Result<N3Closure, String>;

pub fn reason_n3_with_cycles(dict: &mut Dict, src: &str, cycles: NegationCycles)

-> Result<Vec<[Id;3]>, String>;

pub enum NegationCycles { Reject /* default */, FailClosed /* skip them + warning */,

SinglePass /* legacy, may fail open + warning */ }

pub fn reason_n3_terms_with_resolver(src, base, resolver: Option<&Resolver>) -> Result<N3Closure, String>; // n3:: only

// Every forward closure has a round, fact and derived-term-size allowance (see Gotchas).

// These two take the caller's, as do MaterializedN3Graph::with_limits and compiled::eval_with_limits;

// every other N3 entry point uses ClosureLimits::default().

#[non_exhaustive] // build from Default, then set fields: `let mut l = ClosureLimits::default(); l.max_term_bytes = …;`

pub struct ClosureLimits { pub max_rounds: usize /* 1_000_000 */, pub max_facts: usize /* 50_000_000 */,

pub max_term_bytes: usize /* 16 MiB per derived term */,

pub max_join_rows: usize /* usize::MAX (unbounded, opt-in): binding rows + firings per round (GH #6938) */ }

pub fn reason_n3_terms_with_limits(src, base, resolver, cycles: NegationCycles, limits: ClosureLimits)

-> Result<N3Closure, String>;

pub fn reason_n3_with_limits(dict: &mut Dict, src: &str, cycles: NegationCycles, limits: ClosureLimits)

-> Result<Vec<[Id;3]>, String>;

// EYE --pass-all / --pass-all-ground: the closure PLUS the document's own rules, echoed

// back as ONE N3 document (the chainer consumes rules, so --pass output alone can derive

// nothing further). Closure statements are sorted (deterministic), then rules in document

// order — full <…> IRIs, no @prefix reconstruction, so NOT byte-identical to EYE's writer.

// Each document-level @forAll universal (one variable per IRI, ?__ua.<iri>) is declared ONCE, on

// a document @forAll line before the first fact/rule using it; units are ordered so every plain

// mention of the IRI comes first. A formula-level one (GH #6754) is declared inside the formula that

// binds it, right before the first statement that uses it. Err (besides a parse error) when the document could not re-reason exactly

// as the input: a unit mixing a plain mention and the universal (or a cycle of such units), a

// plain mention after the universal's declaration in its formula, a shadowed mention, a

// backward-chaining copy of a universal (__bw<n>___ua.<iri>: its only spelling reads back as

// the universal, which log:equalTo tells apart), or any term the parser would normalize (the

// WHOLE document is re-parsed and compared, universals by exact name). No fallback spelling.

pub fn reason_n3_pass_all(src: &str, vars: RuleVars) -> Result<String, String>;

// n3::serialize — EXACT writers (output parses back to the same terms, or Err; never lossy):

pub fn write_term(t: &Term, out: &mut String) -> Result<(), NotRepresentable>; // + write_statement(&[Term;3], out)

pub fn write_rule(r: &Rule, kind: RuleKind, vars: RuleVars, out: &mut String) -> Result<(), NotRepresentable>;

pub fn serialize_facts<'a>(facts: impl Iterator<Item = &'a [Term; 3]>) -> Result<String, NotRepresentable>; // whole text verified at once

// write_rule / write_term refuse a document-level @forAll universal (only a document can declare

// it); a formula-level one is written under its formula's own @forAll.

pub enum NotRepresentable { UnrepresentableScope(String), MergesVariables(String), Unspellable(String), Reparse(String) } // Display + Error

pub fn display_lossy(t: &Term) -> String; // DISPLAY only (diagnostics); never re-parse it

pub fn statement_display_lossy(f: &[Term; 3]) -> [String; 3]; // proof-node strings; display only

pub fn statement_keys(f: &[Term; 3]) -> [String; 3]; // structural identity key per term (injective)

// EYE --query: every INSTANTIATED conclusion of the query document's forward rules over the

// deductive closure of `data` — a PROJECTION, so a conclusion already in the closure is still

// an answer (unlike --pass-only-new). The premise uses the chainer's own matcher, so builtins,

// quoted `{ … }` formulae and `( … )` lists all work. The query document's FACTS are not loaded

// as data; its `<=` rules ARE available to the premise. No forward rule => error, not "".

// Stratification covers the evaluated set (data rules + both documents' `<=` rules + query

// premises): a negation cycle a query-supplied `<=` rule closes is an error.

pub fn reason_n3_query(dict: &mut Dict, data: &str, query: &str) -> Result<Vec<[Id;3]>, String>;

pub fn reason_n3_query_terms(data: &str, query: &str) -> Result<Vec<[Term;3]>, String>; // term-level

pub enum RuleVars { N3, VarIris } // `?x` (re-parses as the same rule, so re-running is a

// fixpoint) | SWAP `var:` IRIs (`--pass-all-ground`: no `?x` survives in a RULE, at any

// depth — quoted `{ … }` formulae included — but the rule is then constants; the grounded

// form is for RDF consumers, not re-reasoning)

pub fn reason_n3_stratified(dict: &mut Dict, strata: &[&str]) // stratum-by-stratum closure; carries

-> Result<StratifiedN3Closure, String>; // each closure in memory (no re-serialize); the sound

// driver for pipelines shipped as separate documents; each stratum is still checked on

// its own, so a stratum that negates through its own conclusions needs

// reason_n3_stratified_with_cycles(.., SinglePass) and caller-guaranteed completeness;

// per-stratum blank scope. Fields: facts (final interned closure), strata_facts (sizes),

// warnings (each stratum's cycle diagnostic).

pub fn reason_n3_stratified_with_cycles(dict, strata, cycles: NegationCycles)

-> Result<StratifiedN3Closure, String>; // same, with the per-stratum cycle opt-in;

// under FailClosed a stratum that skipped rules carries an INCOMPLETE closure, so any

// negation/aggregation in a later stratum refuses it and the run errors.

// Incremental closure maintenance (closure stays == from-scratch materialize on the current base).

pub struct MaterializedGraph; // RDFS; mutations are dictionary-free

impl MaterializedGraph {

pub fn new(dict: &mut Dict, base: &[[Id;3]]) -> Self;

pub fn insert(&mut self, triples: &[[Id;3]]) -> usize; // returns # actually added

pub fn delete(&mut self, triples: &[[Id;3]]) -> usize; // exact-count retraction; as cheap as insert

pub fn contains(&self, t: &[Id;3]) -> bool;

pub fn closure(&self) -> Vec<[Id;3]>; // sorted, deduped

pub fn iter(&self) -> impl Iterator<Item=[Id;3]> + '_;

pub fn full_rebuilds(&self) -> usize; // TBox edits => full rematerialize

}

pub struct MaterializedOwlGraph; // OWL 2 RL; insert/delete take &mut Dict (fallback path interns)

impl MaterializedOwlGraph { pub fn new(dict: &mut Dict, base: &[[Id;3]]) -> Self;

pub fn insert(&mut self, dict: &mut Dict, triples: &[[Id;3]]) -> usize;

pub fn delete(&mut self, dict: &mut Dict, triples: &[[Id;3]]) -> usize;

pub fn mode(&self) -> OwlMode; /* + contains/closure/len/full_rebuilds */ }

pub enum OwlMode { CountingMono, CountingFixpoint, Fallback }

pub struct MaterializedN3Graph; // user N3 rules; operates on n3::Term facts

impl MaterializedN3Graph { pub fn new(rules_src: &str, base_facts: &[[Term;3]]) -> Result<Self, String>;

pub fn with_limits(rules_src: &str, base_facts: &[[Term;3]], limits: ClosureLimits)

-> Result<Self, String>; // new uses ClosureLimits::default() (GH #6854)

pub fn insert(&mut self, facts: &[[Term;3]]) -> usize; // variables allowed only inside formula values

pub fn delete(&mut self, facts: &[[Term;3]]) -> usize;

pub fn mode(&self) -> N3Mode; // Counting (incremental) | Fallback (re-runs engine)

pub fn fallback_reason(&self) -> Option<&str>; // None <=> counting path active

pub fn closure(&self) -> Vec<[Term;3]>; /* + contains/len/full_rebuilds */ }

pub enum N3Mode { Counting, Fallback }

// `explain` feature only (see Gotchas): one derivation witness as a flat DAG.

pub fn why(&self, dict: &Dict, t: [Id;3]) -> Option<ProofTree>; // RDFS / OWL graphs

pub fn why(&self, fact: &[Term;3]) -> Option<ProofTree>; // N3 graph

pub struct ProofTree; // .nodes() -> &[ProofNode], .root(), .conclusion(), .to_json(), .to_text()

pub struct ProofNode { pub conclusion: [String;3], pub key: [String;3], pub rule: String, pub premises: Vec<u32> } // conclusion = display; key = lossless fact identity (N3: two facts can render alike; the same key from why() and n3_proof_tree) — address facts by key

// explain::n3_proof_tree(dict, &run /* N3ProofRun */, target_ids, opts) -> Result<Option<ProofTree>, AmbiguousN3Target>

// — Err when several structurally distinct closure facts (asserted OR derived) intern to target_ids

// (e.g. () and an rdf:nil IRI); explain::n3_proof_tree_for_key(dict, &run.steps, &key, opts) roots by key.

// statement_keys is injective w.r.t. Term's own Eq: formula rows keep their order and duplicates (as the

// engine compares them); blank labels and __bw copies are not normalized. So a key is only as

// reproducible as the engine's terms. Skolem labels (__sk<n>_e) are numbered in the sorted order

// of each round's firing keys (every variable the conclusion substitutes), so for the SAME parsed

// input the labels and the structural keys of facts carrying them do not depend on hash-set

// traversal or hasher width (native vs wasm32; GH #6749). why() proof steps are covered too:

// where a round derives ONE fact several ways - one rule firing under distinct bindings, two

// different rules, or the transitivity fast path over several intermediate paths - the step

// records the derivation with the least premise vector, not whichever arrived first (GH

// #6844). E.g. with :a :p :v. :b :p :v. and rules

// ?x :p :v => ?x :q :v, ?x :q :v => :m :r :v, :m :r :v => :m :s _:e, the :m :s label and key

// are stable AND its why() tree always cites the same :q witness. A log:conclusion formula's

// derived rows, and the rdf:first/rest cell labels interning a list value mints (_l<k>_<n>),

// are likewise sorted / numbered in a canonical term order, not in a fact set's traversal order.

// Labels are still NOT canonical across reordered isomorphic

// documents (anonymous parser blanks are _b<n> in arrival order, formula rows keep source order,

// and a label depends on the other firings in its round), and they hold only while the binding

// values and firing sets are themselves stable. Values that still carry traversal order -

// log:collectAllIn lists, and backward-renamed __bw<n> terms (that counter is still assigned in

// evaluation order) - can reorder ranks and so labels (GH #6844).

pub struct ExplainOpts { pub max_depth: usize, pub max_nodes: usize } // why_with(.., opts)

```

`Id` / `Dict` come from `sparq_core::dict`; `N3Closure`, `ProofStep`, `RuleVars` from `sparq_reason::n3` (re-exported at the crate root); `Term`, `Rule`, `Resolver` and `reason_n3_terms_with_resolver` are reached through `sparq_reason::n3::…`.

```rust

// `compiled-rules` feature only (`sparq_reason::n3::compiled`, sq-zgbso.3): id-level

// COMPILED N3 evaluation for the access-control subset — no per-call text round-trip

// (the rule IR pre-interns its constants into the caller's Dict; the fixpoint joins run

// on the shared sparq-substrate kernels over [Id;3] facts).

pub fn compile(src: &str) -> Result<CompiledRuleSet, String>; // parse + lower ONCE

pub fn eval(dict: &mut Dict, facts: &[[Id;3]], rules: &CompiledRuleSet) -> Result<Vec<[Id;3]>, String>;

pub fn eval_with_limits(dict: &mut Dict, facts: &[[Id;3]], rules: &CompiledRuleSet, limits: ClosureLimits)

-> Result<Vec<[Id;3]>, String>; // eval uses ClosureLimits::default() (GH #6855)

pub fn intern_facts(dict: &mut Dict, src: &str) -> Result<Vec<[Id;3]>, String>; // test/harness fact loader

impl CompiledRuleSet { pub fn bind(&self, dict: &mut Dict) -> BoundRuleSet<'_>; // intern the symbol table

pub fn n_rules(&self) -> usize; pub fn n_facts(&self) -> usize;

pub fn n_strata(&self) -> usize; } // automatic stratification, as reason_n3;

// compile() errors on a negation cycle

pub fn compile_with_cycles(src: &str, cycles: NegationCycles) -> Result<CompiledRuleSet, String>;

impl BoundRuleSet<'_> { pub fn eval(&self, dict: &mut Dict, facts: &[[Id;3]]) -> Result<Vec<[Id;3]>, String>;

pub fn eval_with_limits(&self, dict: &mut Dict, facts: &[[Id;3]], limits: ClosureLimits)

-> Result<Vec<[Id;3]>, String>; }

```

Compiled-rules scope is EXACTLY the WAC/ACP/ODRL-spike corpus subset (store-scoped `log:notIncludes`, stratified automatically like `reason_n3`, whose subject must be an IRI, a non-`true` literal, or a variable used only as a `log:notIncludes` subject — `{}` (the empty formula) or a bindable subject is a `compile` error, `log:uri`, `log:(not)equalTo`, `string:` concatenation / encodeForUri / scrape (a regex that cannot compile is a `compile` error) / notGreaterThan) **plus RDF 1.2 triple terms in premises** (`sq-6d43t`); anything else is a loud `compile` error — full N3 stays with `reason_n3`. Closure set-equality vs `reason_n3` is pinned by `crates/sparq-reason/tests/compiled_equivalence.rs`.

**Compiled-rules limits (GH #6855).** `eval` runs under the text engine's `ClosureLimits` (`eval_with_limits` takes them; `eval` uses the default) and returns the text engine's `Err("n3: forward closure limit exceeded …")`, never a truncated closure. Each term a builtin builds is sized before it is built, with the text engine's helpers: the `( … )` argument list `string:concatenation` / `string:scrape` would substitute, then the result (concatenation, including its numeric pieces, `string:encodeForUri`, `string:scrape`, `log:uri` both ways). Conclusions copy ids the premise bound and build no new term. Both engines are bounded by the same limits and refuse with the same error, but their fixpoint schedules differ (the text engine's closing naive check round and transitivity fast path, and its quoted-triple substitution checkpoints, which have no compiled counterpart), so under equal `ClosureLimits` they can accept or refuse differently near a boundary. `compiled_equivalence.rs` checks that they agree at the limits it sweeps (`max_term_bytes`, `max_rounds`, `max_facts`) on its fixtures, and `n3_join_work_limits.rs` at every `max_join_rows` it sweeps.

**Compiled-rules triple terms (`sq-6d43t`).** A GROUND `<< s p o >>` is an ordinary symbol-table constant anywhere (fact, pattern position, builtin argument, conclusion): `bind` interns it through the Dict's content-addressed RDF 1.2 triple-term path, so it resolves to the SAME id a store-loaded `<<( s p o )>>` carries. A quotation that still contains VARIABLES is admitted in PREMISE positions and compiles to a component-indexed unpack step — the enclosing join binds the candidate's triple-term id, then the unpack reads its three component ids straight out of the dictionary record (no term reconstruction, no allocation) and binds first occurrences / filters already-bound variables and constants, left to right, nesting through the OBJECT. Three shapes are deliberately loud `compile` errors instead: a quotation with variables inside a `log:notIncludes` body (the anti-join runs a flat list of plain patterns), a quotation with variables in a CONCLUSION (minting a triple term from bound components can violate RDF 1.2's structural constraints at derivation time, which `eval` has no channel to report), and a nested quotation in SUBJECT position (no dictionary triple term can have a triple-term subject, so such a pattern could only ever fire zero times). Each falls back to `reason_n3`, which handles all three.

## RIF-Core rule front-end (opt-in `rif-core` feature, `sparq_reason::rif`)

The W3C RIF **Core** dialect — the **monotone Horn-rule** common subset of RIF-BLD/PRD — as a `rif::Document` rule front-end *over the same N3 forward chainer* (a faithful in-engine model that `validate`s for safety then lowers to N3; the proven `reason_n3` fixpoint computes the closure). Build with `features = ["rif-core"]`; **OFF by default**, so the lean/wasm build links zero RIF code (no new `Profile` variant — no match-arm churn anywhere).

```rust

# #[cfg(feature = "rif-core")] {

use sparq_reason::rif::{Atom, Builtin, Document, Rule, Term};

use sparq_core::dict::Dict;

// uncle(?n,?u) :- parent(?n,?p) , brother(?p,?u) — the canonical RIF Core rule (W3C rif01).

let mut doc = Document::new();

doc.push(Rule::fact(Atom::Frame { obj: Term::Iri("ex:Emeka".into()), pred: Term::Iri("ex:parent".into()), val: Term::Iri("ex:Oke".into()) }));

doc.push(Rule::fact(Atom::Frame { obj: Term::Iri("ex:Oke".into()), pred: Term::Iri("ex:brother".into()), val: Term::Iri("ex:Chi".into()) }));

doc.push(Rule::implies(

vec![Atom::Frame { obj: Term::Var("n".into()), pred: Term::Iri("ex:uncle".into()), val: Term::Var("u".into()) }],

vec![Atom::Frame { obj: Term::Var("n".into()), pred: Term::Iri("ex:parent".into()), val: Term::Var("p".into()) },

Atom::Frame { obj: Term::Var("p".into()), pred: Term::Iri("ex:brother".into()), val: Term::Var("u".into()) }],

));

let mut dict = Dict::new();

let _entailed: Vec<[sparq_core::dict::Id;3]> = doc.closure(&mut dict)?; // monotone forward-chaining closure

# }

# Ok::<(), Box<dyn std::error::Error>>(())

```

- **Atoms.** `Frame { obj, pred, val }` (`o[p->v]` → triple), `Member { obj, class }` (`o # c` → `rdf:type`), `Subclass { sub, sup }` (`c1 ## c2` → `rdfs:subClassOf`), `Equal { left, right }` (body-only; see Equal-atom semantics below), and `Builtin { op, args }` (body-only).

- **Equal-atom semantics (sq-pbz04.5.4 + sq-26vwp — RIF-Core fidelity; body Equal resolved at compile time, NEVER as an `owl:sameAs` triple):**

1. **Equal in a rule head is REJECTED** — `validate()` returns `RifError::EqualInConclusion`. This is the RIF-Core syntactic restriction (unlike RIF-BLD, Core does not permit equality in conclusions).

2. **`t = t` (identical after substitution) is eliminated** — `Equal { left: Term::Iri("x"), right: Term::Iri("x") }` (or `?n=?n`) is trivially true and dropped. It contributes NO bindings for range-restriction — if a head variable is SOLELY bound by a `?x=?x` atom, `validate()` rejects the rule with `UnboundHeadVar` (unifying a variable with itself binds nothing).

3. **`?x = t` (one side a variable) is SUBSTITUTED** — `t` replaces `?x` throughout head+body at validate/lower time, so `?x` becomes **bound-by-substitution** (`?x # C :- ?x = <a>` collapses to the fact `<a> # C`). **`?x = ?y` (two distinct variables) is UNIFIED** — one name is renamed to the other everywhere, so the join requires the SAME node: same-node reflexivity fires *without* any `owl:sameAs` assertion (fixes V2), and an asserted `owl:sameAs` between DISTINCT nodes never over-derives the equality (fixes V1). Substitution runs to a fixpoint, so chained `?x=?y, ?y=t` collapse both to `t`.

4. **Distinct GROUND constants — the NUMERIC half is DECIDED (sq-anyad), the rest fail closed.** When BOTH sides are well-formed numeric literals, the atom is decided by the shared substrate comparator `Num::cmp_relational` (sq-v5evr / #1646), across the XSD numeric tiers: value-EQUAL (`"1"^^xsd:integer = "1.0"^^xsd:decimal`) is eliminated like `t = t` so the rule fires, and value-UNEQUAL (`1 = 2`) makes the body unsatisfiable so the rule is **vacuous** — it validates, and derives nothing. The tower is exact only within an `i128` mantissa, so a well-formed `xsd:integer`/`xsd:decimal` beyond that range is classified out of it — such a pair is still DECIDED, not deferred: when both sides are exact-tier lexicals they are compared EXACTLY by `cmp_plain_decimal` string arithmetic (arbitrary precision, no `f64` promotion), so the same >`i128` value written with and without a leading `+` is equal and a pair differing by one below an f64 ulp is unequal. Everything else still returns `RifError::DistinctGroundEqual { left, right }`: the **non-numeric literal-equality half** (`pred:boolean-equal`, `pred:literal-not-identical` over strings/booleans/dates), an IRI or `List` operand (including a distinct ground *created* by substitution, e.g. `?x=<a>, ?y=<b>, ?x=?y`), an ill-formed numeric lexical — including one outside the value space of its declared **derived integer datatype**, so `"-1"^^xsd:positiveInteger` and `"128"^^xsd:byte` are refused rather than decided (the sign/bounds facets are checked at arbitrary precision, ahead of both the tower and the exact-lexical path) — a `NaN` operand (a comparator type error, not a verdict), and an out-of-tower exact-tier value paired with an `xsd:float`/`xsd:double` operand (which would need the float's exact decimal expansion). That half stays deferred — the front-end refuses rather than answering incorrectly. Vacuity never excuses an unsafe rule: range-restriction is checked even for an unsatisfiable body. No body `Equal` atom ever reaches N3 lowering — a stray one fails closed, never emits `owl:sameAs`.

- **Builtins (`rif::Builtin`).** Numeric predicates (`NumericEqual`/`LessThan`/`GreaterThan`/`NotLessThan`/`NotGreaterThan`/`NumericNotEqual`) + functions (`NumericAdd`/`Subtract`/`Multiply`/`Divide`), string predicates (`StringContains`/`StartsWith`/`EndsWith`) + functions (`StringConcat`/`StringLength`/`StringUpperCase`/`StringLowerCase`/`StringEncodeForUri`), and list `ListContains`/`ListLength`/`ListConcatenate` (variadic — `is_variadic()` returns `true`; `arity()` is the minimum). `is_filter()` distinguishes a predicate (all args inputs) from a function (last arg = computed output). Each lowers to the equivalent `math:`/`string:`/`list:` N3 builtin. A **deferral ledger** (`rif::UNIMPLEMENTED`) records builtins that are NOT mapped because no sound N3 target exists today (e.g. `func:numeric-integer-divide` truncation semantics, `pred:matches` XSD-regex vs Rust-regex dialect gap, date/time builtins lacking a temporal tower); those entries are tracked, never silently dropped.

- **Builtin SAFETY / range-restriction (enforced).** `Document::validate()` (also called by `to_n3_source`/`closure`) **rejects** an unsafe rule with a `RifError` rather than letting the chainer loop or over-derive: a head variable not bound by a positive body atom (`UnboundHeadVar`), a builtin *input* not range-restricted (`UnboundBuiltinInput`), a builtin in a head (`BuiltinInHead`), wrong arity (`BadBuiltinArity`), Equal in a head (`EqualInConclusion`), or distinct ground constants in a body Equal that numeric value-space equality cannot decide (`DistinctGroundEqual`).

- **MONOTONE — NAF is EXCLUDED by design.** RIF-Core is monotone Horn; negation-as-failure / RIF-PRD actions / aggregation are **not in the dialect** and are not representable in the `Atom` model. Adding facts only ever *adds* conclusions. Larger-RIF surface (RIF-BLD function symbols, the SPARQL-RIF Core Entailment Regime) is documented out-of-scope in `rif::UNIMPLEMENTED` — tracked, never faked. The expressivity ratchet is `sparq-conformance`'s `rif_core_suite` (opt-in `rif-core` feature; `RIF_CORE_FLOOR`, a sparq-EXTENSION row in the central scoreboard).

- **RIF/XML importer** (`rif-xml` feature, `rif_xml::import()` / `rif_xml::import_with_closure()`): parses the W3C RIF-Core XML

presentation syntax into a `rif::Document`. Applies three sound desugarings at import: body

`Or` → rule-splitting (Lloyd-Topor, one rule per disjunct); body `Exists` → existential

vars become ordinary body vars (range-restriction validated by `Document::validate`);

multi-slot `Frame` → per-slot conjunction (see below, sq-jsgyn). Fail-closed:

`Import` directives, non-Core elements, unknown `External` IRIs, named-argument uniterms,

and malformed XML each produce a named `ImportError` variant; any element whose resolved

namespace is not RIF (#3360; checked per element, so a descendant `xmlns="…"` or a rebound

prefix cannot leave RIF, and prefixed attributes are ignored) and element nesting deeper than 256 levels (#3359, stack-overflow guard) are

refused as `MalformedXml`. Parsing only — no new inference

beyond the existing `rif-core` forward chainer. Unblocks sq-pbz04.5.5 (W3C RIF WG test-suite arm).

**Positional predicate atoms** (`<Atom><op>P</op><args>…</args></Atom>`, sq-n7y15): the dominant

form in real W3C RIF Core test files. Arity-1 maps to `Atom::Member` (membership `a # C`),

arity-2 maps to `Atom::Frame` (frame atom `a[P → b]`). Arity-0 and arity-3+ are rejected

fail-closed (`ImportError::UnrecognizedElement`) — no sound mapping exists in the Core model.

**Multi-slot Frame desugaring** (`obj[p1->v1 p2->v2 …]`, sq-jsgyn): a `<Frame>` with N `<slot>`

children desugars into N `Atom::Frame` atoms — one per `(pi, vi)` pair, sharing the same `obj`.

Under RIF-Core §2.3 a multi-slot frame is the conjunction of per-slot frames; in body position

this becomes a body `And`, in head position N head atoms are added, and as a bare fact N

`Rule::fact` entries are produced. Fail-closed: zero slots → `MalformedXml`; named-arg slot →

`NamedArgUniterm`; duplicate `<object>` → `MalformedXml`. `<slot>` is multi-cardinality;

`<object>` remains single-cardinality.

**Imports-closure consistency check** (`import_with_closure(xml_bytes, resolver)`, sq-wbql1):

unlike `import()` which blanket-refuses any `<Import>` directive, `import_with_closure` accepts

a caller-supplied `resolver: impl Fn(&str) -> Option<Vec<u8>>` and performs a GENUINE consistency

check: (1) profile-checks the `<Import>` `profile` attribute — a non-Core profile IRI (BLD, PRD,

OWL-Direct, …) → `ImportError::InconsistentImport` (a NON-VACUOUS detection, distinct from a

blanket refusal); (2) if the resolver returns bytes for the import location, the imported document

is parsed as RIF-Core and its rules are merged; the combined rule set is then validated — a

validation failure → `ImportError::InconsistentImport`; (3) if the resolver returns `None`, the

import is still rejected fail-closed with `ImportError::ImportDirective`. The fail-closed

invariant: an inconsistent/unresolvable/incompatible import is ALWAYS rejected; a consistent

import (resolvable, Core-compatible profile, combined rules pass `validate()`) is accepted and

the merged `Document` returned. The W3C RIF ImportRejectionTests target profile-mismatch

invalidity; with a file-system resolver wired to the fetched `Core_v1.22` archive, tests using

non-Core `profile` attributes graduate from `skip:imports` to `Outcome::Pass`.

## Stratified Datalog rules (opt-in `datalog` feature, `sparq_reason::datalog`)

RDFox-parity track (`research/stratified-datalog-rules.md`): a small native

rule dialect with single/grouped `NOT` (negation as failure),

`AGGREGATE COUNT`/`SUM`/`MIN`/`MAX`/`AVG` atoms (including

`COUNT(DISTINCT ?v)`), variable predicates, and numeric `FILTER` over exact,

float, and double values. Its **stratification checker** rejects programs with a

recursion cycle through NOT/AGGREGATE; dependencies are class-granular for

`rdf:type`, while variable predicates conservatively couple to every relation. It has a

semi-naive per-stratum evaluator on the shared substrate join kernels, and

**incrementally maintained materialization** (`MaterializedProgram`: DRed for positive

strata, stratum-boundary rederivation for `NOT`/`AGGREGATE` strata).

```rust

use sparq_reason::datalog::{eval, parse_program, stratify, MaterializedProgram};

pub fn parse_program(dict: &mut Dict, src: &str) -> Result<Program, String>;

pub fn stratify(dict: &Dict, p: &Program) -> Result<Stratification, String>; // checker alone

pub fn eval(dict: &mut Dict, facts: &[[Id;3]], p: &Program) -> Result<Vec<[Id;3]>, String>;

impl Program { pub fn n_rules(&self) -> usize; }

impl Stratification { pub fn n_strata(&self) -> usize; }

// Incrementally maintained materialization (sq-4foq0). insert/delete return the

// exact closure delta; delete of a still-derivable fact keeps it (owner changes);

// update() is one batch: new base = (base \ deletes) ∪ inserts.

impl MaterializedProgram {

pub fn new(dict: &mut Dict, facts: &[[Id;3]], p: Program) -> Result<Self, String>;

pub fn insert(&mut self, dict: &mut Dict, facts: &[[Id;3]]) -> usize;

pub fn delete(&mut self, dict: &mut Dict, facts: &[[Id;3]]) -> usize;

pub fn update(&mut self, dict: &mut Dict, ins: &[[Id;3]], del: &[[Id;3]]) -> (usize, usize);

pub fn contains(&self, f: &[Id;3]) -> bool;

pub fn closure(&self) -> Vec<[Id;3]>; // a SET; also len() / is_empty()

}

```

```rust

let mut dict = Dict::new();

let rules = parse_program(&mut dict, r#"@prefix ex: <http://ex/> .

[?x, ex:deg, ?c] :- AGGREGATE([?x, ex:edge, ?y], [?y, ex:tag, ?t]

ON ?x BIND COUNT(DISTINCT ?y) AS ?c) .

[?x, a, ex:Hub] :- [?x, ex:deg, ?c], FILTER(?c >= 3) .

[?x, a, ex:Leaf] :- [?x, a, ex:Node],

NOT { [?x, a, ex:Hub], [?x, ex:disabled, "yes"] } ."#)?;

let closure = eval(&mut dict, &facts, &rules)?; // inputs + derivations, a SET

```

Grouped absence accepts `NOT { atom, atom }` or `NOT EXISTS { atom, atom }`; atoms

may be comma- or period-separated. The whole conjunction is tested jointly, with

free variables existential and group-local. Legacy `NOT atom` is unchanged. Variable

predicate atoms scan all relations; a variable head predicate emits only when its

binding is an IRI. Aggregate numeric inputs use the shared XSD numeric tower and

non-numeric rows fail closed; `FILTER` uses relational numeric comparison, so NaN

also fails the row (including `!=`). Head/FILTER vars must be bound positively;

non-`ON` aggregate-body vars are aggregate-local (name collisions rejected). `COUNT(?v)`

counts distinct full-body matches per group; `COUNT(DISTINCT ?v)` de-duplicates the

projected value within each group. Counts mint `xsd:integer` literals. `SUM`

and `AVG` follow SPARQL numeric promotion (`AVG` of integers is `xsd:decimal`), while

`MIN`/`MAX` preserve the original extremal term id. `xsd:float`/`xsd:double` operands

are accepted (not rejected) on all four, so `SUM`/`AVG` can emit float/double; because

float addition is not associative the fold order is PINNED to ascending value, ties

broken by RDF-term CONTENT (datatype, then lexical form — not by dictionary id, which

follows interning order), and `MIN`/`MAX` order `NaN` below `-INF` (`NaN` is not a row

failure here, unlike `FILTER`) with `+0.0`/`-0.0` a content-broken tie — so the closure

is a function of the completed lower strata, not of derivation order. Semi-naive rounds run per stratum.

Incremental maintenance is differential-pinned (closure == from-scratch `eval` after

every randomized insert/delete step) and skips strata whose input predicates did not

change; its per-update set/index bookkeeping is O(affected visible input) — the

incrementality win is delta-driven RULE-FIRING work (deterministic counters), not set

ops.

**CLI surface** (`sparq-cli --features datalog`; sq-p4zci). The rules live in a file,

because unlike `rdfs`/`owl` a Datalog program is user-supplied, so the reasoning profile carries an

argument — `datalog:<rules.dlog>`, split on the first `:`:

```bash

# Materialize the closure to N-Triples...

sparq-cli reason graph.nt ntriples datalog:rules.dlog closure.nt

# ...or reason-then-query in one shot; derived facts are ordinary triples, so this is plain BGP

sparq-cli query graph.nt ntriples 'SELECT ?x WHERE { ?x a <http://ex/Leaf> }' \

--reason datalog:rules.dlog

```

Reasoning runs at the parse → index-build seam (as `--reason rdfs` does), and stderr reports the

program shape and the expansion: `reasoned [datalog rules.dlog]: <n> rule(s) in <k> stratum/strata;

<base> -> <total> distinct triples (+<derived> derived) in <elapsed>s`. A rule document outside the

documented fragment — or with a plain syntax error — (exit 1, the parser names the construct) and a

program whose recursion cycles through `NOT`/`AGGREGATE` (exit 1, the checker names a predicate on

the cycle) both fail LOUDLY, each message carrying the rules-file path.

Without the feature, `--reason datalog:…` is exit 2 naming it, with **no** fall-back profile —

RDFS/OWL-RL are monotone, so silently substituting one would drop `NOT`/`AGGREGATE` and change the

answer set. The one-shot CLI path uses `eval`; for a long-lived closure under mutation, use

`MaterializedProgram` from the library API above.

## D-entailment datatype typing (opt-in `d-entail` feature, `sparq_reason::dtype`)

The RDF 1.1 Semantics D-entailment regime materializes the **rdfD1 datatype-typing rule**: a well-formed literal of a recognized datatype `d` entails a typing triple. `materialize(Profile::D, …)` adds the recognized 30-XSD-datatype map via `Recognized::standard()` — the `DTYPE_TABLE` single source of truth in `dtype.rs` — plus the always-recognized `rdf:langString` (or bring a custom map via `materialize_d(d, …, …)`):

**Supported datatypes** (complete signed/unsigned integer family, exact decimals/temporal):

- String family: `xsd:string`, `xsd:normalizedString`, `xsd:token`; pattern-restricted derived types `xsd:language`, `xsd:Name`, `xsd:NCName`, `xsd:NMTOKEN`.

- Boolean: `xsd:boolean`.

- Integer family (13 XSD types — `xsd:integer` + 12 derived): `xsd:long`/`xsd:int`/`xsd:short`/`xsd:byte` (signed); `xsd:unsignedLong`/`xsd:unsignedInt`/`xsd:unsignedShort`/`xsd:unsignedByte` (unsigned); `xsd:nonNegativeInteger`/`xsd:positiveInteger`/`xsd:nonPositiveInteger`/`xsd:negativeInteger` (restricted).

- Numeric: `xsd:decimal` (exact, unbounded magnitude via canonical-decimal STRING comparison, never f64), `xsd:double`, `xsd:float` (IEEE 754, distinct value spaces).

- Temporal: `xsd:dateTime`, `xsd:dateTimeStamp`, `xsd:date`.

- URI: `xsd:anyURI`.

- Binary: `xsd:hexBinary`, `xsd:base64Binary` (shared octet-sequence value space).

**Value-space equality (the load-bearing invariant):** `"1"^^xsd:integer` and `"1.0"^^xsd:decimal` denote THE SAME value and must compare equal in D-entailment. Integer/decimal are compared as a canonical-decimal STRING (sign + minimal integer/fraction digits), NEVER via f64 (which aliases integers past 2^53 and loses decimal precision — silent bugs in semantic equality). `xsd:float`/`xsd:double` are IEEE value spaces; `xsd:date` and `xsd:dateTime` are disjoint temporal families (even at the same instant).

**Fail-closed posture:** unmapped datatypes are not typed; facet-invalid literals (`"200"^^xsd:byte`, `" a"^^xsd:token`) are rejected before value mapping; `xsd:time`, duration types, and XML datatypes (`rdf:XMLLiteral`) are deferred — tracked in the design record (`research/d-entailment-datatype-map.md` §3.2), never silently mapped. The `Recognized::default()` set carries ONLY the always-recognized `xsd:string` / `rdf:langString` pair — safe to materialize over arbitrary data.

## Quoted-triple (RDF 1.2 reifier) inference (opt-in `quoted-triples` feature)

The loaders desugar every RDF 1.2 quotation form (`<< :s :p :o >>`, `:s :p :o ~ :r`, `{| … |}` annotation blocks) to a reifier node `R` with `R rdf:reifies <<( s p o )>>`, the triple term being ONE opaque structural dictionary id. With `features = ["quoted-triples"]`, `materialize(Profile::OwlRl, …)` additionally runs the two **bridge rules** between that shape and the classic reification vocabulary, alternated with the RL closure to their joint fixpoint:

- **reif-dtr (destructure):** `(r rdf:reifies <<( s p o )>>)` ⊢ `(r rdf:type rdf:Statement)`, `(r rdf:subject s)`, `(r rdf:predicate p)`, `(r rdf:object o)` — so domain/range/subPropertyOf/sameAs reasoning reaches the recovered components.

- **reif-ctr (construct):** `(r rdf:subject s)`, `(r rdf:predicate p)`, `(r rdf:object o)` **and `(s p o)` present in the closure** ⊢ `(r rdf:reifies <<( s p o )>>)`, minting the triple term. Two finiteness guards: only EXISTING triples are ever reified (asserted or derived — never invented), and no component of a constructed triple term may itself be a triple term (quotation-of-a-quotation is never constructed), which keeps the Herbrand base FINITE, materialization terminating AND idempotent (termination argument in `sparq-reason/src/reify.rs`).

**Opacity:** quotation never asserts — `:r rdf:reifies <<( :s :p :o )>>` does NOT entail `:s :p :o` — and no rule rewrites inside a triple term (`owl:sameAs` substitutes whole ids only). Reifier ANNOTATIONS are ordinary triples and get full RL reasoning without touching the quoted content.

**Strict opacity (`ReifyMode`, second increment):**  the bridge COMPOSITION (destructure → eq-rep on the classic vocabulary → construct) can still quote an `owl:sameAs`-VARIANT spelling of an existing triple. `materialize_owl_rl_reify(&mut dict, &mut triples, ReifyMode::DestructureOnly)` suppresses that: reif-ctr never runs, so inference never mints a triple term at all — destructure, annotation reasoning, and the RL core are unchanged. `materialize_owl_rl` ≡ `ReifyMode::Bridge` (the full bridge).

**Strict opacity incrementally (third increment):**  `MaterializedOwlGraph::with_reify_mode(&mut dict, &base, ReifyMode::DestructureOnly)` fixes the mode at construction; every Fallback re-materialization (the initial one and every mutation's) runs it, so the handle's closure always equals the MATCHING batch oracle — `materialize_owl_rl_reify(dict, base, mode)` from scratch — and inference never mints a triple term under an edit sequence either. `MaterializedOwlGraph::new` ≡ `ReifyMode::Bridge`; `reify_mode()` reports the mode. Mode DETECTION is unchanged (reify vocabulary → Fallback in both reify modes: the counting modes model neither bridge rule).

**OFF by default** (the bridge is a deliberate, non-normative entailment extension): plain `Profile::OwlRl` closures are byte-identical without the feature, and occurrence-guarded even with it (reify-free data pays nothing). `MaterializedOwlGraph` routes reify-vocabulary bases to its documented Fallback mode (incremental == from-scratch parity preserved). No new `Profile` variant, no new deps.

## OWL 2 EL classification (`sparq-reason-el`, separate opt-in crate)

OWL 2 RL is **sound but silently incomplete for class classification**: it has no rule that reasons *through* an existential successor, so `--reason owl` over an EL ontology (GO/ChEBI/SNOMED-style) returns a `rdfs:subClassOf` hierarchy that **silently omits** subsumptions like `A ⊑ D` from `A ⊑ ∃r.B`, `B ⊑ C`, `∃r.C ⊑ D` (Krötzsch, ISWC 2012). **`sparq-reason-el`** closes that gap — a consequence-based classifier that normalizes the TBox (Baader–Brandt–Lutz forms) and saturates `S(C)`/`R(r)` under completion rules **CR1–CR5** to compute the **complete** subsumption lattice, then emits it into the **same** `(Dict, Vec<[Id;3]>)` seam as the RL `scm-*` rules (queryable by plain BGP eval).

```rust,ignore

// Cargo.toml (publish = false: take sparq-core from the SAME git source, or Dict types differ):

// sparq-core = { git = "https://github.com/sparq-org/sparq" }

// sparq-reason-el = { git = "https://github.com/sparq-org/sparq" } // SEPARATE; depending on it is the opt-in

use sparq_core::Graph;

use sparq_reason_el::{classify_graph, Classifier};

// Materialize the complete subsumption lattice in place, then query as usual.

let (mut dict, mut triples) = Graph::parse_to_triples(ttl, "turtle")?;

let report = classify_graph(&mut dict, &mut triples); // adds derived rdfs:subClassOf edges

let g = Graph::from_parts(dict, triples);

// Or a typed, non-mutating view (super-classes / subsumption test / unsatisfiable classes):

let (dict, triples) = Graph::parse_to_triples(ttl, "turtle")?;

let h = Classifier::classify(&dict, &triples);

let _ = h.super_classes(some_class_id);

let _ = h.unsatisfiable_classes(); // classes forced ⊑ owl:Nothing (e.g. via disjointWith)

let _ = h.report().thing_unsatisfiable; // global owl:Thing ⊑ owl:Nothing clash

```

- **Scope (default, Phase E1):** `EL+⊥` minus RBox — `rdfs:subClassOf`/`owl:equivalentClass`, `owl:intersectionOf`, `owl:someValuesFrom` restrictions, `owl:disjointWith`, `owl:Thing`/`owl:Nothing` — **plus safe nominals** (bead `sq-pbz04.2.1`): a singleton `owl:oneOf` (`{a}`) and an object-valued `owl:hasValue` (`∃r.{a}`) are basic concepts reasoned over by completion rule **CR6** (the reachability-guarded nominal merge, "Pushing the EL Envelope" IJCAI-05 — the guard is what keeps `C ⊑ {a}, D ⊑ {a} ⊬ C ⊑ D` when `D` may be empty; negative tests in `tests/nominals.rs` pin it). Every CR6 derivation is sound; completeness is claimed for the typical safe usage, NOT for every EL++ nominal interplay (unrestricted nominal interaction needs a stronger calculus — ELK line of work, KR 2012). **Global bottom:** `Report::thing_unsatisfiable` is `true` when saturation derives `owl:Thing rdfs:subClassOf owl:Nothing`; `unsatisfiable_classes()` remains a named-class-only list and deliberately excludes `owl:Thing`. **Self-restrictions** (bead `sq-pbz04.2.6`): `owl:hasSelf "true"^^xsd:boolean` + `owl:onProperty r` is the profile's `ObjectHasSelf` (`∃r.Self`, local reflexivity) — decoded as a self-concept atom and reasoned over by **CR-Self-1** (`X ⊑ ∃r.Self ⇒ (X,X) ∈ R(r)`), **CR-Self-2** (`∃r.Self ⊑ D ⇒ X ⊑ D`, realised via the self-concept atom + CR1), and — bead `sq-8zqwb`, EL wave 2 — **CRs3, nominal reflexivity** (a SAME-NOMINAL self-link `({a},{a}) ∈ R(r)`, e.g. an asserted or derived `a r a`, reads off as `∃r.Self ∈ S({a})` — sound because a nominal denotes a singleton, so its r-successor inside itself IS itself). Load-bearing side-condition: a GENERAL `(X,X)` link from `X ⊑ ∃r.X` (CR3) — whose invariant is only `X ⊑ ∃r.X`, NOT `X ⊑ ∃r.Self` — must NEVER trigger CR-Self-2 or CRs3 (only a NOMINAL's self-link is local reflexivity); a malformed `owl:hasSelf` (non-`true`/non-boolean object, missing `owl:onProperty`) stays a counted skip (fail-closed). The default TBox classifier does NOT internalize ABox `rdf:type`/property assertions (that stays its contract in every feature state — see the opt-in `abox` feature below for assertion realisation + whole-ontology consistency). Class axioms outside the recognised fragment are **not applied** and counted in `Report::skipped_axioms` (honest, never silently misapplied). Single-threaded by default (see the opt-in `par` feature below).

- **RBox role reasoning + lattice readoff (opt-in `rbox` feature, Phases E2/E3, beads `sq-xetf7`/`sq-pbz04.2.7`):** add `features = ["rbox"]`. Applies `rdfs:subPropertyOf` role inclusions (**CR10**) and `owl:propertyChainAxiom` + `owl:TransitiveProperty` compositions (**CR11**, incl. the SNOMED-critical right-identity `r ∘ s ⊑ s`) via a saturated role automaton, so links propagate up the role hierarchy and along chains before CR4/CR5 fire. `classify_graph` ALSO emits the **NON-REFLEXIVE told-inclusion closure** as `rdfs:subPropertyOf` triples (readoff of the already-computed `RoleBox::super_of` table — no new saturation; self-pairs excluded). `Report::emitted_role_subsumptions` counts the new triples added (told pairs already in the graph are not re-emitted; second call idempotent). **Regularity honesty (bead `sq-oj06v`):** the OWL 2 global restrictions require the RBox to be REGULAR (a strict order on roles must admit every chain axiom); a TOLD RBox that is not — its role-inclusion/chain dependency graph has a cycle through a property-chain constraint (checked on the told n-ary chains, NOT the binarized forms, so a told left identity `s ∘ p ∘ q ⊑ s` is correctly regular) — sets **`Report::rbox_non_regular`**: CR10/CR11 saturation still terminates and every derived subsumption stays sound, but the EL+ completeness argument assumes regularity, so classification **may be incomplete** (the `skipped_axioms` honesty posture — flagged, never silently wrong; pure inclusion cycles i.e. equivalent roles and binary transitivity `r ∘ r ⊑ r` are NOT flagged). **OFF by default** — zero role-automaton code in the default/wasm build; without it RBox axioms are left unapplied (roles compared for equality only). `Classifier::classify` (typed API) is unchanged.

- **Transitive reduction → Hasse diagram (opt-in `hasse` feature, Phase E3, bead `sq-s2nob`):** add `features = ["hasse"]`. `DirectHierarchy::from_closure(&h)` reduces the *full* closure to **direct (immediate) subsumers** and collapses **equivalence cliques** (`direct_super_classes` / `representative` / `equivalent_classes`); `classify_hasse_graph(&mut dict, &mut triples)` materializes the COMPACT taxonomy — direct `rdfs:subClassOf` + `owl:equivalentClass` edges, **O(N)** on a deep chain instead of the O(N²) full closure `classify_graph` emits. The closure of the direct edges (chased through cliques) re-derives the complete relation, so it loses nothing. **OFF by default** — zero reduction code without it; the full-closure `Classifier`/`classify_graph` API is unchanged. Deterministic (rep = min dict id, sorted output) so the Hasse **edge count** is a hard assertion target; timings advisory.

- **Concrete domains — CR7–CR9 (opt-in `cdomain` feature, bead `sq-pbz04.2.2`):** add `features = ["cdomain"]`. Faceted datatype restrictions — `owl:onDatatype` + `owl:withRestrictions` with `xsd:min/maxInclusive`/`xsd:min/maxExclusive` facets — are decided EXACTLY on the shared `sparq_substrate::numeric` value tower (`Dec` i128 fixed-point, never lossy f64) for `xsd:decimal`, `xsd:integer` and the 12 derived integer types (implicit bounds folded in, so `xsd:byte` + `minInclusive 1000` is genuinely empty; exclusive integer bounds TIGHTEN, so integer `(5, 6)` is empty while decimal `(5, 6)` is not). An **EMPTY** range is `⊑ owl:Nothing` (the clash reaches classes with an `∃p.range` obligation via CR5 → `unsatisfiable_classes()`); a **proven value-space containment** (`[5,10] ⊆ [0,20]`, integer-inside-decimal, point-in-range) threads subsumptions through data-property existentials via the ordinary CR1/CR3/CR4. Exact-numeric `DataHasValue` (`owl:hasValue 5`) and singleton `DataOneOf` (`owl:oneOf (5)`) are point ranges (`{5}`, `{5.0}` and faceted `[5,5]` unify on ONE concept). **Deferred — no verdict is EVER guessed** (stays in `skipped_axioms`): pattern/length/digit facets (an unknown facet defers the WHOLE range — ignoring it could fabricate a containment), float/double or non-numeric bases and bound values, `owl:onDataRange` (cardinality vocabulary, outside EL), `owl:datatypeComplementOf`, ill-formed bounds (`"300"^^xsd:byte`), and mixed range/class-expression nodes. Known sound incompleteness: a decimal-sorted range is not derived ⊆ an integer-sorted one (non-point cases), and a plain facet-free datatype IRI filler keeps its opaque-class treatment. **OFF by default** — zero concrete-domain code and no `sparq-substrate` dep without it; every concrete-domain occurrence is then skipped as before. `tests/cdomain.rs` pins the sat/unsat/deferral matrix with exact-closure oracles. Composed with `abox` (bead `sq-vkq9u`) the same point machinery rescues `DataPropertyAssertion`s — see the ABox bullet below.

- **ABox realisation + whole-ontology consistency (opt-in `abox` feature, bead `sq-pbz04.2.5`):** add `features = ["abox"]`. The additive `realize(&dict, &triples) -> Realization` / `realize_graph(&mut dict, &mut triples) -> AboxReport` entry internalizes `ClassAssertion` (`a rdf:type C` ⇒ `{a} ⊑ C`) and `ObjectPropertyAssertion` (`a p b` ⇒ `{a} ⊑ ∃p.{b}`) as SAFE-NOMINAL axioms over the CR6 machinery, then reads the saturation off: `{a} ⊑ C` (C a NAMED class, incl. `owl:Thing`) ⇒ **`a rdf:type C`**; a derived `{a} ⊑ {b}` ⇒ **`a owl:sameAs b`**; a derived `∃r.Self ∈ S({a})` (bead `sq-pbz04.2.6`, `owl:hasSelf`) ⇒ the property assertion **`a r a`** via `Realization::self_assertions()` (the WG `New-Feature-SelfRestriction-001` "Peter likes Peter"; the CONVERSE — an asserted `a r a` ⇒ `Peter ∈ ∃likes.Self` typings via CRs3, the `New-Feature-SelfRestriction-002` converse shape — graduated in bead `sq-8zqwb`); `{a} ⊑ ⊥` (two disjoint `ClassAssertion`s, an instance of `∃owl:bottomObjectProperty.⊤` or `∃op.owl:Nothing`) or a global `⊤ ⊑ ⊥` ⇒ a whole-ontology **`is_inconsistent()`** verdict (on `Realization` and the returned `ClassHierarchy`). **Every emitted typing/sameAs/inconsistency holds in EVERY model** (soundness over completeness; the CR6 reachability side-condition is untouched — this path only READS the saturation `classify::saturate` produced). The TBox `Classifier::classify`/`classify_graph` are **byte-identical in every feature state** (they NEVER internalize assertions — so the `el-suite` conformance floor is unaffected even under `--all-features`). **Composed with `cdomain` (bead `sq-vkq9u`)** a `DataPropertyAssertion` whose literal lies in the exact numeric tier is ALSO internalized — `a q 5` ⇒ `{a} ⊑ ∃q.{5}`, over the very point range CR9 mints for `DataHasValue 5` — so CR8 containment threads an **asserted VALUE** into the TBox's data-range obligations (`:alice :age 42` with `∃age.[18,∞) ⊑ :Adult` ⊨ `:alice a :Adult`; two asserted values in provably-disjoint ranges ⇒ `is_inconsistent()`). Sound because `a q v` asserts `(a^I, v) ∈ q^I` and `v ∈ {v}^D`; `tests/abox_cdomain.rs` pins it (that feature CONJUNCTION is its own feature-matrix leg). **Fail-closed:** a data-property literal with no minted point range — EVERY literal without `cdomain`, and with it the string / lang-tagged / float-tier / ill-formed-for-its-own-datatype cases — and a non-EL class expression in a `ClassAssertion` stay counted in `Report::skipped_assertions`, never guessed; an INCONSISTENT ontology realises to NOTHING (the verdict is the surface, not an everything-entailed flood). **OFF by default** — zero assertion-reasoning code without it. `src/abox.rs` pins the readoff over the WG `WebOnt-Ontology-001` / `DisjointClasses-002` / `New-Feature-BottomObjectProperty-001` / `WebOnt-Restriction-001` / `WebOnt-Thing-003` shapes.

- **Parallel saturation (opt-in `par` feature, Phase E4, bead `sq-wy3i6`):** add `features = ["par"]`. `Classifier::classify_par(&dict, &triples, threads)` / `classify_graph_par(&mut dict, &mut triples, threads)` (`threads: NonZeroUsize`) run the SAME CR1–CR6 (+`rbox` CR10/CR11) rules as **deterministic bulk-synchronous rounds**: the membership frontier is partitioned across a bounded `std::thread::scope` worker pool that derives rule firings read-only against the round-start snapshot, then a sequential apply phase reuses the single-threaded `add`/`add_link` machinery. **The derived closure is IDENTICAL to the single-threaded engine at every thread count** (soundness + completeness + determinism — pinned by `tests/par_differential.rs` differentials incl. delayed-filler CR4 / CRs1-link mutation witnesses and a repeated-run determinism stress, plus the `sparq-conformance/el-suite-par` differential over the W3C EL corpus in the CI el-suite lane); emitted triples match content AND order. **OFF by default** — zero threading code without it; native targets only (do NOT enable for wasm, where `std::thread` cannot spawn — the default single-threaded path is the wasm story). No wall-clock/speedup claim is made or pinned (work-box timings are non-canonical).

- **Phase attribution (`par`, bead `sq-q0o82`):** only the **compute** phase is parallel; **apply** (`add`/`add_link`, and the `rbox` CR10/CR11 closure) is still sequential, so the E4 speedup is Amdahl-bounded by it. `classify_graph_par_stats(&mut dict, &mut triples, threads) -> (Report, ParPhaseStats)` is `classify_graph_par` plus that split — the graph mutation, emitted triples and `Report` are byte-identical (it only reads two clocks per round). `ParPhaseStats::{rounds, frontier_items, derived_members, derived_links}` are a function of the input ALONE and are **invariant across thread counts** (chunking decides *which worker* derives a conclusion, never *which* conclusions — pinned in `tests/par_differential.rs`), so they are safe to assert on; `compute_nanos`/`apply_nanos` are wall-clock, non-deterministic and **non-canonical** — use `ParPhaseStats::apply_fraction()` (the sequential share, `0.0..=1.0`) as a ratio and never quote an absolute figure. The `par_phase_bench` example (`--features par`) prints the split: with no args it runs a synthetic wide-taxonomy workload and *asserts* the closure matches sequential and the work counts are thread-invariant; with `<path> [format]` it gathers the same row for a real ontology — the input the still-OPEN **parallel-apply refinement** decision needs (a GO/SNOMED-scale dump this repo does not vendor), since a sharded apply would put the identical-closure invariant at risk and is not worth it on synthetic evidence alone.

- **Keys + negative property assertions + differentFrom (also `abox`, bead `sq-pbz04.2.8`):** the `realize` / `realize_graph` readoff ALSO reasons over three more ABox mechanisms, all sound-over-complete. **`owl:hasKey(C, keys)`** merges two DISTINCT **named (IRI)** individuals BOTH derivably in `C` that share a value on **EVERY** key property (⇒ **`a owl:sameAs b`**, in `Realization::same_as()`). Object keys match a shared **nominal successor** (`{b} ∈ R(p)[{a}]`, asserted or derived); data keys a shared **literal TERM** (identical terms ⇒ identical values — sound; value-equal-but-lexically-distinct literals are an honest incompleteness pending the `cdomain` numeric tower). Firing on a **PARTIAL** match is impossible **by construction** (each key property's shared-value set must be non-empty AND intersect — the classic HasKey over-derivation trap, pinned by a negative test; e.g. `New-Feature-Keys-006`'s single-member key never fires, and the functional-property clash it needs is honestly out of fragment). **`owl:NegativePropertyAssertion`** is a whole-ontology clash (**`is_inconsistent()`**) iff the corresponding POSITIVE is asserted or DERIVED — object NPA against a nominal successor (asserted *or* derived), data NPA against an asserted `a p "v"` triple or, with `cdomain`, an entailed point-range successor of `{a}` via `p` that matches the exact numeric VALUE of `v` (so `"5"^^xsd:integer` meets `"5.0"^^xsd:decimal`, and a positive derived through a TBox axiom counts; a wider range does not). Other literals keep term-identity matching against asserted triples. **`owl:differentFrom`** (in `Realization::different_from()`, `realize_graph` materializes `owl:differentFrom` triples) is read off **ONLY** from a derived nominal clash (`{a} ⊓ {b} ⊑ ⊥` via a disjointness — `WebOnt-disjointWith-001`) or the SYMMETRIC closure of an asserted inequality (`WebOnt-differentFrom-001`) — never fabricated; a `sameAs`/`differentFrom` coincidence (`New-Feature-Keys-002`) is **inconsistent**. **Fail-closed:** a malformed key (non-atomic class, empty/non-IRI list) or NPA stays counted in `Report::skipped_assertions`. `src/abox.rs` pins the `Keys-001/-002/-003/-006`, both NPA-001, `differentFrom-001`, `disjointWith-001` shapes plus the partial-key negative test.

- **Incremental classification under TBox edits (opt-in `incremental` feature, Phase E5, bead `sq-clsv6`):** add `features = ["incremental"]`. `IncrementalClassifier::new(&dict, &triples)` classifies once and KEEPS the CR1–CR6 saturation; `apply_edits(&dict, added, removed) -> IncrementalReport` then re-classifies the edited TBox and `hierarchy() -> ClassHierarchy` / `triples()` read the post-edit state. **READ THE SCOPE BEFORE RELYING ON THE NAME.** EL saturation is a monotone least fixpoint, so only ADDITION is incremental: a **monotone extension** (new class axioms + brand-new class-expression nodes) is folded into the live fixpoint by a delta-seeded resume (`classify::resaturate` re-queues just the retained memberships a new axiom's trigger keys occur in — the least-fixpoint argument for why that equals a from-scratch closure is in its doc comment). **Any RETRACTION takes a full re-classification**, as does any RBox / concrete-domain change and any edit that attaches structure to a node the graph already MENTIONS (that can CHANGE an existing axiom rather than add one — including the first structure on a node an axiom currently reads as an opaque class atom). The saturation keeps **no derivation provenance**, so DRed / ELK affected-context deletion repair (Kazakov & Klinov, ISWC 2013) is **NOT implemented** — deferred, never faked. Which path ran is always disclosed in `IncrementalReport::disposition` (`NoOp` / `Incremental` / `Full(FullReason::{Retraction, ExistingNode, Vocabulary, ConcreteDomain})`), with `added_axioms` / `reseeded_memberships` as the work measures. **The invariant that holds on BOTH paths:** the post-edit hierarchy equals `Classifier::classify` over the post-edit triple set — pinned edit-by-edit in `tests/incremental.rs` against the hand-derived ELK-calculus closure oracle AND against a from-scratch classification, over hand-built edited-TBox fixtures plus randomized add / add-and-retract / **triple-at-a-time** streams. `Report::skipped_axioms` agrees with a from-scratch extraction too; `Report::named_classes` does NOT (it reports the live concept-index size, which also counts fresh normalization names earlier edits minted). TBox-only in every feature state (never internalizes ABox assertions), single-threaded (independent of `par`), and **OFF by default** — the stateless E1–E4 entries carry zero edit-tracking state or code. No wall-clock/speedup claim: the win is skipping the SATURATION, but every edit still rescans the graph structurally, so on a small graph the fixed costs can dominate (work-box timings are non-canonical).

- **Deferred EL fragment (honest incompleteness, surfaced — NOT silently wrong):** without `cdomain`, ALL concrete-domain shapes (`owl:onDataRange`/`owl:withRestrictions`/`owl:onDatatype`/`owl:datatypeComplementOf` + literal `hasValue`/`oneOf`) land in `Report::skipped_axioms`; with it, the unsupported remainder above still does. Distinct from constructs **outside EL entirely** (unionOf / complementOf / allValuesFrom / cardinality / a **multi-individual** `owl:oneOf` — the profile's `ObjectOneOf` admits exactly one individual, more is a disjunction — all skipped, but those need ALC / Horn-SHIQ, not a deferred EL slice; `owl:hasSelf` is NO LONGER here — it is in-fragment via CR-Self, bead `sq-pbz04.2.6`) and from RBox (a *gated* capability via `rbox`, not permanently deferred). Parallel saturation is the opt-in `par` feature (E4, bead `sq-wy3i6` — identical closure at every thread count); incremental-ADDITION re-classification under TBox edits is the opt-in `incremental` feature (E5, bead `sq-clsv6` — retraction falls back to a full re-classification, reported). `classify_graph` (full closure) and `classify_hasse_graph` (reduced) are both available — pick by whether you want every derived subsumption or just the immediate-parent taxonomy.

- **End-to-end scaling check.** `cargo run -p sparq-reason-el --features rbox,hasse --example snomed_go_scale_bench --release [SCALE]` runs a SNOMED/GO-shaped slice (is-a forest + transitive part-of + SNOMED right-identity role chain + existential restrictions) at 1×/2× and asserts a **relative** (dimensionless) property: closed-form derived counts hold at both scales (conformance) AND the work proxy doubles at most ~2× — confirming normalise + RBox + Hasse compose with **no hidden quadratic**. No hard-coded ms (work-box timings are non-canonical); `tests/snomed_go_scale.rs` is the CI-gated counterpart (runs under the `rbox`/`hasse` legs).

- **W3C OWL 2 EL suite — a pinned EXTENSION ratchet (bead `sq-pbz04.2.4`/`sq-pbz04.2.9`, opt-in `sparq-conformance/el-suite`).** The W3C OWL WG export (`tests/w3c/owl2/all.rdf`), filtered to `test:EL` ∧ `test:RDF-BASED` (Approved, inline RDF/XML premise, no `owl:imports`), is run through the **REAL** classifier: each premise is classified with `classify_graph` (materializing the complete `rdfs:subClassOf` lattice IN PLACE, with **`rbox`** + **`cdomain`** also on — the CI lane exercises the full shipped feature set) and each declared check decided — **consistency** (no unsatisfiable named class), **inconsistency** (some unsatisfiable named class), **positive-entailment** (the lattice ENTAILS the conclusion via the bnode-homomorphism `entail::entails` after output-vocabulary completions: datatype axiomatic-set + mutual-subsumption → `owl:equivalentClass` augmentation — a semantic identity that graduated WebOnt-equivalentClass-003, sq-pbz04.2.9), **negative-entailment** (non-conclusion NOT entailed). `EL_SUITE_FLOOR` is the **MEASURED PASS count** — a **`sparq extension`** row in the central scoreboard (`scoreboard::SUITES`), tallied **separately** and **NOT** a full-OWL-2-EL-conformance claim: tests needing **ABox inconsistency** (individual assertions), or a conclusion in `owl:sameAs`/`rdfs:subPropertyOf`/`owl:equivalentProperty`/`owl:TransitiveProperty`/`owl:unionOf` axiom form (output-vocabulary gaps distinct from inference gaps) are **audited PERMANENT divergences** (reported separately, **never summed into the floor**). `EL_SUITE_FLOOR` is read textually by `tests/scoreboard_floors.rs`, so the mirrored scoreboard value cannot drift; `--nocapture` prints an `OWL 2 EL ratchet pass N of M (floor F)` line the CI job `inference-conformance` re-greps.

- **CLI surface (opt-in `sparq-cli` `el` feature, Phase E6, bead `sq-2ch27`):** `cargo run -p sparq-cli --features el -- classify <data-file> <format> [out.nt]` runs the classifier and prints the report as `name<TAB>value` lines on stdout (`triples`, `named_classes`, `emitted_subclassof`, `emitted_subpropertyof`, `skipped_axioms`, `unsatisfiable_classes`, `thing_unsatisfiable`, `rbox_non_regular`), writing the lattice-augmented graph to `out.nt` when given. The same classifier is also a **reasoning profile**: `query … --reason el` and `reason <f> <fmt> el [out.nt]` classify then hand the augmented triples to the ordinary query/serialisation path. The CLI feature pulls `sparq-reason-el` **with `rbox`** (E1+E2), so role inclusions/chains/transitivity are applied and the role lattice is emitted. Everything the classifier could not reason over is printed as an explanatory NOTE on **stderr** (non-zero `skipped_axioms`, a non-regular RBox, unsatisfiable classes, `owl:Thing ⊑ owl:Nothing`) rather than swallowed. **Without the feature `--reason el` is a hard exit-2 error naming it — never a silent fall-back to `owl`**, which would return a quietly incomplete hierarchy. The other EL features (`hasse`, `cdomain`, `abox`, `par`, `incremental`) have **no CLI surface** — they are library-only today. **That bounds the CLI capability to E1+E2, short of the full OWL 2 EL profile:** with `cdomain` off, every concrete-domain axiom (faceted `owl:onDatatype`/`owl:withRestrictions`, literal `owl:hasValue`/`owl:oneOf`) is deferred into `skipped_axioms` and NOT applied, so a *valid EL* ontology using supported datatype restrictions can classify to an INCOMPLETE hierarchy under `classify` / `--reason el`. The per-run `skipped_axioms` count is honest about a given run; reach for the library API (`sparq-reason-el` with `cdomain`) when the ontology needs CR7–CR9.

- **Use EL, not `--reason owl`, when you need a class hierarchy over an EL ontology** (complete for the fragment the enabled features cover — see the CLI-surface bullet above for the `cdomain` deferral). RL is not an approximation you can tune up with more rules — EL needs a different algorithm. A verified in-repo differential (`crates/sparq-cli/tests/el_cli.rs::el_derives_what_rl_cannot`): given `B ⊑ C`, `B ⊑ E`, `C ⊓ E ⊑ D`, `--reason el` derives `B ⊑ D` (completion rule **CR2**) and `--reason owl` does not — RL's `scm-int` only DECOMPOSES an intersection, and the composition direction exists in the RL/RDF rule set only as the assertional `cls-int1`, over individuals.

## OWL 2 QL query rewriting (`sparq-reason-ql`, EXPERIMENTAL, separate opt-in crate)

OWL 2 QL (DL-Lite_R) is **FO-rewritable**: instead of materializing a closure, you **rewrite the query** into a **union of conjunctive queries** (UCQ) that, evaluated over the **unmodified data**, returns the **certain answers** under the schema (Calvanese et al., *PerfectRef*, JAR 2007). **`sparq-reason-ql`** is a query-rewriter (not a materializer): it reuses the engine's query path — it emits a rewritten `spargebra::Query` (a `Union`-folded UCQ) that the planner/executor run unchanged.

```rust,ignore

// Cargo.toml (publish = false; take spargebra from the SAME git source so `Query` types match):

// sparq-reason-ql = { git = "https://github.com/sparq-org/sparq", features = ["experimental"] }

// spargebra = { git = "https://github.com/sparq-org/sparq", package = "sparq-spargebra" }

use sparq_reason_ql::{rewrite, rewrite_production, as_conjunctive_query, CqError};

use spargebra::SparqlParser;

let q = SparqlParser::new().parse_query("SELECT ?x WHERE { ?x a <http://ex/Employee> }")?;

// `tbox`: &[oxrdf::Triple] carrying rdfs:subClassOf/subPropertyOf/domain/range, owl:inverseOf …

let r = rewrite(&q, &tbox)?; // baseline PerfectRef UCQ; r.report.disjuncts / .skipped_axioms

// Production path: PerfectRef + tree-witness folding + UCQ-containment MINIMISATION (smaller UCQ,

// SAME certain answers). r.report.disjuncts_before_minimisation - r.report.disjuncts = dropped.

let p = rewrite_production(&q, &tbox)?;

// The CQ-shape gate alone (no feature needed) classifies a query without rewriting:

match as_conjunctive_query(&q) { Ok(_cq) => {}, Err(CqError::OutOfScope(why)) => { let _ = why; } }

```

- **FAIL-CLOSED CQ-shape gate (the soundness keystone) with broadened sound fragment.** PerfectRef is sound + complete only for **conjunctive queries**. The gate is **fail-closed** and now accepts a BROADENED sound fragment: **(B1)** top-level UCQ (`UNION` of CQ branches, each rewriting independently; `as_ucq`); **(B2)** RDF literal constants in role-atom object position (rigid, never `_`-eligible — the applicability condition is unchanged); **(B3)** `FILTER` over **distinguished-only** variables (passed through, fail-closed for non-distinguished vars); **(B4)** constant-only `VALUES` over distinguished variables (re-applied as an inner join, fail-closed for UNDEF / non-distinguished); **(B3/B4 per-branch, sq-sg542)** in a MULTI-branch UCQ — a hand-written `{ … FILTER } UNION { … }`, or an alternation path whose `#1671` desugaring distributes a top-level `FILTER` into EACH branch — the emitter is **branch-aware** (`emit::ucq_to_pattern_per_branch`): each branch emits its OWN `FILTER`/`VALUES` over its OWN sub-union, so a branch's modifier constrains only that branch (never hoisted over the whole union, never silently dropped — the leak is differential-tested in BOTH directions in `tests/branch_aware_emit.rs`); this shape was previously rejected fail-closed; **(Bbnode, sq-pbz04.3.6)** body blank nodes in subject/object positions are lifted to fresh existential variables — each distinct blank-node LABEL in a CQ maps to one unique `Unbound` id (shared labels get the same id, so `is_bound_var` correctly treats the shared position as bound and blocks the existential applicability condition on it; distinct labels get distinct ids). The **emitter** completes the round-trip: a repeated `Unbound` id maps to ONE output variable, so a shared body blank node emits as a genuine **JOIN** (not a cartesian product over-approximation) — the load-bearing invariant that lets the shared-existential SELECT cases (`sparqldl-07`/`-08`) graduate rather than fall to `oracle-divergent`. **(B5, sq-pbz04.3.2)** non-recursive property paths — sequence `p1/p2` (fresh non-distinguished intermediate, shared → a JOIN), inverse `^p` (subject/object swap), alternation `p1|p2` (branch multiplication into the B1 UCQ machinery) — are desugared to an equivalent CQ/UCQ BEFORE the entailment rewrite, after which PerfectRef soundness applies (STEP-0-verified: the vendored spargebra parser already lowers a top-level sequence/inverse to a BGP, so only a surviving `Path` alternation is rewritten — no double-translation); `+`/`*`/`?` (recursion / zero-length) and negated property sets stay fail-closed. **(B6)** `rdfs:subClassOf`, `rdfs:subPropertyOf`, `rdfs:domain`, `rdfs:range`, and all `owl:` predicates used as **atom predicates** are **rejected** (intensional-atom guard — fail-closed); annotation predicates (`rdfs:label/comment/seeAlso/isDefinedBy`) are admitted. Everything outside this fragment — `OPTIONAL`/`MINUS`/**recursive-or-negated** property paths (`+`/`*`/`?`/`!p`)/aggregation/variable-predicate/non-distinguished FILTER or VALUES — is **rejected as `CqError::OutOfScope(reason)`**, never silently mis-answered. The applicability condition (an existential generator fires only on an UNBOUND, non-distinguished, non-shared variable) is enforced explicitly. The `reduce` MGU treats **distinguished (answer) variables as rigid** — it never identifies two answer columns.

- **Scope (`experimental`):** the **positive** DL-Lite_R inclusions — `rdfs:subClassOf`/`subPropertyOf`, `rdfs:domain`/`range` (`∃R ⊑ A`, `∃R⁻ ⊑ A`), `owl:inverseOf`, `owl:equivalentClass`/`equivalentProperty` (decomposed to inclusion pairs, named operands only), and **unqualified** `∃R` `owl:someValuesFrom owl:Thing` restrictions. Non-QL axioms are counted in `RewriteReport::skipped_axioms`, never applied.

- **TBox-capture accounting (`TBox` struct, `sq-pbz04.3.3`).** `TBox::extract(triples)` now tallies every `rdfs:`/`owl:` triple it sees: positive inclusions go to `concept_incl`/`exists_super`/`role_incl`; `skipped` counts non-QL constructs (unchanged); **`consistency_relevant`** counts QL-legal negative/disjointness axioms (`owl:disjointWith`/`propertyDisjointWith`/`complementOf`) — present but never applied for REWRITING; `owl:disjointWith`/`propertyDisjointWith` with resolvable operands are additionally captured STRUCTURALLY into **`neg_incl`** (input to the opt-in `ql-consistency` check, sq-p6yb7) with the residue counted in **`consistency_uncaptured`** (invariant: `consistency_relevant == neg_incl.len() + consistency_uncaptured`); so is the **subClassOf-complement** shape `A rdfs:subClassOf [ owl:complementOf B ]` (sq-fj8lj follow-up) — QL's `superClassExpression ::= ObjectComplementOf(subClassExpression)`, i.e. exactly the negative inclusion `A ⊑ ¬B`, so it is counted at the `rdfs:subClassOf` axiom (consistency-relevant, NOT `skipped`; the complement blank node's own `owl:complementOf` triple is then not tallied again) with `∃R` operands resolving on either side, while a **NAMED-subject** `A owl:complementOf B` still asserts the stronger biconditional `A ≡ ¬B` and stays uncaptured; **`unrecognised_schema`** counts OWL/RDFS constructs the extractor does not classify — either an `rdfs:`/`owl:`-predicate triple not handled above, or an `rdf:type` triple whose object is unmodelled schema vocabulary (e.g. `:p rdf:type owl:FunctionalProperty`); `fully_captured()` can therefore be `false` even when all *predicate* IRIs are outside the `rdfs:`/`owl:` namespace. **`TBox::fully_captured()`** returns `true` iff `skipped == 0 && unrecognised_schema == 0` — an accounting/honesty signal that no schema triple was silently dropped, not a DL-Lite_R completeness proof. A `consistency_relevant > 0` count does not block `fully_captured()`.

- **Production path (`rewrite_production`):** baseline PerfectRef **augmented** with bounded **tree-witness** folding (existential witnesses captured with no unbounded chase) then **UCQ-containment minimisation** (drop disjuncts contained in a retained one). Same certain answers as `rewrite`, in a smaller UCQ. **Minimisation is FAIL-CLOSED:** containment is NP-complete, the homomorphism search is bounded, and an **undecided-within-budget** check **KEEPS** the disjunct — minimisation only ever removes a disjunct **proven contained**, so it removes no answers.

- **Oracle-tested; the FORMAL DL-Lite_R suite GRADUATED to a pinned floor (sq-qo1a9).** Validated against a hand-checked DL-Lite_R oracle (`sparq-reason-ql/tests/oracle.rs`, incl. tree-witness + minimisation cases), because no Rust PerfectRef reference exists to diff against. **DL-Lite_R consistency checking is opt-in** (`ql-consistency` feature, sq-p6yb7): `check_consistency`/`check_consistency_with` compose a boolean violation query per captured negative inclusion, rewrite it through the SAME PerfectRef saturation, and evaluate it over the data — **INCONSISTENT** iff some violation query matches (sound at any capture level, by monotonicity); definitive **CONSISTENT** only when the TBox is `fully_captured()` AND `consistency_uncaptured == 0` (the Calvanese-et-al. cln(T) completeness argument, written out in `src/consistency.rs`); fail-closed **Unknown** otherwise — an inconsistent KB certain-answers EVERYTHING, so consumers must treat the verdict, not the positive UCQ answers, as definitive. Oracle-tested in `tests/consistency_oracle.rs` (hand-derived verdicts incl. anonymous-canonical-witness violations). On the **formal DL-Lite_R suite** — the hand-derived certain-answer oracle from `sq-g19x0`, every case a conjunctive query within sound rewriting — the rewrite is **sound AND complete case by case**: `rewrite_production`'s UCQ, evaluated over the **unmodified ABox** through the real engine, returns **exactly** the hand-derived certain answers. That is now a **pinned floor** (`sparq-conformance`'s `tests/ql_dllite_suite.rs`, opt-in `ql-experimental`; `QL_DLLITE_FLOOR = 11` sound-and-complete cases), registered as a **`sparq extension`** row in the central scoreboard (`scoreboard::SUITES`) and tallied **separately** — **NOT folded into the standards-conformance total**, and **NOT a full-OWL-2-QL-conformance claim** (there is no runnable normative W3C QL certain-answer suite; the W3C QL material is structural). Like the RIF-Core / RSP / BM25 extension rows, it pins a faithful sparq-OWN oracle. `QL_DLLITE_FLOOR` is read textually by `tests/scoreboard_floors.rs`, so the mirrored scoreboard value cannot drift.

- **The `pr:QL` `sparql11/entailment` arm: the SOUND subset is GRADUATED to a pinned named-case floor (sq-pbz04.3.4); the rest stays held with an exhaustive reason taxonomy (sq-kuvu3; opt-in `sparq-conformance/ql-experimental`).** Every `sd:EntailmentProfile pr:QL` case runs through a **six-condition graduation predicate** (`inference::sparql_entail::run_ql_graduation`), each condition **checked in code, never assumed**: (1) the fail-closed CQ-shape gate accepts the query AND it carries no intensional schema-vocabulary atom (B6, sq-pbz04.3.1 — now built into the gate); (2) the TBox is **totally captured** (`fully_captured()`, sq-pbz04.3.3); (3) the **consistency condition** — zero consistency-relevant (negative/disjointness) axioms, OR (sq-p6yb7) the DL-Lite_R violation-query consistency check proves the KB **CONSISTENT** (a proven-INCONSISTENT KB holds at `inconsistent-kb` — entailment-regime behaviour on an inconsistent graph is implementation-defined, never a guessed everything-entailed pass — and an UNKNOWN verdict holds at `pending-consistency`); (4) default-graph dataset only; (5) the **regime-coincidence guard** — the crate computes CERTAIN ANSWERS while W3C entailment-regime solution mappings bind every variable to an RDF term; the semantics provably coincide iff all body terms are distinguished (a body blank node counts as a non-distinguished variable) OR the TBox has no existential-generating inclusion (`exists_super` empty) — the fail-closed §4 default, deliberately not widened; (6) the rewritten UCQ evaluated over the **unmodified data** is **result-equivalent to the W3C oracle**. The graduated cases form the **pinned named-case floor** `QL_ENTAILMENT_FLOOR_CASES` in `sparq-conformance`'s `tests/ql_entailment_floor.rs` (exact set equality: a regressing pinned case AND an unpinned newly-eligible case both fail — additions need an evidence-carrying PR; enforced in the `inference-conformance` CI job), mirrored as a **`sparq extension`** scoreboard row (`QL_ENTAILMENT_FLOOR`, read textually by `tests/scoreboard_floors.rs`) — **NEVER summed into the standards-conformance total, NOT a full-regime/full-profile OWL 2 QL conformance claim**. Every non-graduated case carries a specific taxonomy hold: **permanently-outside** (BIND / variable predicates / intensional schema queries / OPTIONAL–MINUS shapes — no sound rewriting in this design), **pending-gate** (B1/B2/B3/B4/B6 landed under sq-pbz04.3.1; **(B5)** non-recursive property-path desugaring — sequence/inverse/alternation — now landed under sq-pbz04.3.2, so a path-shaped CQ is no longer held at the gate; recursive/zero-length/negated paths stay fail-closed; **(Bbnode)** body blank nodes lifted to fresh existential variables so the applicability condition applies correctly — sq-pbz04.3.6), **pending-capture**, **pending-consistency** (now ONLY structurally-uncaptured negative axioms, e.g. a NAMED-subject `owl:complementOf` — the subClassOf-complement spelling `A rdfs:subClassOf [ owl:complementOf B ]` IS captured, sq-fj8lj follow-up; the bucket measured 0 BEFORE the sq-p6yb7 check landed, so the upgrade graduates no case at the current rdf-tests pin), **inconsistent-kb**, **pending-coincidence**, **oracle-divergent**, or **inconclusive** — plus a loud **unclassified-abstain** bucket the floor test asserts EMPTY, so no new abstain class can hide in a catch-all. In the inference BINARY every QL row (graduated or held) remains OutOfScope — no QL row can inflate the binary's conformance ratchet (the D-entailment precedent); `tests/ql_experimental_arm.rs` asserts exactly that plus the taxonomy invariants.

## OWL 2 Direct Semantics (`sparq-reason-dl`, separate opt-in crate — all five layers built: L1 model, L2 profile checker, L3 ALCH tableau, L4 dispatch, L5 conformance arm)

The three profile reasoners above (RL / EL / QL) each cover a *tractable* OWL fragment; **OWL 2 Direct Semantics** (the model-theoretic DL semantics) covers the boolean heart of DL — arbitrary `⊔` / `¬` / `∀` — that none of them can reach. `sparq-reason-dl` is a **separate opt-in crate** building a **layered, fail-closed Direct-Semantics checker**; **all five layers are built: L1 (structural model + extractor), L2 (syntactic EL/QL/RL profile checker), L3 (ALCH tableau — the first layer that does semantic reasoning), L4 (the fragment-dispatch `DirectChecker` + entailment-by-refutation, behind the crate's opt-in `dispatch` feature, bead sq-pbz04.4.4), and L5 (the `sparq-conformance` DIRECT-arm behind that crate's opt-in `dl-direct` feature, bead sq-pbz04.4.5)**. HONEST SCOPE: this is **not** full OWL 2 DL (SROIQ(D) satisfiability is 2NEXPTIME-complete and deliberately out of scope) — it is a scoped **ALCH-fragment** effort, sound/complete only within the argued fragment. L1 delivers:

- **A structural OWL model** (`sparq_reason_dl::model`) — `Axiom` / `ClassExpression` / `ObjectPropertyExpression` typed enums for the ALCH fragment: named classes, `owl:Thing`/`owl:Nothing`, `owl:intersectionOf` (⊓), `owl:unionOf` (⊔), `owl:complementOf` (¬), `owl:someValuesFrom` (∃R.C) and `owl:allValuesFrom` (∀R.C) over **named object properties**; GCIs, `owl:equivalentClass`, `owl:disjointWith`, `rdfs:subPropertyOf`, `rdfs:domain`/`rdfs:range`, and a ground ABox. Purely structural — **no semantics attached at L1**.

- **A FAIL-CLOSED reverse RDF mapping** — `extract(&Dict, &[[Id; 3]]) -> Result<Ontology, ExtractError>` maps the `(Dict, triples)` substrate into the model per the W3C *Mapping to RDF Graphs* tables restricted to ALCH. **A single out-of-fragment or malformed triple aborts the WHOLE extraction** with a typed `ExtractError`, rather than being silently dropped: the (future) checker must never reason over a graph it only *partially* understood — a dropped axiom can flip a consistency verdict. Understood in full, or refused. The rejection taxonomy has five arms — `OutOfFragment` (cardinality / nominals / inverses / `owl:sameAs` / property characteristics / chains / keys), `DataConstruct` (datatypes / data properties — no concrete domain in L1), `MalformedList`, `MalformedClassExpression`, `Unclassifiable` (an undeclared predicate that cannot be mapped soundly) — while annotations, declarations, and ontology headers are recognised and ignored.

- **Forward RDF renderer** (`render`, bead sq-pbz04.4.7) — `render_to_triples(&Ontology, &mut Dict) -> Vec<[Id; 3]>` maps the structural model BACK to OWL RDF triples (the inverse of `extract`), enabling full-fragment round-trip testing (`RDF → extract → render → extract` yields the same structural model; blank-node identity may differ but `Ontology: PartialEq` holds). `render_to_turtle(&Ontology, &mut Dict) -> String` serialises the same output to minimal Turtle for human-readable diagnostics. No extra dependencies; always compiled (not feature-gated). The round-trip invariant is checked at TWO tiers: the hand-written `render::tests` fragments (incl. two regression cases for the sq-pbz04.4.17 fix below), and — belt-and-suspenders — EVERY ontology document of the W3C DIRECT-arm corpus via `inference::dl_suite::run_render_roundtrip_arm` in `sparq-conformance` (opt-in `dl-direct` feature, bead sq-pbz04.4.17; `RenderRoundTripReport` with EXACT-pinned counts — `DL_RENDER_ROUNDTRIP_FLOOR` — and a hard EMPTY-violations assertion: a mis-render is a REAL fidelity bug, never a pinnable divergence). The corpus arm's first run CAUGHT and fixed one: a named-composite `EquivalentClasses(A, expr)` used to render as an INLINE backbone on `A`, which re-extracts differently whenever `A` is referenced elsewhere (14 corpus mismatches) and refuses outright on a self-referential definition (`WebOnt-someValuesFrom-003`); the renderer now always emits the explicit `A owl:equivalentClass _:b` shape, which round-trips both origins. sq-pbz04.4.18 completes the corpus sweep with `run_render_roundtrip_rdf_based_arm`, the same invariant over the DISJOINT **RDF-BASED-only** slice (`test:RDF-BASED` without `test:DIRECT`), pinned separately via `DL_RDF_BASED_ROUNDTRIP_FLOOR`. Admissible because the round trip is purely syntactic — it makes no semantics claim, so no reasoning verdict is ever attributed to an RDF-BASED test. MEASURED, correcting the bead's "several hundred more documents" estimate: **479 of the export's 493 cases are DUAL-tagged** and were already covered, so the slice is just **7 cases / 13 documents** (+1.9%); 10 round-trip, 3 are refused at L1, and violations are 0 — it found no new fidelity bug. Coverage is exhaustive over the ELIGIBLE slice — every non-`Rejected` case that carries a recognised check kind (consistency / inconsistency / positive- or negative-entailment / profile-identification) and is sanctioned `test:DIRECT` and/or `test:RDF-BASED` — NOT over the raw export: the 1 case tagged with NEITHER semantics, and any case carrying no recognised check kind, is selected by neither arm and its documents stay unmeasured.

**L2 — syntactic EL/QL/RL profile-membership checker (`profile`, bead sq-pbz04.4.2):** NOW

BUILT. `profile::profiles(onto: &Ontology) -> ProfileSet` runs a purely syntactic grammar walk

(W3C OWL 2 Profiles §2/§3/§4) over the structural model and returns a `ProfileSet` with three

fields — `el`, `ql`, `rl` — each a `Membership` enum: `Membership::In` (all axioms pass),

`Membership::NotIn(reason)` (first violation, fail-fast), or `Membership::Unknown(err)`

(extraction failure, only from `profile::profiles_from_extraction(&Result<Ontology, ExtractError>)`).

Convenience methods: `Membership::is_in()` / `is_not_in()` / `is_unknown()`;

`ProfileSet::in_all()` / `in_any()`. An empty ontology is `In` all three profiles. Terminating

by construction — no semantic reasoning, just a grammar walk over the finite acyclic structural model.

**L3 — terminating ALCH tableau (`nnf` + `tableau`, bead sq-pbz04.4.3):** NOW BUILT — the

consistency / class-satisfiability core. `tableau::consistency(&Ontology, Budget)` and

`tableau::class_satisfiability(&ClassExpression, &Ontology, Budget)` return a tri-state

`Verdict` — `Satisfiable`, `Unsatisfiable`, or `Unknown(UnknownReason)` — and

`tableau::consistency_from_extraction(&Result<Ontology, ExtractError>, Budget)` is the

fail-closed RDF-level entry: ANY extraction failure yields `Unknown(OutOfFragment)` BEFORE the

tableau starts (the checker never reasons over a partially-understood graph). The engine is a

completion-forest tableau with GCI internalisation, `⊓`/`⊔`/`∃`/`∀`/GCI rules matched modulo

the `rdfs:subPropertyOf` closure, **ancestor subset blocking** (sufficient precisely because

ALCH has no inverse roles), and chronological backtracking over `⊔`-branches. The full

termination / soundness / completeness argument — citing Baader–Sattler 2001, including why

subset blocking would be insufficient with inverses — is reproduced in the `tableau` module

docs (§3–§5). Budgets are **deterministic counts only** (`Budget { max_nodes,

max_rule_applications }`; wall-clock budgets banned); exhaustion yields

`Unknown(ResourceBudget)`, **never a verdict**. `nnf` provides the negation-normal-form

rewrite (`nnf` / `nnf_complement` / `is_nnf`) and the finite `subexpression_closure` the

termination argument rests on. HONEST BOUNDARY: verdicts are sound/complete ONLY for the exact

ALCH fragment (named classes, ⊤/⊥, ⊓/⊔/¬, ∃/∀ over named properties, GCIs, `subPropertyOf`,

ground ABox) — never beyond it; the implementation is not claimed worst-case optimal (ALC+GCI

satisfiability is EXPTIME-complete).

**Opt-in transitive roles (`dl_transitive` cargo feature, OFF by default, bead sq-zfwzq

):** extends the fragment to **ALCH + transitive roles** (Horrocks–Sattler *S with

role hierarchies* — still NO inverses / cardinality / nominals, which stay fail-closed): L1

recognises `owl:TransitiveProperty` as the feature-gated `Axiom::TransitiveObjectProperty`

(instead of refusing it), L2 classifies it per the profile grammars (IN EL §2, NOT-in QL §3,

IN RL §4), and the L3 tableau adds the **∀₊-propagation rule** (`∀R.C` at `x`, edge `x –S→ y`,

transitive `T` with `S ⊑* T ⊑* R` ⇒ add `∀T.C` at `y`) with the termination / soundness /

completeness argument EXTENDED AND WRITTEN OUT in `tableau.rs` module docs **§5a** (subset

blocking is UNCHANGED — sufficient precisely because there are still no inverses; the model

construction interprets `R^I = E(R) ∪ ⋃ E(T)⁺`). L4 dispatch routes any transitive ontology

STRAIGHT to the tableau (the only transitivity-complete branch; the RL/EL guards also

recognise the axiom kind fail-closed as defence in depth); a transitivity CONCLUSION in

entailment is decided by the two-step-chain refutation encoding (`O ⊨ Trans(R)` iff

`O ∪ {R(a,b), R(b,c), B(c), (∀R.¬B)(a)}` unsatisfiable — argued in `check.rs`). With the feature

enabled, a declaration-free conclusion role assertion may reuse a role kind established by

a transitivity-bearing premise; the checker adds only semantically inert declarations for

premise-confirmed roles during conclusion extraction and never guesses an unknown predicate.

With the feature OFF the crate compiles to exactly the pre-extension code (fail-closed refusal). The

`sparq-conformance` `dl-direct` arm enables it, graduating the corpus's transitive

consistency/entailment cases from abstentions to definitive verdicts (floors re-pinned with

evidence in `tests/dl_suite.rs`).

**L4 — fragment-dispatch checker + entailment-by-refutation (`check`, opt-in `dispatch`

feature, bead sq-pbz04.4.4):** NOW BUILT. `check::DirectChecker` (constructed with `new()` or

`with_budget(Budget)`) dispatches an extracted ontology IN ORDER — RL (via `sparq-reason`

materialization + clash scan, Theorem-PR1-precondition-CHECKED, divergence-guarded), EL (via

`sparq-reason-el`, triple-guarded: skipped-axioms / unapplied-axiom-kinds / ⊤-guard), QL

(always abstains `QlConsistencyPending` unless the opt-in `dispatch_ql` feature routes it to

`sparq-reason-ql`'s consistency checker, sq-fj8lj), else the L3 ALCH tableau —

returning `ConsistencyOutcome` / `EntailmentOutcome`: a tri-state verdict PLUS the `Branch`

that produced it (traceability). `entailment()` checks `O ⊨ α` per conclusion axiom by an

argued refutation encoding onto the tableau (`SubClassOf`, `ClassAssertion`,

`ObjectPropertyAssertion` via a fresh-class encoding, `EquivalentClasses`, `DisjointClasses`,

domain/range, and — since sq-pbz04.4.9 — `SubObjectPropertyOf(R,S)` via the

fresh-individual-pair lift `{R(a,b), B(b), (∀S.¬B)(a)}`, sound and complete because the

tableau's ∀-rule fires modulo the role hierarchy). Every guard fails CLOSED — uncertainty is a

typed `UnknownReason`, never a guessed verdict. **Refutation budget fallback (sq-pbz04.4.10):**

the tableau still OWNS every refutation (it is the only branch complete for the whole fragment),

but when — and only when — one exhausts the deterministic count budget, the SAME question is

re-asked of the RL/EL branches under their SAME guards, with the augmented model serialised by

the L1 forward renderer and its round-trip VERIFIED per call (re-extract, compare axiom

multisets). Strictly abstention-reducing: it can only replace `Unknown(ResourceBudget)` with a

definitive verdict, and any fallback abstention keeps the tableau's original budget reason. In

practice it is the RL branch that recovers — every encoding adds an ABox assertion the EL

classifier does not apply, so the EL arm always abstains today. **Conclusion anonymous individuals

(sq-pbz04.4.13):** a blank-node individual in the CONCLUSION is read EXISTENTIALLY (per the

official Direct-Semantics tests) — L1's skolem-constant reading is entailment-preserving on the

premise but would certify a WRONG `NotEntailed` on the conclusion, so before the refutation loop a

TREE-shaped anonymous assertion set (`a p _:x`, `_:x` typed / chaining to more blank nodes) **rolls

up** into an existential class assertion `a : ∃p.(⊓ types ⊓ ⊓ ∃q.⟨child⟩)` the tableau decides

SOUNDLY in both directions (so `somevaluesfrom2bnode` / `WebOnt-someValuesFrom-003` graduate to

genuine passes); any non-rollable shape — shared between two assertions, cyclic, a named/nominal

successor, or an unanchored free-existential root — abstains fail-closed

(`ConclusionAnonymousIndividual`), never a skolem `NotEntailed`.

**L5 — the conformance DIRECT-arm (`sparq-conformance`, opt-in `dl-direct` feature, bead

sq-pbz04.4.5):** NOW BUILT. `inference::dl_suite::run_direct_arm` runs the DIRECT-sanctioned

arm of the OWL WG export (`tests/w3c/owl2/all.rdf`) with **tri-state accounting

`{Pass, Fail, OutOfFragment(reason)}` — an abstention is NEVER a pass**: a

profile-identification lane (the L2 checker vs the export's POSITIVE `test:profile` tags

ONLY — the explicit-negative `owl:NegativePropertyAssertion` direction was MEASURED and not

adopted, because L2's `In` is fragment-grammar membership and cannot refute full-profile

membership (runner module docs); nothing inferred from a missing tag; the `test:species`

DL/FULL check stays deferred) and a Direct

consistency/inconsistency/entailment lane (the L4 `DirectChecker` under a PINNED

deterministic count budget). Floors are EXACT-pinned in `tests/dl_suite.rs`

(`DL_PROFILE_FLOOR` / `DL_DIRECT_FLOOR`, `==` not `>=`, so abstention-inflation and

regression both fail), mirrored as **`sparq extension`** scoreboard rows labelled **scoped

fragment — NOT full OWL 2 DL**, never folded into standards-conformance totals; the

dual-tagged tests' RDF-Based runs stay in the RL `owl_suite` / `el-suite` lanes (separate

semantics). Functional-syntax-only inputs (27 cases) and `owl:imports` are OutOfScope;

`test:status test:Rejected` is excluded.

**Scoped-fragment decision table — NOT full OWL 2 DL (grounded in code).** Deferral ledger

(live source of truth): `sparq-conformance/tests/dl_suite.rs` — `DOCUMENTED_DIVERGENCES`

(5 named rows; audited mechanisms M3/M5/M6; M1/M2/M4 FIXED and removed from the pin),

abstention counters `DL_DIRECT_ABSTAINED` / `DL_PROFILE_ABSTAINED`, pass floors

`DL_DIRECT_FLOOR` / `DL_PROFILE_FLOOR` — all EXACT-pinned (`==` not `>=`; both inflation and

regression fail CI). Design record: `research/owl2-direct-semantics-scoping.md`.

sq-pbz04.4.6

**L1 extraction boundary** (`extract.rs` `ExtractError` — one out-of-fragment triple refuses

the whole graph, never a partial extraction):

| Construct | L1 outcome | `ExtractError` variant |

|---|---|---|

| Named classes; ⊤/⊥; ⊓/⊔/¬; ∃R.C/∀R.C over a named property; GCIs; SubProperty; domain/range; ground ABox (`ClassAssertion`, `ObjectPropertyAssertion`) | Accepted | — |

| Cardinality (min/max/exact/qualified) | Refused | `OutOfFragment` |

| Nominals (`owl:oneOf`, `owl:hasValue`, `owl:hasSelf`); inverse properties (`owl:inverseOf`); property characteristics (Transitive/Functional/IFP/Sym/Asym/Refl/Irr) | Refused | `OutOfFragment` |

| `owl:sameAs` / `owl:differentFrom`; property chains; keys; `owl:disjointUnionOf` | Refused | `OutOfFragment` |

| Datatypes / data properties / data-range restrictions; a bare datatype-map IRI (`xsd:*`, `rdfs:Literal`, `owl:real`/`rational`) in ANY class position incl. an `rdfs:range`/`rdfs:domain` object (sq-pbz04.4.9) | Refused | `DataConstruct` |

| Malformed RDF list (unterminated, cyclic, branching, empty, orphan cell, `rdf:nil` as list cell) | Refused | `MalformedList` |

| Malformed class expression (missing filler/property, conflicting shapes, cyclic, bare blank) | Refused | `MalformedClassExpression` |

| Undeclared predicate (role-vs-annotation ambiguous); RDF 1.2 triple term | Refused | `Unclassifiable` |

**L4 dispatch — consistency** (`check.rs` `UnknownReason`; in-order, non-falling-through;

`Branch` set for traceability on every verdict):

|---|---|---|---|

| QL (in-QL; opt-in `dispatch_ql`, sq-fj8lj → sparq-reason-ql's `ql-consistency` checker over the raw triples) | Only past the QL crate's OWN capture accounting (`fully_captured()` ∧ `consistency_uncaptured == 0`; L2's `In` only routes, never justifies) | Yes (violation query matched — sound at any capture level by monotonicity) | `QlCaptureGap` (the QL crate's gap accounting); without `dispatch_ql`: `QlConsistencyPending` (always) |

**L4 dispatch — entailment** (all conclusion kinds routed through the complete ALCH tableau):

| Conclusion kind | Decides `Entailed` / `NotEntailed` | Abstains (`UnknownReason`) |

|---|---|---|

| `SubClassOf`, `ClassAssertion`, `EquivalentClasses`, `DisjointClasses`, `ObjectPropertyDomain` / `ObjectPropertyRange` | Yes (sound + complete via refutation encoding) | — |

| `ObjectPropertyAssertion` (fresh-class encoding — sound and complete, `check.rs` §4) | Yes | — |

| `SubObjectPropertyOf` (fresh-individual-pair encoding `{R(a,b), B(b), (∀S.¬B)(a)}` — sound and complete; sq-pbz04.4.9) | Yes | — |

| Tree-shaped conclusion blank node (rolls up to an existential class assertion; sq-pbz04.4.13) | Yes | — |

| Non-tree conclusion blank node (shared / cyclic / named-successor / free-existential root) | Never | `ConclusionAnonymousIndividual` |

| A future axiom kind without an argued encoding (none expressible today) | Never | `UnencodedConclusion` |

| Deterministic count budget exhausted mid-search | Never | `ResourceBudget` |

Deferred constructs — inverse roles, cardinality/functionality, nominals, transitivity,

`sameAs`/`differentFrom`, datatypes, keys — are each **rejected, never mis-mapped**, with a

named reason and unlock path in the deferral ledger: `sparq-conformance/tests/dl_suite.rs`

(`DOCUMENTED_DIVERGENCES`, `DL_DIRECT_ABSTAINED`, `DL_PROFILE_ABSTAINED`) and the design

record `research/owl2-direct-semantics-scoping.md`.

**Full OWL 2 DL front end (`sparq_reason_dl::owl2dl`, issue #7031, in progress).** The

ALCH layers above are being extended to OWL 2 DL (SROIQ(D)) by a hypertableau reasoner.

Its first layer is built: `owl2dl::extract(&dict, &triples)` reads the whole OWL 2 RDF

mapping (inverses, cardinalities, nominals, `hasSelf`, chains, keys, datatypes and facets,

`sameAs`/`differentFrom`, negative assertions, n-ary disjointness) into a typed

`owl2dl::Ontology`, every axiom carrying the input triple indices it came from. It stays

fail-closed: a triple it cannot place gives an `ExtractError` naming that triple.

Annotations are kept too (annotation axioms, plus ontology and reified axiom annotations in

`Ontology::annotations`), outside the logical axioms.

`owl2dl::check_dl(&dict, &onto)` runs the OWL 2 DL global restrictions (declarations and

typing, punning, reserved vocabulary, simple roles, property-hierarchy regularity,

anonymous-individual forests, operand sets, ill-typed literals, facets, datatype

definitions) and returns a `DlProfileReport`. It is fail-closed: `verdict()` is

`Some(false)` on a violation, `Some(true)` only when every restriction was checked, and

`None` when one was not (listed in `unchecked`: `xsd:pattern` syntax, `rdf:XMLLiteral`

content, an unloaded imports closure, anonymous individuals outside an anonymous forest,

literal values beyond the represented range such as a year past `i64` or a language tag

that is not well-formed BCP 47 (or, in an `rdf:PlainLiteral`, not a `langtag`), and the facet space of a bound outside the restricted

datatype's value space, and whether operands with cardinality restrictions are distinct). Cardinalities must be valid non-negative `xsd:nonNegativeInteger` or

`xsd:integer` literals; others are refused as unsupported. Lexical forms get no

whitespace normalisation (RDF applies no `whiteSpace` facet), and with unloaded imports

the violations an import could repair (undeclared entities, unknown datatypes) are

unchecked rather than definite.

`blocking()` lists the violations a reasoner must refuse. `owl:imports` is recorded in

`Ontology::imports`, never dereferenced.

`owl2dl::check(&dict, &onto, Budget::default())` is the reasoner: a hypertableau (Motik,

Shearer and Horrocks) over DL-clauses, with pairwise anywhere blocking, merging and

dependency-directed backjumping. It returns a `DlReport` with the profile report,

`consistency` (`Consistent`, `Inconsistent`, or `Unknown(reason)`) and, when consistent, a

`Classification` (unsatisfiable named classes, every entailed named subsumption, and the

`inferred` ones not asserted; `classification_unknown` says why a consistent ontology has

none, which happens when the shared classification budget runs out).

`owl2dl::Reasoner::new(&dict, &onto, budget)` answers single

`is_satisfiable(iri)` / `is_subclass_of(sub_iri, sup_iri)` queries by class IRI

(`Option<bool>`; `owl:Thing`, `owl:Nothing` and

classes no axiom mentions included; `None` when an unloaded import could change a negative

- answer). The decided fragment is SHOIQ(D) with `hasSelf` and `R∘R ⊑ R`: nominals

+ answer). `owl2dl::IncrementalChecker::check(&dict, &onto, budget)` rechecks successive

+ versions of an ontology and returns `(DlReport, Reuse)`: the same report as `check`, except

+ that it reuses the last decided answer when the logical axioms are the same

+ (`Reuse::Identical`, no reasoning) or a superset (`Reuse::Extension`: by monotonicity the

+ old inconsistency carries over, and old unsatisfiable classes and subsumptions are taken

+ without a test), so a reused answer may be decided where a fresh one ran out of budget.

+ Axioms are compared by the terms they name (each check may use its own `Dict`; an anonymous

+ individual by its blank-node label); the profile check and clausification always run, and a

+ refused version keeps the kept answer. The decided fragment is SROIQ(D) without the top and bottom properties: regular

+ property chains (`owl:propertyChainAxiom`, transitivity; each non-simple property gets an

+ automaton over the property words that imply it, and `∀R.C` follows its states), nominals

(`ObjectOneOf`, `ObjectHasValue`; a node labelled `{a}` is merged into `a`'s node, and with

nominals every class test runs with the ABox), number restrictions up to

`MAX_CARDINALITY`, and data properties: domain, range, sub- /

equivalent / disjoint data properties, `FunctionalDataProperty`, `DataSomeValuesFrom`,

`DataAllValuesFrom`, `DataHasValue`, data min / max / exact cardinality (qualified or

not), and positive and negative data property assertions, over data ranges of the OWL 2

datatype map (datatypes, facet restrictions, `DataOneOf`, `DataIntersectionOf`,

`DataUnionOf`, `DataComplementOf`, and named datatypes with one acyclic

`DatatypeDefinition`, which is expanded). Data edges end in concrete nodes; a datatype

check over the graph of value inequalities (per node, peeling, exact search over

enumerated `DataOneOf` nodes, and clique counting) decides the labels with

`owl2dl::data_ranges`. Literals are compared by value (`"1"^^xsd:int` and

`"01"^^xsd:integer` are one value; float `-0` and `+0` are two), and an ill-typed literal

in an assertion, `DataHasValue` or `DataOneOf` (e.g. `"sixteen"^^xsd:nonNegativeInteger`)

makes the ontology `Inconsistent`. Literal policies that decide verdicts: lexical forms

are not whitespace-normalised, so `" 1"^^xsd:integer` is ill-typed; an `rdf:PlainLiteral`

without `@` is ill-typed; `rdf:langString` is accepted as a datatype (it is RDF 1.1's, not

in the OWL 2 map); `xsd:hexBinary` and `xsd:base64Binary` share no values (OWL 2 §4.5);

the data domain has values outside every datatype of the map (the Direct Semantics allows

them), so the complement of the whole map is not empty, while `rdfs:Literal` is the whole

domain. A branch closed as undecided or unconfirmed never makes the alternatives after it

look forced: no subsumption is read off them.

Nominals are decided without SHOIQ's NI-rule: a complete branch is accepted only when its

graph provably unravels into a model (no blocked node keeps an edge to an individual, no

edge outside the tree joins two blockable nodes, and no number restriction at an

individual can count two copies of a repeated node). Otherwise the branch is closed as

unconfirmed, and when no other branch gives a model the answer is `Unknown(Unconfirmed)`.

Keys (`HasKey`, object property expressions including inverses, and data properties)

apply to named individuals only, as OWL 2 specifies: two named members of the key class

sharing a named value on every object property and a value on every data property are

merged. Data values are compared when the tableau fixed them to literals (ABox

assertions, `DataHasValue`); a pair that might share a value not fixed yet closes the

- branch as unconfirmed. A key on an object property with a transitive sub-property

- (a non-simple one) is `OutOfFragment`: the values it compares would lie along paths.

+ branch as unconfirmed. A key on a non-simple object property (transitive, or

+ implied by a chain or a transitive sub-property) is `OutOfFragment`: the values it compares would lie along paths.

Still out of the fragment, as

- `Unknown(OutOfFragment { construct, source })`: other chains, the top and bottom object and data properties

+ `Unknown(OutOfFragment { construct, source })`: a hierarchy the automaton construction finds

+ irregular or too large (`MAX_AUTOMATON_STATES`; the profile check reports irregular ones as

+ `NotInDl` first), the top and bottom object and data properties

in axioms (except `SubDataPropertyOf(D owl:topDataProperty)`), datatypes outside the map

without exactly one definition, cyclic or repeated definitions, literals of datatypes

outside the map, and a property used both as an object and as a data property. A data

question the oracle answers Unknown for (an XSD pattern with a block escape, a facet bound

outside the restricted datatype's value space, a value beyond the represented range, an

`rdf:XMLLiteral` literal), or a value-inequality graph outside the shapes the check

decides, gives `Unknown(DatatypeUnknown { source })`: a branch the check cannot decide is

closed as undecided, so the answer is `Consistent` only from a fully checked model and

`Inconsistent` only when every branch closed on a real clash. A blocking profile

violation gives `Unknown(NotInDl)`, an exhausted step budget gives

`Unknown(ResourceBudget)`, and unloaded imports turn `Consistent` into

`Unknown(ImportsNotLoaded)` with no classification; `classification_unknown` carries

`ResourceBudget`, `DatatypeUnknown` or `Unconfirmed`. It never guesses a verdict. Its answers are checked

against HermiT on seeded corpora (`tests/owl2dl_reasoner.rs`), one of data properties

and datatypes, one with nominals and one with keys; the constructs where HermiT departs from the Direct Semantics

(ill-typed literals, float zeros, `NegativeDataPropertyAssertion` compared by lexical

form, data booleans and single-value intervals under data cardinalities) are kept out of

that corpus and pinned by hand-written tests instead.

`owl2dl::data_ranges` answers the datatype questions the tableau asks of a data range

(`DataRangeExpr`: a datatype, a facet restriction, `OneOf`, `And`, `Or`, `Not`):

`is_empty`, `contains`, `has_at_least(r, n)` for data cardinalities, and

`conjunction_satisfiable(pos, neg, distinct, values)`, which asks whether `distinct`

pairwise different values exist inside every range of `pos`, outside every range of `neg`

and outside `values`. Each answer is a `Tri`: `Yes` and `No` are exact (rational bounds

without rounding, discrete floats with `-0` and `+0` distinct, the ±14:00 rule for

`xsd:dateTime`, strings of XML characters, and automata for XSD patterns, lengths, basic

language ranges and BCP 47 tags, `langtag`s only for `rdf:PlainLiteral`), and `Unknown` covers particular `rdf:XMLLiteral`

values (their XML content is not checked), a facet outside the datatype's facet space

(including an order bound outside its value space), a value no literal has, data ranges nested more than 64 deep, an XSD pattern this implementation does

not support (block escapes such as `\p{IsBasicLatin}`, or groups nested more than 64 deep),

and string searches over a fixed automaton budget (states, edges and automaton bytes).

From JavaScript the same pipeline (parse, `extract`, `check`) is `checkOwlDl(tbox, abox?,

options?)` in `@sparq-org/sparq`, backed by the separate, lazily-loaded `crates/sparq-dl-wasm`

bundle; it returns the report as JSON with the offending triples as N-Triples lines — see

[`../javascript-wasm/references/owl-dl.md`](../javascript-wasm/references/owl-dl.md).

## Common recipes

**1. OWL 2 RL closure + inconsistency report.** OWL includes RDFS; run the clash check on the materialized result.

```rust

use sparq_core::Graph;

use sparq_reason::{materialize, inconsistencies, Profile};

let (mut dict, mut triples) = Graph::parse_to_triples(owl_text, "turtle")?;

materialize(Profile::OwlRl, &mut dict, &mut triples);

let clashes = inconsistencies(&dict, &triples); // e.g. disjointWith / sameAs↔differentFrom

if !clashes.is_empty() { eprintln!("INCONSISTENT: {clashes:?}"); }

let g = Graph::from_parts(dict, triples);

# Ok::<(), String>(())

```

**2. Notation3 rules + facts in one document → entailed ground triples.** The rules and data live in the same N3 source; only ground facts survive the closure. RDF 1.2 quoted-triple TERMS (`<< s p o >>` / `<<( s p o )>>`) are first-class in rule bodies AND heads: premises match them structurally (variables inside the quotation bind, nesting included), heads derive them, and `reason_n3` interns ground triple terms via the Dict's content-addressed RDF 1.2 triple-term path (GH #2012). The opt-in `compiled-rules` path also matches them at the id level (`sq-6d43t`, see the compiled-rules section for the exact envelope); the incremental counting profile still disqualifies on them and falls back to the text engine. The N3 parser accepts at most 64 levels of `{ }` / `( )` / `[ ]` / `<< >>` nesting, counted together: one level more is a parse error (a cut inside `log:parsedAsN3` / `log:semantics`), never a stack overflow, on any thread with a 2 MiB stack, debug build included. Evaluation is bounded the same way (#6732): a term that rules build past 128 levels, or past the deepest term handed in as terms rather than text (a rule that wraps its conclusion one level deeper each round, or a chain of premise atoms), is dropped as a cut; nested `log:conclusion` / `log:supports` closures, backward proof steps and store-scoped clauses (`log:notIncludes`, `log:collectAllIn`, `log:forAllIn`) all draw on one stack allowance per run, so a chain of distinct documents through `log:semantics` cannot reset it (a nested closure past it fails the run with an error, a proof step or clause past it is a cut); and matching formulae (`log:includes`, formula-to-formula unification) takes no stack per statement. A cut is recorded on the run, so a later negation or aggregation is refused rather than reading missing facts as absent.

```rust

use sparq_core::dict::Dict;

use sparq_reason::reason_n3;

let n3 = r#"

@prefix : <http://ex/> .

{ ?x a :Human } => { ?x a :Mortal } .

:socrates a :Human .

"#;

let mut dict = Dict::new();

let closure = reason_n3(&mut dict, n3)?; // includes :socrates a :Mortal

for t in &closure { println!("{} {} {} .", dict.term(t[0]), dict.term(t[1]), dict.term(t[2])); }

# Ok::<(), String>(())

```

**3. Incremental RDFS maintenance** (data updates cost time ∝ the change, not a full re-materialize):

```rust

use sparq_reason::MaterializedGraph;

let mut g = MaterializedGraph::new(&mut dict, &base_triples);

g.insert(&[[alice, ty, person]]); // closure updated incrementally (one sweep over the delta)

g.delete(&[[alice, ty, person]]); // exact-count retraction; a still-derivable fact survives

assert!(g.contains(&[alice, ty, agent])); // entailed via subClassOf

let materialized: Vec<[u64; 3]> = g.closure(); // feed back into Graph::from_parts to query

```

> Note: an `insert`/`delete` touching a **TBox** triple (`subClassOf`/`subPropertyOf`/`domain`/`range`, and the OWL schema predicates) triggers a full rematerialize — watch `g.full_rebuilds()`. Keep ABox edits and schema edits separate when you care about incremental cost.

> A **meta** schema — an RDFS schema property (`rdf:type`, `subClassOf`, `subPropertyOf`, `domain`, `range`) is itself a sub-property or has a domain/range — needs a true fixpoint (#5090). `materialize_rdfs` and `MaterializedGraph` then run a semi-naive evaluation whose hierarchy rules step along raw schema edges, so the closure is complete and `why()` still explains every derived fact. In that mode every `insert` (TBox included) is incremental, and a `delete` runs DRed (overdelete, rederive, propagate) over the fixpoint, so its cost follows the consequences it touches rather than the closure size. Only a delete that makes the schema stop being meta rebuilds.

**4. Incremental N3 with a fallback check.** Term-level facts; verify you actually got the fast path.

```rust

use sparq_reason::{MaterializedN3Graph, n3::Term};

let rules = "{ ?x <http://ex/p> ?y } => { ?y <http://ex/q> ?x } .";

let mut g = MaterializedN3Graph::new(rules, &base_facts)?; // base_facts: &[[Term;3]]

g.insert(&[[Term::Iri("http://ex/a".into()),

Term::Iri("http://ex/p".into()),

Term::Iri("http://ex/b".into())]]);

if let Some(why) = g.fallback_reason() { eprintln!("running batch fallback: {why}"); }

let closure: Vec<[Term;3]> = g.closure();

# Ok::<(), String>(())

```

**5. Derivation proof (`explain` feature).** Returns ONE witness derivation of a triple from the asserted base; render as text or JSON.

```rust

// Cargo.toml: sparq-reason = { version = "0.1", features = ["explain"] }

use sparq_reason::MaterializedGraph;

let g = MaterializedGraph::new(&mut dict, &base);

if let Some(tree) = g.why(&dict, [alice, ty, agent]) {

println!("{}", tree.to_text()); // indented, root first; rule ids like cax-sco / rdfs9 / prp-trp

let json = tree.to_json(); // {"root":R,"nodes":[{"id":..,"conclusion":[s,p,o],"key":[ks,kp,ko],"rule":..,"premises":[..]}]} — "key" = lossless identity (whyN3 wire field too)

}

```

**6. `log:semantics` / `log:content` document access.** The engine does NO I/O of its own; supply a `Resolver` closure to decide what an IRI may dereference to (without one, an evaluation of those builtins counts as a cut, so a later negation or aggregation is refused):

```rust

use sparq_reason::n3::reason_n3_terms_with_resolver;

let resolver = |iri: &str| std::fs::read_to_string(iri.trim_start_matches("file://")).ok();

let closure = reason_n3_terms_with_resolver(src, Some("http://ex/"), Some(&resolver))?;

# Ok::<(), String>(())

```

**Import cycles always terminate (with a LIVE resolver).** N3 is Turing-complete, so a `log:semantics` document whose closure re-imports a document active up the resolution stack — directly (`A→A`), indirectly (`A→B→A`), or via a re-used node in a diamond — would otherwise spin forever once a real (filesystem/network) resolver is wired (the offline conformance harness never hit it). The engine tracks the formulae whose closure is in progress; re-entering one already in progress returns it **unclosed** (cwm's "a document already being loaded is not re-loaded") instead of recursing, so reasoning terminates. A diamond that re-uses a shared document across **sibling** branches is not a cycle and still resolves on every branch — only the pathological cyclic case changes; valid acyclic imports are byte-identical to before.

**Same-box materialization comparison (sparq vs Jena / VLog / Nemo).** To compare

sparq's closure materialization against other reasoners on the LUBM `(ABox+TBox)`

corpus, run `scripts/bench/materialize-same-box.sh` (`ONLY=sparq LUBM_UNIVS=1 …`

for the fast self-check; supply `VLOG=`/`NEMO=` binary paths for those columns).

The oracle is the **closure size** (pinned at `univ=1`: `owl=150589`,

`rdfs=126732`). The VLog and Nemo columns run **validated Datalog encodings**

(`bench/reason-encodings/{vlog/*.dlog,nemo/*.rls}`, `sq-hmd7l.30/.31`) that

reproduce sparq's closure **set-for-set** — so all three engines' closure counts

**AGREE** (folded into `count_crosscheck.same_ruleset_agree`). Critical honesty

caveat: this holds because sparq `reason owl` is the **full W3C OWL 2 RL/RDF** rule

table and the encodings transcribe exactly the rules the LUBM TBox exercises; a

**Jena** column, by contrast, has no full OWL 2 RL reasoner (its `OWL_MICRO`/

`OWL_MINI`/RDFS rule reasoners are OWL-subset + add axiomatic triples) so its

closure size *differs by construction* — recorded per column as a profile caveat,

never reconciled. Never read a raw closure-size delta as a correctness gap without

the profile.

## Gotchas / feature flags / prerequisites

- **Not in the *lean* wasm bundle, but wasm-portable.** `sparq-reason` pulls `regex` and (by default) `rayon`; it is never in the **lean** `sparq-wasm` triplestore bundle. For wasm or single-threaded builds use `default-features = false` (disables the `parallel`/rayon feature). The crate itself compiles to `wasm32-unknown-unknown` — `regex` (the N3 `string:matches` builtin) is pure-Rust and wasm-portable — and ships as the **tier-b `sparq-reason-wasm` ("W-reason") bundle** (sq-6qw3): a `Reasoner` exposing `materialize` / `entailed` / `materializeStats` / `reasonN3` (and, behind the bundle's opt-in `explain` feature, `why()` / `whyN3()` proof trees — the latter sq-ixc3.20: one witness derivation of an N3-derived triple under the same combined rules+facts document `reasonN3` consumes, powering the GUI's click-to-explain proof panel) for in-tab live inference, lazy-loaded on the showcase site's `/surface/inference` page and in the GUI workbench. There is no Noir/ZK toolchain requirement here — proofs are plain Rust structs.

- **Features:** `parallel` (default, rayon-parallel fixpoint), `explain` (NON-default — enables `why()`/`why_with()` and the `explain` module; zero hot-path cost when off, and `why` methods don't exist without it), `d-entail` (NON-default — enables `Profile::D` + the `dtype` module; zero code when off — the lean default/wasm build is byte-identical, `sq-e5atd`), `rif-core` (NON-default — enables the `rif` module: the RIF-Core monotone-Horn rule front-end over the N3 chainer with range-restriction safety; zero code when off, no new `Profile` variant, `sq-rh4gu`), `substrate-join` (NON-default — the RDFS predicate join + the rdfs9 type join + the OWL-RL `Δ⋈full` delta adjacency (`sq-qonbz.2`) drive the SHARED `sparq-substrate::join` kernels; `sq-yk6or` + `sq-pbz04.1.1` + `sq-qonbz.2`, see next bullet), `substrate-compare` (NON-default — the `compare` module: the SHARED `sparq-substrate::compare` SPARQL term total order implemented for dictionary ids, so entailed-solution ordering is parity-identical to the engine's `ORDER BY`; zero code when off, `sq-pbz04.1.2`, see the bullet after next), `compiled-rules` (NON-default — the `n3::compiled` module: id-level COMPILED N3 evaluation for the access-control rule subset over the shared substrate join kernels; zero code when off, `sq-zgbso.3`, see the Key-APIs compiled block).

- **Shared join kernels (`substrate-join`, opt-in, `sq-yk6or`, epic `sq-pbz04`).** The RDFS single-pass predicate join — rdfs7 (subPropertyOf rewrite), rdfs2 (domain typing), rdfs3 (range typing), keyed on the asserted triple's predicate — and the rdfs9 subclass-typing join (`sq-pbz04.1.1`, keyed on the type-assertion's OBJECT column: the "orientation" is just a different `JoinKeys` probe-column index) drive the *same* `sparq_substrate::join::{build_table, probe_emit, hash_probe_serial}` hash-join body the SPARQL engine drives (epic `sq-qonbz` Phase 3, #1300). The reasoner supplies its OWN `JoinKeys` (predicate-keyed) + its OWN `Budget` (the unbounded `NoBudget`; materialisation runs to completion — a closure-level budget is a fixpoint concern, installed around the whole call, not per-join), monomorphically — no `Box<dyn>`/vtable on the probe loop. This is the end-to-end proof of "share join logic across the engine AND the reasoners" (`research/shared-eval-substrate.md` Phase 5). **Behaviour-neutral:** the materialised closure is byte-identical to the hand-rolled `FxHashMap` adjacency path (asserted per-branch by `rdfs::tests::substrate_join_emits_identical_plain_branch` / `substrate_join_emits_identical_type_branch`, and whole-closure by `closure_is_byte_identical_across_join_paths`, which runs in BOTH feature states); only the join machinery changes. **OFF by default** so the byte/bundle ratchets stay exactly the hand-rolled path; the only deps it pulls (`sparq-substrate` `rows`+`join`, `smallvec`) are already in the crate's tree. **Residual disposition (`sq-pbz04.1.1`):** the `PropExpand` inverseOf/Symmetric predicate-rewrite branch is RETAINED hand-rolled *permanently* — its per-match combine is data-dependent (the `swapped` flag picks the subject/object orientation per matched build row) and cascades into a second dom/rng join keyed on the DERIVED predicate, a variable-arity shape the kernel's one-fixed-row-per-match combine cannot express without rebuilding the rule structure around it (full rationale in `substrate_join.rs`; the oriented emission is pinned by `rdfs::tests::prop_expand_inverse_types_through_oriented_domain` so any future adoption attempt inherits a red/green harness). **OWL-RL delta adjacency (`sq-qonbz.2`, NOW SHIPPED under this same feature):** the semi-naive `Δ⋈full` adjacency for `prp-fp` (functional), `prp-ifp` (inverse-functional), and `prp-trp` (transitive) is also behind `substrate-join`. A persistent `DeltaAdj` struct (two `DeltaTable`s — forward `out_tbl` keyed on `[p,s]`, backward `inc_tbl` keyed on `[p,o]`) replaces the per-round nested `FxHashMap` probes; `extend_one` grows both tables incrementally as new delta triples commit, and `probe_out`/`probe_inc` emit results via a generic `FnMut(Id)` closure (monomorphised, no `Box<dyn>`, no vtable — `check-no-dyn-dispatch.py` is clean). **Behaviour-neutral:** the OWL-RL ratchet output is byte-identical in both feature states; the three probe paths (`prp-fp` forward, `prp-ifp` backward, `prp-trp` backward) are pinned by `tests/substrate_join_owl.rs` (8 required-feature tests: fp/ifp/trp alone and in combination, closure-length and no-chain guards). UnionFind (`sameAs` merge) is NOT touched by this change.

- **Shared term total order (`substrate-compare`, opt-in, `sq-pbz04.1.2`, substrate seam 3).** The `compare` module implements the substrate's `CompareTerm` trait for the reasoner's term representation — a dictionary `Id` resolved against its `Dict` (`compare::IdTerm`) — so `compare::compare_ids` / `compare::sort_ids` order ids under the *same* `sparq_substrate::compare::compare_terms` total order the SPARQL engine's `ORDER BY` drives: error/unbound < blank < IRI < literal < RDF 1.2 triple term; literals numeric-aware (with the `exact_cmp` f64-collapse recheck for distinct integers past 2^53), then strict typed/temporal (`xsd:dateTime`/`xsd:date` by TIMELINE via the shared `sparq_core::temporal::ExactTimeline` — cross-timezone order, not lexical; booleans; same-tag language strings; same-other-XSD lexically), then lexical string fallback; triple terms component-wise through the dict's structural component ids. **Ordering parity is pinned byte-for-byte against a REAL engine `ORDER BY`** over the same materialised closure (`tests/compare_parity.rs`, a mixed IRI/bnode/literal/triple-term fixture whose entailed rows participate); the observation hooks reuse the shared machinery (`ExactTimeline`, the substrate `Num`/`Dec` tower, `parse_xsd_f64`) rather than reimplementing it, and the small `Num::of_literal` borrowed-parts mirror is anti-drift-pinned by a unit test against the substrate itself. Adopted MONOMORPHICALLY — `IdTerm` is a generic `CompareTerm` impl, no `Box<dyn>`/`&dyn` between the sort loop and the comparator (`scripts/check-no-dyn-dispatch.py` lists the module). **Purely additive:** no materialiser calls it — which triples are entailed and their emission order are byte-identical in both feature states; undecidable pairs (e.g. `NaN`) collapse to `Equal` exactly as the engine's sort does, and equal-comparing DISTINCT terms (equal values across datatypes, equal instants across timezones) keep stable-sort input order on both sides — the engine's own tie semantics, not a divergence.

- **Two value levels.** RDFS/OWL APIs work on dictionary `Id`s (`materialize*`, `Materialized(Owl)Graph`); N3 batch APIs intern into a `Dict` (`reason_n3`), while term-level N3 (`reason_n3_terms`, `MaterializedN3Graph`) works on `n3::Term` and is **not interned** (formula `{ … }` terms have no dictionary id). Don't mix the two.

- **The materialize → from_parts seam.** `materialize` mutates `(Dict, Vec<[Id;3]>)` *before* indexes are built. Use `Graph::parse_to_triples` (not `Graph::load_str`) so reasoning runs between parse and index build; then `Graph::from_parts`. It interns any vocabulary terms it needs and is idempotent (a second call adds nothing).

- **RDFS scope is deliberate:** the non-explosive subset (rdfs2,3,5,7,9,11 — subClass/subProperty/domain/range). No axiomatic or reflexive `rdfs:subClassOf`/`type` triples (they add no useful inferences and explode the store).

- **D-entailment (`Profile::D`, opt-in `d-entail`) scope + caveats:** materializes the rdfD1 datatype-typing rule — a well-formed literal `"l"^^d` of a *recognized* datatype `d` (the `Recognized` map; `xsd:string`/`rdf:langString` always, `Recognized::standard()` adds the numeric/boolean/temporal core) entails `"l"^^d rdf:type d`. The emitted typing triples are **generalized** (literal in subject position) — feed the closure to a query only after dropping literal-subject rows (they can never be a SPARQL answer; this is also why the W3C `d-ent-01` test correctly returns NO rows). The load-bearing invariant is **value-space equality** via `d_value_eq`: `"1"^^xsd:integer` ≡ `"1.0"^^xsd:decimal` (the integer/decimal value spaces coincide), compared as a CANONICAL DECIMAL STRING — **never an f64 fast path** (f64 silently aliases integers past 2^53 and loses decimal precision). `float`/`double` are a DISJOINT IEEE-754 value space; `date` and `dateTime` are disjoint temporal families. NOTE: the SHARED SPARQL term total order now lives in `sparq-substrate::compare` (`compare_terms` over the generic `CompareTerm` trait — error/unbound < blank < IRI < literal < triple, numeric-aware + strict typed/temporal + string fallback; epic `sq-qonbz` Phase 4, `sq-vezew`, #1300-chain). A reasoner that orders entailed solutions (RIF `order`, an EL/QL `ORDER BY` over a materialised answer set) reuses it by implementing `CompareTerm` for its own term type — the same monomorphisation seam `substrate-join` uses for `JoinKeys`; sparq-reason now SHIPS that impl for dictionary ids behind the opt-in `substrate-compare` feature (`sq-pbz04.1.2`, see the shared-term-total-order bullet above). The trait carries an `exact_cmp` **f64-collapse recheck** hook (`sq-rikm7`): the numeric arm coerces to f64 for speed, and when two operands tie there `exact_cmp` recovers the exact order of distinct integers past 2^53 / high-precision decimals — so a reasoner `ORDER BY` / `MIN` / `MAX` agrees with the relational `=`/`<` rather than falling into the very f64-aliasing this caveat warns about (return `None` from it if your term type has no exact numeric tier). D's typed *value-space-equality* comparator (`d_value_eq`, used for entailment not ordering) stays reasoner-resident for now; D-inconsistency (ill-typed-literal / value-space clashes) and cross-type value-space *subset* reasoning are tracked-not-yet-shipped here (epic `sq-pbz04`).

- **OWL 2 RL is sound but INCOMPLETE for class classification.** Running `Profile::OwlRl` / `--reason owl` over an EL ontology returns a `rdfs:subClassOf` hierarchy that silently omits derivable subsumptions: the RL/RDF rule set's completeness theorem is scoped to *assertional* conclusions, and class classification is a TBox-conclusion task. Two mechanisms, stated precisely — (a) RL has **no TBox conjunction-composition rule**: `B ⊑ C`, `B ⊑ E` ⊬ `B ⊑ C ⊓ E` (`scm-int` only decomposes; `cls-int1` composes only over *individuals*), so `C ⊓ E ⊑ D ⊬ B ⊑ D`; (b) RL never **introduces or reasons through a fresh existential successor**, and `ObjectSomeValuesFrom` in *superclass* position is outside the RL grammar entirely. Caveat worth knowing so you calibrate correctly: sparq implements `scm-svf1/2`, so an existential bridge whose *both* restriction nodes already appear syntactically (`A ⊑ ∃r.B`, `B ⊑ C`, `∃r.C ⊑ D`) **is** in fact derived by this repo's RL — the gap is real but narrower than "RL misses every existential subsumption". Mechanism (a) is the one pinned by an in-repo differential (`crates/sparq-cli/tests/el_cli.rs::el_derives_what_rl_cannot`). For the **complete** class hierarchy use `sparq-reason-el` (above) — via the library, or the CLI's `classify` / `--reason el` under the opt-in `el` feature — not more RL rules.

- **The RL materializer is COMPLETE for the assertion-style RL/RDF rules — the W3C OWL-RL conformance row is at the RL ceiling (sq-350ms).** Every rule with a positive-assertion head in Profiles §4.3 Tables 5/6/9 is implemented (the `owl.rs` per-rule status table + `research/inference-completeness-audit.md` §2/§2b are the per-rule proof). The 13 documented OWL-RL conformance divergences are PROVABLY outside the RL profile, **not** missing rules: TBox-axiom conclusions, invented class expressions (`owl:complementOf`/`unionOf`), reified `owl:AllDifferent` structures, the `prp-pdw`/`prp-fp`/`prp-ifp` **contrapositives** (RL has NO rule producing `owl:differentFrom` between INDIVIDUALS — `dt-diff` emits it only between unequal-value literals, otherwise it appears only in clash bodies), `owl:ReflexiveObjectProperty` (EXCLUDED from the RL grammar — there is no `prp-rfx`), and datatype-range INTERSECTION. They stay documented divergences (closing them would be unsound or beyond-profile); the inference ratchet HOLDS — see `inference-conformance-report.md` and the central scoreboard (`scoreboard::SUITES`, CI job `inference-conformance`) for the current pinned count. Multi-round assertion-rule completeness and the prp-pdw/prp-fp soundness boundary are pinned by in-crate guards in `owl.rs::tests`; the per-divergence disposition pass (sq-pbz04.1.3) re-audited all 13 from the raw export premises/conclusions (verdict: 13/13 PERMANENT, zero in-profile fixes), tagged every report-facing rationale `PERMANENT — …` with its rule-level grounding, and pinned tag+grounding with an in-crate disposition test in `owl_suite.rs`.

- **OWL incremental fallback is silent.** `MaterializedOwlGraph` drops to `OwlMode::Fallback` (re-materializes via `materialize_owl_rl` every mutation, still correct) when the base uses `owl:sameAs`, Functional/InverseFunctional, property chains, restrictions, cardinality, hasKey, oneOf, intersection/union — and on any TBox mutation. Check `.mode()` / `.full_rebuilds()` if incremental cost matters. These usually live in a static TBox, so the mode is decided once at load.

- **`MaterializedN3Graph` keeps the caller's blank nodes apart from every other blank (GH #6775).** A caller's `Term::Blank(l)` (in `new`'s base, `insert`, `delete`, `contains`, `why`) is the caller's own node, never one of the rules document's blanks (the parser's `[]` labels `_b1`, `_b2`, … or a written `_:x`) nor one minted at run time. `closure()` and `why()` show caller labels unchanged and every other blank in the reserved `N3_GRAPH_BLANK` space (`__d.` + its label: the document's `_:x` is `_:__d.x`), so output terms are distinct exactly when the nodes are and `contains(t)` holds for every `t` in `closure()`. A label `__d.<label>` passed in names that graph node. A `__d.` label that `closure()` could never return is refused: `new` returns `Err`, while `insert`, `delete` and `contains` ignore the fact. Documents parsed at run time (`log:parsedAsN3`, `log:semantics`) get their blanks standardized apart by the engine as `__rp{k}_<key>_<label>`, in every entry point including `reason_n3_query`, so their text cannot spell a blank of the source, the query or the caller's. `key` is specified: the first 8 bytes (16 hex digits) of SHA-256 over `"sparq-n3-runtime-doc\0"`, then the text and the base, each preceded by its byte length as a big-endian `u64`; so a label depends only on the document, is the same on every build, and is stable in exported proof keys. Two documents with one key fail the run. A runtime-document table (a run's, or a `MaterializedN3Graph`'s for its whole life) keeps a constant-size entry per distinct document (SHA-256 digest and label prefix, not the text) and takes at most 100,000 documents; one more fails the run (`runtime-document limit exceeded`, recorded as a cut). A source blank spelled exactly as a runtime blank (`__rp{k}_<16 hex>_<label>`), whether an exported closure or a person wrote it, names that runtime document's blank and does not move `k`, so `reason_n3_pass_all` over its own output stays a fixed point and an annotation on an exported runtime blank joins the reparsed node. A `MaterializedN3Graph` keeps its runtime-document table (and `k`) for its whole life, shared by rebuilds and `why()`, so a returned runtime blank can be annotated through its `__d.` label and stays the same node. `why_document_with(fact, opts)` explains the graph's closure as `why_with` does (same lifetime runtime-document table, `None` for a fact outside that closure) but takes and shows blanks in the rules document's own labels, as `reason_n3` prints them. For a standalone document (no graph) `why_n3_document(src, fact, opts)` (feature `explain`) is a batch evaluation of `src` exactly as `reason_n3` runs it, and returns `None` for every fact, asserted ones included, when that evaluation fails (e.g. an unstratifiable negation cycle); the WASM `whyN3` uses it, and it is tested to explain every triple `reasonN3New` derives from document blanks and from runtime texts spelling `_:__bs0_x`, with and without a later `log:notIncludes` rule.

- **N3 incremental qualification is narrow.** `MaterializedN3Graph` only runs `N3Mode::Counting` (truly incremental) for a monotone, input-stratified rule fragment: forward rules with ground-IRI predicates, no conclusion blank nodes, builtins limited to the parity whitelist (`log:uri`, `log:equalTo`/`notEqualTo`, `string:concatenation`/`scrape`/`encodeForUri`), and negation only via the store-scoped `?x log:notIncludes { … }` idiom over input-only predicates. Base facts containing formula values with variables (including inside lists or triple terms) also use the checked fallback: counting emission requires recursive groundness, while batch preserves formula-scoped variables. `insert` accepts these values and switches to fallback under the same `ClosureLimits`; deleting them allows counting to resume. Ground formula values remain eligible, and base facts with variables outside formulas are still ignored, both by `insert` and by `new` / `with_limits`. Anything else → `N3Mode::Fallback`; always consult `.fallback_reason()` (`None` ⇔ counting active). `MaterializedN3Graph::new` refuses a rules document that negates through a dependency cycle; if a later rematerialization is refused (e.g. a nested closure over a cyclic formula), the closure fails closed to the base facts and `.stratification_warning()` says why. The full *batch* N3 engine (`reason_n3`) supports the much larger `math:`/`string:`/`list:`/`time:`/`log:` builtin set and goal-directed `<=` rules.

- **N3 `math:` comparisons follow XPath numeric type promotion by DATATYPE (GH #6745).** `math:greaterThan` / `lessThan` / `notGreaterThan` / `notLessThan` / `equalTo` / `notEqualTo`, and the check a functional `math:` builtin runs against an already-bound object (`(1 2) math:sum 3`), promote both operands as XPath `op:numeric-*` does: an integer (any derived integer type) or `xsd:decimal` pair compares EXACTLY on its digits via the substrate's `cmp_plain_decimal` (arbitrary precision — `9007199254740993 math:equalTo 9007199254740992` does NOT fire, nor do values past `i128`); with an `xsd:float` and no `xsd:double` both sides are promoted to `xsd:float` (`0.1 math:equalTo "0.1"^^xsd:float` fires); with an `xsd:double` both are promoted to `xsd:double`. `NaN` is unordered, so every comparison but `notEqualTo` is false. A bare N3 numeral takes its datatype from its lexical form (`1` integer, `1.0` decimal, `1e0` double); a literal of a non-numeric datatype (a string) is still coerced by lexical shape, as EYE does; an ill-typed operand (`"1.5"^^xsd:integer`, `"-1"^^xsd:positiveInteger`) never matches. A typed numeric literal gets XSD `whiteSpace=collapse` (`" 3"^^xsd:integer` is 3; `"3 4"^^xsd:integer` stays ill-typed); a string operand is trimmed in the bound-object check (`(1 2) math:sum " 3"` fires) but not in the six comparisons. The one non-XSD form read is `"inf"` / `"-inf"` / `"NaN"`^^xsd:decimal — how a non-finite f64 fallback result is rendered (`(0.5 -1024) math:exponentiation ?x`) — which reads as ±INF / NaN, so such a result still matches a bound `"INF"^^xsd:double` and later comparisons on `?x`. Arithmetic RESULT datatypes and lexical forms are unchanged (EYE-compat rules below).

- **N3 `math:` exact arithmetic is on the SHARED substrate tower (`sq-pbz04.5.1`, seam 2).** The chainer's exact add / subtract / multiply / negate / abs core (and the scale-aligned comparison the max/min and value-equality paths use) DELEGATES to `sparq-substrate::numeric::Dec` — a base, non-optional `numeric`-slice dependency, the SAME exact fixed-point `mant * 10^-scale` decimal the SPARQL engine's FILTER/BIND path drives — so the reasoner and the engine can never diverge on exact-decimal arithmetic (`0.1 + 0.2` is exactly `0.3`; `('2.7' '2') math:difference` is exactly `0.7`). The private `NumVal` enum stays a thin EYE-compat ADAPTER over that core: EYE's own edges are byte-identical and stay adapter-resident — lexical-shape string coercion, the `numval_term` result rendering (whole-`f64` → `xsd:integer`), `math:remainder`'s divisor-sign integer semantics, `math:integerQuotient`'s floor, `math:quotient`'s scale-34 exactness rule (non-terminating → `f64`, exact integer/integer → `xsd:integer`, NOT substrate `Dec::checked_div`'s always-decimal scale-18 rounding), integer `math:exponentiation`, and the `Int`-collapse rendering of floor/ceiling. The i128↔i64 wrinkle: the chainer `Int` tier is `i128` while substrate `Num::Int` is `i64`, so an out-of-`i64`-range integer is carried as substrate `Dec { mant, scale: 0 }` (exact for the full `i128` range; a mantissa overflow falls back to `f64` exactly as before). N3/EYE differential + expressivity floors and `RIF_CORE_FLOOR` are all byte-identical (the closure is unchanged; a direct old-`NumVal`-vs-substrate differential over the `>i64::MAX` / `0.1+0.2` / INF-NaN / `2.7-2` matrix pins it).

- **An N3 forward closure that never reaches a fixpoint is refused (GH #6757).** Each forward closure (one document's fixpoint over all its strata, and each nested `log:conclusion` closure on its own) may run `ClosureLimits::max_rounds` rounds (default 1,000,000) and hold `ClosureLimits::max_facts` facts, asserted and derived (default 50,000,000). Past either limit the call returns `Err("n3: forward closure limit exceeded …")` and records a cut, so no entry point returns the truncated closure, and `MaterializedN3Graph` fails closed as it does for any refused rematerialization. A semi-naive closure needs about one round per step of its longest derivation chain, so a linear walk over N edges needs about N + 2 rounds. Raise the limits with `reason_n3_with_limits` / `reason_n3_terms_with_limits` for longer finite walks, or lower them to fail faster. Rules whose **terms** grow (a string or list that doubles each round) are caught by `ClosureLimits::max_term_bytes` instead (GH #6771, default 16 MiB). In the **text engine**, the terms it builds are sized from borrowed inputs and charged to the run's limit **before** they are built:

- **Substitution under bindings** goes through one primitive, `bounded::substitute` / `substitute_deep`. The raw `apply` is private to `n3/bounded.rs`; that privacy is the guarantee, and the guard test `substitution_goes_through_the_bounded_module` is only a lexical tripwire for a crate-internal copy. This covers premise patterns, conclusions, scope and collection templates, list generators, backward-rule projection and builtin arguments.

- **Every non-numeric builtin result, and a functional builtin's data-list arguments.** Every functional builtin has a size entry in `output_bytes`, an exhaustive match: a loose bound over the limit is refined to the exact size without building anything. The other result paths size their term from the borrowed input the same way: `log:uri` both ways, `log:dtlit` reversed, the member or `(index member)` pair `list:member` / `list:in` / `list:iterate` bind, the tail a virtual `rdf:rest` of a list value binds (in matching and in formula containment), and the literal `log:content` returns.

- **Numeric results** ([GH #6901](https://github.com/sparq-org/sparq/issues/6901)): the forward and reverse results of the arithmetic and other numeric builtins, counts and date parts are sized from the computed value (digit count, decimal scale, sign, exponent) before the literal is rendered, so a decimal whose scale grows each round is refused like a growing string. `string:concatenation` sizes its numeric pieces the same way, without rendering them.

- **The list `log:collectAllIn` collects** and **the formula `log:conclusion` returns.**

- **The formula `log:parsedAsN3` / `log:semantics` returns.** The parser charges every byte it keeps before allocating it: each string (the initial base, decoded literals, expanded prefixed names, resolved IRIs, directive prefixes and bases), each term node once, and each copy of a term at its full size (a subject or predicate shared by a `;` / `,` list, a formula included). An expanding parse stops near the limit; once the parse returns, the formula is sized again at the size it will have once its blank labels are standardized apart (`__rp{k}_{key}_…`), and refused before any label is rewritten.

Binding a variable to a term that already exists (premise matching, `log:includes`) copies that term; it builds nothing new and is not sized again.

`tests/n3_builtin_alloc.rs` counts heap bytes with a counting global allocator. For each builtin result path, substitution, `log:collectAllIn` list and `log:conclusion` formula it checks that an oversized term is refused, and that it was not built first: the heap peak during evaluation stays within half the term's size of a control run that derives nothing large. Where the evaluation already holds copies of an input as large as the term (URI encoding, case mapping, `log:uri`, `log:dtlit` reversed, list generators, virtual `rdf:rest`, `list:first` / `list:last`, `time:timeZone`), it is the bytes allocated that must stay within half the term of the control's. For `log:conclusion`, whose nested closure copies its statements many times over, the bytes are counted from the closure's last resolver read. `log:content` is checked for the refusal only: its literal takes the resolver's string without copying it.

Past the limit, the call returns `Err("n3: forward closure limit exceeded: … max_term_bytes …")` and the cut is recorded. Every closure of the run fails, rather than aborting on a failed allocation. The size is approximate: string bytes plus a fixed cost per node. It bounds each derived term, not total memory: many distinct terms just under the limit are bounded only by `max_facts`.

**Not covered:**

- the document's own parse, which is not charged: its memory is bounded by its input text. A `log:parsedAsN3` / `log:semantics` parse is charged; beyond its allowance it holds only a scratch copy of one token, or an error message quoting one, at a time (each bounded by the length of the source token), the spare capacity of its strings, vectors and maps, its fixed-size state, and the text it parses;

- the text a resolver supplies (`log:content`, `log:semantics`), which the caller allocates before it is sized (the literal or formula built from it is refused);

- total memory: the rows of one round are bounded only by `max_join_rows` (below), which is unbounded unless set; set it, as `max_facts`, to bound a run's memory;

- the steps of a formula-scope search beyond the matches it finds (each search has its own step budget, `CONTAINMENT_BUDGET`, and a search it stops is a cut), and the pairings formula unification tries (`formula_unify`: a `{ … }` pattern against a `{ … }` value), which yields at most one binding and so adds no rows. Each unification has its own step budget: `UNIFICATION_BUDGET` steps, plus a free allowance for its outermost formula match that covers a search that never backtracks and is dropped when that match ends, so it never tops up the budget. A unification that runs out does not match, and the run records a cut (`formula unification exhausted its step budget`), so a negation or aggregation that read it is refused. The unifications inside one formula-containment search share one such budget; one that runs out stops the search as a containment cut ([GH #6953](https://github.com/sparq-org/sparq/issues/6953)).

**Join work per round (GH #6938).** `ClosureLimits::max_join_rows` bounds the binding rows and rule firings one round may produce, counted together; each round (and each nested closure) gets it afresh. **The default is unbounded (`usize::MAX`)**: that sentinel turns the accounting off entirely, so the default never refuses. It is opt-in, like a lowered `max_facts`. Without it a premise of k unconstrained patterns over n facts builds n^k rows in one round however few facts it concludes. Every engine (text, `compiled-rules`, the incremental counting path) charges the same things: a **row** for each binding row a step that can multiply rows produces (a join atom's stored-fact matches, backward proofs and semi-naive delta seeds; `list:member` / `list:in` / `list:iterate`; each match a formula-scope search finds, for `log:includes` / `log:notIncludes` / `log:collectAllIn` / `log:forAllIn` over a written formula; the rows of store-scoped clauses such as a `log:notIncludes` body), and a **firing** for each conclusion triple a complete binding instantiates (the transitivity fast path included), new or not. Filters and functional builtins keep at most one row per input row and are not charged. The text and counting engines charge each row before storing it; the compiled hash join checks the allowance once per probed candidate and charges its output in one batch; every engine charges a rule's firings in one batch before instantiating any. Past a set allowance the call returns `Err("n3: forward closure limit exceeded: … max_join_rows …")` and records a cut. An N3 query charges its premise rows over the closure as one more round. The text and compiled engines charge the same per round on `tests/n3_join_work_limits.rs`'s fixtures (the compiled evaluator's first round of a stratum is naive, as the text engine's is); in general their schedules differ (debug builds' closing naive round, the transitivity fast path), so near a boundary they can refuse differently. The counting engine's rounds are propagation waves: past the allowance it rebuilds through the batch engine under the same limits, so it never refuses a closure the batch engine accepts, but a mutation whose wave fits is kept even when a from-scratch batch round over the new facts would not fit.

The opt-in `compiled-rules` evaluator is covered ([GH #6855](https://github.com/sparq-org/sparq/issues/6855)): see "Compiled-rules limits" above.

**The incremental counting engine behind `MaterializedN3Graph` is covered ([GH #6854](https://github.com/sparq-org/sparq/issues/6854)).** `MaterializedN3Graph::with_limits` takes the graph's `ClosureLimits` for its whole life (`new` uses the default). On the counting path each whitelisted builtin substitutes its subject and object through `bounded::substitute` (so a `( … )` argument list is sized before it is built) and sizes its result with the text engine's own checkpoint (`output_bytes` for `string:concatenation` / `scrape` / `encodeForUri`, the shared `log:uri` sizing both ways); conclusions are variables, IRIs and literals and build no new term. Each propagation (a construction or rebuild, one `insert`, one `delete`) is charged one round per wave, and per round of a recursive layer's local fixpoint, against `max_rounds`. Each new distinct fact is checked against `max_facts` as it is collected, and so is the closure after each wave (the last included): a closure of exactly `max_facts` facts is accepted, and none larger is published. Past any limit the graph rebuilds through the batch engine under the same limits: when that refuses, the graph fails closed (`new` / `with_limits` return the `Err`; after a mutation the closure is the base alone, `stratification_warning()` holds the error and `fallback_reason()` names the limit) until a mutation brings it back within them. The counting path's rounds are propagation waves, not the batch engine's fixpoint schedule, so under equal round or fact limits the graph can hold a closure that a from-scratch batch run near the boundary refuses. `tests/incremental_n3_closure_limits.rs` checks that the graph and the batch engine agree at every `max_term_bytes` it sweeps, through construction, insert and delete, on its fixtures.

**Deliberate over-refusal:** a builtin's argument list is itself a term it builds. So `log:conjunction` over many copies of one large formula is refused when the copies together pass the limit, even if the merged result would fit.

- **A formula-level `@forAll` binds only in its formula (GH #6754, the Team Submission's quantification rules).** A document-level `@forAll :x` is one variable, `?__ua.<iri>`, everywhere after it (unchanged). Inside a formula, `@forAll :x` makes each later mention of `:x` in that formula and its inner formulae (until an inner formula re-declares `:x`) the variable `?__uf.<n>.<iri>`, where `n` is the number of formula boundaries between the mention and the declaring formula (a de Bruijn index). Consequences: (1) a rule's premise and conclusion, sibling formulae, and a nested re-declaration never share a variable; (2) the name depends only on the formula's own structure, so two copies of one closed formula are the SAME term (`log:equalTo` holds, `log:notEqualTo` does not), wherever each sits; copies that declare DIFFERENT IRIs are different terms, as blank labels are; (3) the `.` keeps every generated name outside the quickvar lexical space, so no `?…` can spell or capture it. In a rule `{ P } => { C }`, the premise's own universals (`__up.<iri>`) are quantified in the premise only, never in the conclusion (GH #6882): `{ @forAll :x. :x :p :b } => C` fires only where the store proves `∀x. x :p :b`. The text engine binds a premise universal like a rule variable, then keeps a firing only if each one bound a universal of this run's store (a document-level `__ua.` one; inside a `log:conclusion` / `log:supports` run, that formula's own, never an enclosing formula's or the document's), distinct premise universals bound distinct store universals, and no other variable of the firing mentions that store universal at any depth (so `@forAll :z. :z :p :z.` does not prove `{ @forAll :x. :x :p ?y }`), nor binds a value holding a blank node (an existential scoped inside the universal, so `@forAll :z. :z :p _:b.` does not prove it either; refusing every blank is conservative). A ground fact proves nothing. Matching is sound, not complete: one store universal must carry the whole premise (`∀z. z :p :o` and `∀w. w :q :r`, stored apart, do not prove `{ @forAll :x. :x :p :o. :x :q :r }`). It is supported where the universal is the subject or object (or inside a list or triple term there) of a forward rule's stored-predicate atom, in a document with no backward rules. Anywhere else (a premise that also holds a blank constant, as a rule closed inside a formula can, a builtin operand, a quoted formula, a variable predicate, `rdf:first` / `rdf:rest`, a scoped or aggregated clause, a backward rule, an N3 query document), naive, compiled and incremental engines all return `N3: universally quantified antecedents are unsupported (@forAll in a rule premise or scoped body pattern)`. The `compiled-rules` engine compiles a supported rule as one that never fires (its store holds ground ids only and it refuses universal facts, so the text engine never fires it there either); `MaterializedN3Graph` runs it in fallback mode (the batch engine). One recursive check tells executable formulas from values: the premise, a containment pattern (`log:includes`, `log:notIncludes`, `log:supports`), the `log:collectAllIn` clause and both `log:forAllIn` clauses are executable, at any nesting depth (an aggregation inside another's clause included); a `collectAllIn` template, a scope and any other quoted formula term are values. A universal bound by an executable formula is rejected wherever it occurs below it; a value's own universals are allowed (a template is collected, and a formula quoted inside a pattern matches by identity). A clause or `log:includes` / `log:notIncludes` pattern reached through a variable is checked on its bound value, by the same walk, when the builtin is evaluated, and the run fails with the same error; the incremental graph rejects them before choosing counting or fallback execution. Quantified formulas used as containment subjects still hold opaque terms. The conclusion's own (`__uc.<iri>`) are not bound by the premise: a forward firing asserts them as document-level universals (`__ua.<iri>`; a conclusion triple left holding one at top level is not ground and is dropped, as any unbound variable is), and a backward rule matches goals through them. Every other formula-level universal belongs to its quoted formula: it matches only itself (an ordinary premise atom `:a :says { @forAll :x. :x :q :z }` matches that formula term, not `:a :says { :k :q :z }`), substitution never reaches it, and no rule variable can bind to it on its own (`{ ?s :q :z }` does not match `{ @forAll :x. :x :q :z }`; a `log:includes` pattern blank still does when the quantified scope is supplied as a formula value). `log:conclusion` / `log:supports` reason over a formula's statements with its own universals as that run's document-level ones, so a quoted rule under the formula's `@forAll` fires; universals a rule's conclusion asserts during that run are that run's too; the result formula names all of them as its own again. Two different IRIs with one local name (`@forAll a:x, b:x`) are two variables. A document parsed at run time (`log:parsedAsN3`, `log:semantics`) becomes a quoted formula, so its top-level `@forAll` binds in that formula: `"@forAll :x. :x :p :b." log:parsedAsN3 ?g` gives the same term as `{ @forAll :x. :x :p :b }` (not a document-level `__ua` universal), and a parsed quantified formula used as a clause is rejected like the inline one.

- **`reason_n3_pass_all` echoes rules, with two caveats.** `RuleVars::N3` output re-parses to the same rules, so re-running it is a FIXPOINT — *unless* a rule mints an existential (a blank node in its CONCLUSION), which gets a fresh `_:__sk…` label per firing, so such a document grows on every re-run (the same caveat EYE carries). `RuleVars::VarIris` (the `--pass-all-ground` form) replaces `?x` with `<http://www.w3.org/2000/10/swap/var#x>` throughout the echoed RULES — at every depth, quoted `{ … }` formulae included, since N3 quantifies `?x` in the outermost formula — but the rule is then made of CONSTANTS, so feeding that document back to the reasoner does **not** re-derive anything. It grounds rules, not data: a document that ASSERTS a formula-valued fact carrying a variable (`:a :p { ?x :q :b }.`) still echoes that `?x` in the closure half, so "no `?` anywhere" holds for rule documents, not for every input. Parity is by construction (closure + rules), not byte-verified against EYE's own writer: sparq emits full `<…>` IRIs with no `@prefix` reconstruction and sorts the closure statements. It is exact or it fails: each `@forAll` universal is declared once, on a document `@forAll` line before the first fact or rule using it (units ordered so plain mentions of the IRI come first), and the whole output is re-parsed and compared, universals by exact name; when a closure fact or rule has no lossless N3 form (a unit mixing a plain mention and the universal, a cycle of such units, a backward-chaining copy of a universal) the call returns `Err` instead of writing a document that would re-reason differently.

- **`why()` is a witness, not a proof set.** It returns the first derivation in deterministic order, or `None` if the triple isn't in the closure or `ExplainOpts` caps (default depth 128, 65 536 nodes) are exceeded — not an enumeration of all derivations.

- **Deletion semantics:** `delete` removes *base* (asserted) triples; a deleted base triple still derivable from the remainder stays in the closure, and deleting a derived-only fact is a no-op (standard materialized-view semantics).

## Migrating from eye-js (`@sparq-org/eyereasoner-compat`)

The npm package **`@sparq-org/eyereasoner-compat`** (`packages/eyereasoner-compat/`) is a

drop-in for [eye-js](https://github.com/eyereasoner/eye-js)'s `n3reasoner(data, query?, options?)`,

backed by this crate's wasm bundle (`crates/sparq-reason-wasm`) — no SWI-Prolog, a lighter

browser payload. It maps the eye-js surface onto three wasm entry points and is HONEST about the

boundary:

- **Output modes.** `derivations` (default, EYE `--pass-only-new`) → `Reasoner.reasonN3New`;

`deductive_closure` (`--pass`) → `Reasoner.reasonN3`; `none` → empty. The `…_plus_rules` modes

(`--pass-all` / `--pass-all-ground`) still **throw in the npm package**: the *reasoner* half

now exists — `reason_n3_pass_all(src, RuleVars::…)` emits the closure plus the echoed rules

(`sq-xqchl.2`) — but it is not yet exposed as a `sparq-reason-wasm` entry point, so the

package has nothing to call. Wiring the binding + the two `switch` arms is the remaining

step; until it lands the modes fail loudly rather than return a different result set.

- **Query filter.** `n3reasoner(data, query)` evaluates the EYE `--query` rule over the

materialised closure (`Reasoner.reasonN3Query` → `reason_n3_query`). The premise runs through

the reasoner's OWN matcher, so **builtins, `{ … }` formulae and `( … )` lists all work** in a

query rule (`sq-xqchl.1`); the earlier SPARQL-`CONSTRUCT` translation could evaluate none of

them and rejected them fail-closed.

- **Builtins.** Only this crate's `math:`/`string:`/`list:`/`time:`/`log:` subset is available

(EYE's full library is larger); an unsupported builtin simply does not fire.

- **SWIPL surface.** `SwiplEye` / `loadEyeImage` / `runQuery` / `EYE_PVM` / `linguareasoner` etc.

are re-exported as **throwing migration stubs**; `SWIPL` / `cb` options warn-and-ignore.

See `packages/eyereasoner-compat/README.md` for the CDN (esm.sh/jsdelivr/unpkg) usage and the

full output-mode + builtins-coverage tables.

## See also

- `noir-circuit-patterns`, `noir-optimisation`, `verifiable-credentials-zk`, `sparql-formal-semantics` — the single-prover ZK estate; the `explain` `ProofTree` is intentionally a flat, id-free, premises-before-conclusion DAG meant as a ZK-derivation witness.

- `mpc-protocols` — multi-party layer over (federated) SPARQL.

- `hdt-format`, `fused-decompress-parse`, `rust-parallel-parsing` — sibling ingest/storage skills for getting triples into the graph you then reason over.

- `research/owl2-el-ql-reasoning-spike.md` — the EL/QL feasibility spike: why EL first, the RL-incompleteness proof (the CR4 counterexample), and the phased plan (E1–E6) `sparq-reason-el` implements.

- `research/reasoner-suite-on-substrate.md` §2.5 — the QL track design: the PerfectRef applicability trap, the strict CQ-shape gate, and why the production path (tree-witness + UCQ-containment minimisation) is sequenced late by soundness risk (the phased plan `sparq-reason-ql` implements through phases Q1–Q3, and the sparq-extension conformance floors — the DL-Lite_R certain-answer floor `QL_DLLITE_FLOOR` and the sound-subset entailment-arm floor `QL_ENTAILMENT_FLOOR` — have both graduated, sq-qo1a9 / sq-pbz04.3.4).

- **N3 conformance — what is measured.** `sparq-inference-conformance` runs the w3c/N3 community-group manifests (reasoner / parser / extended / TurtleTests; results in `inference-conformance-report.md`). The community **notation3tests** suite (codeberg `phochste/notation3tests`, issue #6467) runs through `sparq-notation3tests` (`crates/sparq-conformance/src/notation3tests.rs`: cases are the `.n3` files under the checkout's `tests/`, scored by the suite's name-keyed expectation: `success-*` must derive `:result :has :<name>` or `:test :is true` (never `false`), negative `fail-*` must derive no verdict at all, `crash-*` input must be rejected (parse/reasoning error); buckets pass / nonconform / incomplete / crashed / timeout, plus unavailable for a `log:content`/`log:semantics` resource the offline runner cannot serve; one process per test, `--timeout`) in the ADVISORY weekly lane `.github/workflows/notation3tests.yml`. It has **no measured baseline yet** and no floor — do not cite an N3 pass rate from it until a run at a pinned suite SHA records one. Goal-directed `log:query` output is not implemented, so tests that only report through it fail.

- `crates/sparq-conformance/tests/ufo_sn3/` — **UFO-SN3**: a finite-world, function-free, range-restricted N3 projection of representative UFO (Unified Foundational Ontology) concepts — rigidity, identity criteria, relators, events/participation, dispositions, commitments/norms, situations/worlds/accessibility — run as committed vocab + rules + fixture cases through plain `reason_n3` (`tests/ufo_sn3_suite.rs`, `UFO_SN3_FLOOR`, an UNGATED sparq-EXTENSION row in the central scoreboard). Demonstrates the reification-node projection for statement-level (triple-term-shaped) claims, since the N3 `Term` model has no triple-term variant (a tracked gap).

The opt-in `substrate-compare` temporal ordering borrows exact integer-second

and fractional-digit keys from core. It preserves nanosecond and large-year ordering

without changing approximate epoch/vector caches; no additional materialization

rules are introduced. See [temporal scope](../zk-query-proofs/references/exact-temporals.md).