Crate nibli_reason 

nibli-reason (logic/reasoning) engine: FOL assertion and query via demand-driven backward-chaining.

This is the core inference component of Nibli. It maintains a stateful knowledge base with a fact index and backward-chaining rule engine:

• Fact assertion — Ground predicates stored as typed StoredFact via pluggable FactStore backend. Universal quantifiers compile to UniversalRuleRecord templates for backward-chaining.
• Entailment queries — Recursive formula checking via [check_formula_holds] with demand-driven backward-chaining through universal rules.
• Proof traces — [check_formula_holds_recording] builds a proof tree recording which rule/axiom was applied at each step (19 proof rule variants). Multi-hop derivation provenance traces derived facts through universal rule chains via backward-chaining.
• Witness extraction — [find_witnesses] returns all satisfying entity bindings for existential variables.
• Compute dispatch — ComputeNode predicates are forwarded to the host-provided compute-backend WIT interface for external evaluation.

The knowledge base uses RefCell (not Mutex) — single-threaded WASI. All mutable state — facts, rules, the predicate-result cache, the compute dispatch, and the cancel flag — lives PER-INSTANCE on KnowledgeBaseInner; there are no global or thread-local statics, so distinct KBs (e.g. one per request on the multithreaded server) never interfere.

Re-exports

pub use kb::KnowledgeBase;

Modules

fact_store

Fact store abstraction (trait + in-memory implementation). Fact store abstraction for the reasoning engine.

kb

Structs

ComputeRequest

Batch compute request.

StratumEdge

One outgoing dependency edge in a StratumRow.

StratumRow

One predicate’s row in KnowledgeBase::stratification_report.

Enums

Ineligible

Why a relation was NOT admitted for materialisation. Surfaced by KnowledgeBase::materialization_report — without it a knowledge base cannot tell whether it actually got the lookup, only that its query is still slow.

Functions

default_compute_predicates

The built-in arithmetic predicates marked as ComputeNode by default — product (×), sum (+), quotient (÷). The shared default for every embedder (nibli-engine, nibli-pipeline, nibli-wasm), paired with transform_compute_nodes.

transform_compute_nodes

Transform registered compute predicates from Predicate → ComputeNode in a logic buffer. Call this after nibli-semantics compilation and before asserting/querying.