inference

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):

[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):

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):

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 'SELECT ...' --reason rdfs  # reason then query

Key APIs

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

// 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
pub fn reason_n3_terms(src: &str, base: Option<&str>) -> Result<N3Closure, String>; // term-level, no Dict
pub fn reason_n3_terms_with_resolver(src, base, resolver: Option<&Resolver>) -> Result<N3Closure, String>;
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 the non-monotonic ops (store-scoped log:notIncludes, log:collectAllIn/forAllIn);
    // per-stratum blank scope. Fields: facts (final interned closure), strata_facts (sizes).

// 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 insert(&mut self, facts: &[[Term;3]]) -> usize;     // ground facts only
    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 rule: String, pub premises: Vec<u32> }
pub struct ExplainOpts { pub max_depth: usize, pub max_nodes: usize } // why_with(.., opts)

Id / Dict come from sparq_core::dict; Term, Rule, N3Closure, ProofStep, Resolver from sparq_reason::n3 (re-exported at the crate root).

// `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) -> Vec<[Id;3]>;
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; }
impl BoundRuleSet<'_> { pub fn eval(&self, dict: &mut Dict, facts: &[[Id;3]]) -> Vec<[Id;3]>; }

Compiled-rules scope is EXACTLY the WAC/ACP/ODRL-spike corpus subset (scoped log:notIncludes over stratum-complete predicates, log:uri, log:(not)equalTo, string: concatenation / encodeForUri / scrape / notGreaterThan); 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.

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 validates 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).

# #[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 are REJECTED fail-closed — validate() returns RifError::DistinctGroundEqual { left, right } (including a distinct ground created by substitution, e.g. ?x=<a>, ?y=<b>, ?x=?y). Value-space equality (e.g. "1"^^xsd:integer = "1.0"^^xsd:decimal) needs the substrate value-space comparator (Num::cmp_relational, sq-v5evr / #1646 — now merged), which the RIF Equal-atom path has not yet adopted; until that wiring lands the front-end refuses rather than answering incorrectly. 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 (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. 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).

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()
}

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. 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.

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). Batch-only: MaterializedOwlGraph's Fallback re-materialization always runs the full bridge.

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).

// Cargo.toml:  sparq-reason-el = "0.1"     // a SEPARATE crate; 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)

• 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). 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.
• 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 ClassAssertions, 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). Fail-closed: data-property assertions (the cdomain point-range rescue is a sequenced follow-up bead) 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).
• 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 (data positives are not internalized: an honest incompleteness, never an unsound missed clash). 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.
• 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). 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.
• Use EL, not --reason owl, when you need a complete class hierarchy over an EL ontology. RL is not an approximation you can tune up with more rules — EL needs a different algorithm.

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.

// Cargo.toml:  sparq-reason-ql = { version = "0.1", features = ["experimental"] }
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); 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. owl:complementOf; 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.

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 [GPT-5.6]): 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 (consistency wholly deferred to sq-pbz04.3.4 — always abstains), 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. 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. [OPUS-4.8] 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):

Branch	Decides Consistent	Decides Inconsistent	Abstains (UnknownReason)
RL (in-RL; PR1 preconditions pass; no divergence-guarded construct)	Yes (past divergence guard)	Yes (PR1-checked)	RlPr1Preconditions, RlDivergenceGuard
EL (in-EL; ⊤-free TBox; no ABox; no skipped/unapplied axioms)	Yes (empty-interpretation model construction)	Never	ElSkippedAxioms, ElUnappliedAxioms, ElTopGuard
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)
ALCH (all else the L1 extractor accepted)	Yes (complete for L1 fragment)	Yes (complete for L1 fragment)	ResourceBudget

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.

Common recipes

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

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; outside the compiled-rules subset and the incremental counting profile — both fall back to the text engine).

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):

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.

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

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.

// 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],"rule":..,"premises":[..]}]}
}

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 (otherwise those builtins simply don't fire):

use sparq_reason::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