What Nibli guarantees

Derived from the engine README and GUARANTEES.md. The full contract text lives in those files; this page is a short operator summary.

One surface language

Nibli has one front-end language: nibli KR (predicate-call surface: dog(Adam)., animal(every dog).). Name resolution is fail-closed: an unknown word is a compile error, never an arity-guessed new predicate. Normative spec: NIBLI_KR.md.

Soundness (relative to what you asserted)

The engine never returns TRUE for a formula that does not follow from the asserted facts and compiled rules plus any proof-local compute checks evaluated for that query, given a correct implementation and correct trusted backend replies. A TRUE answer comes with a formal proof trace. Bugs would be deterministic and testable — not stochastic fabrication.

This is not omniscience: change the premises and the verdict can change.

Proof sources are explicit. A stored tuple is not automatically called a user assertion: Asserted names every active fact id and label, Derived cites the rule assertion and grounded premises even for eagerly forward-chained facts, and legacy existential-import evidence is Presupposed. Duplicate assertions remain separately citable; retraction and reopen reconstruct citations from the same authoritative assertion registry. Equality substitution cites the real stored equality path it used.

Ordinary-predicate temporal rule literals are flavor-exact. Bare rules are unqualified and do not silently lift into past, now, or future; authors declare same- or cross-flavor mappings explicitly. Negation-as-failure follows the same rule: bare ~P checks bare P, while past ~P checks only for a Past witness. Stratification remains conservatively keyed by surface relation, so temporal flavors cannot be used to evade a negative-cycle rejection. Identity and query-time compute built-ins retain their separately documented semantics. One formula path may carry one temporal prefix or one deontic prefix, never both. must past P and past must P are compile errors rather than formulas whose outer wrapper could be lost in the one-flavor fact/rule store. The same fail-closed rule applies to manually nested raw IR before assertion or query. It is path-scoped, so separate rule literals may use different flavors, as in an explicitly declared past P -> must Q mapping.

Closed world and closed domain

Inference assumes:

• Closed world — a fact you did not assert is taken to be false, not unknown.
• Closed domain — quantifiers range only over entities the knowledge base knows.

The default clean-core profile does not infer existence from a universal: animal(every dog). alone makes no dog, and some dog remains plain ∃. Legacy xorlo import is an explicit opt-in (NIBLI_EXISTENTIAL_IMPORT=1 or :existential-import on). When enabled, the imported witness is a full logical entity: it participates consistently in ∃/∀/find/count/aggregate. Find and proof metadata label it existential-import, count proofs disclose the imported share, and the host/UI show which profile is active. Toggling the profile rebuilds the current KB transactionally, so existing rules change immediately.

Ordinary reasoner-minted witnesses are labeled generated-witness; asserted user constants remain knowledge-base, even when their display text resembles sk_N. Internally, generated witnesses have source-scoped typed identities (source assertion, binder ordinal, sort, and origin). Their friendly sk_N or sk_N(argument) rendering is never semantic, so equal-looking user constants stay distinct through equality, event joins, find/count, proof, persistence, retraction, and rebuild. A compute call that would expose an internal witness to the string-only backend protocol fails closed as UNKNOWN (backend-unavailable); an equal-looking user constant still dispatches normally.

Exact counts are observations, not constraints

exactly N and no are query-only formulas over the current closed domain. They count identity-equivalence classes and disclose any legacy existential-import contribution in the proof. Assertion ingress rejects them before allocating a fact id: Nibli does not persist or enforce cardinality constraints, and exactly 0 is never a stored prohibition. Assert ordinary facts, then re-query after additions, equality changes, or retractions. Counts inside opaque fact { … } or event { … } content remain quoted content and do not constrain the outer KB.

Four-valued outcomes

How to read a query result (product README wording):

All four are QueryResult variants in the engine itself, not host conventions — RESOURCE_EXCEEDED carries which limit was hit. Raise them with the NIBLI_FUEL / NIBLI_MEMORY_MB env vars or the :fuel / :memory REPL commands; see GUARANTEES.md.

Witness enumeration has a separate complete-or-error contract. Native query_find/count_witnesses, and WIT query-find-text, return a reasoning error if any evaluated candidate leaf is UNKNOWN or RESOURCE_EXCEEDED; they do not turn an undecided membership into an empty row set or partial count. This includes non-finite arithmetic and negated non-definitive leaves, even if another OR branch is true. Definitive TRUE/FALSE enumeration is unchanged. Native aggregate inherits the same refusal before numeric projection, and the projection itself fails closed: a binding set that does not bind the variable, a non-numeric value, a non-finite operand, and a non-finite (overflowed) result each refuse with a distinct error instead of silently dropping rows. A complete empty enumeration is the typed AggregateOutcome::Empty; a valid aggregate carries its contributing-witness count as provenance (AggregateOutcome::Value { value, witnesses }). Exact-count formulas use their separate domain-based CountNode evaluator and are not changed by this collection rule, including the disclosed NaN-only domain boundary.

Trusted proof-local compute

Results from the external compute backend (exponential, logarithm, or another registered corpus relation) are trusted evidence for the current ComputeCheck, not stored premises. Registration is post-compile routing: it accepts an existing corpus spelling or canonical relation, normalizes aliases/committed compounds to the canonical IR name, and declares neither vocabulary nor arity. An unknown registration is refused and remains a text compile error. Native raw-IR callers may instead query an arbitrary explicit ComputeNode without registration; that remains query-only. The shipping component has no raw-buffer query or vocabulary/schema method, so a custom host backend cannot add an arbitrary text predicate by itself.

Built-in arithmetic (product / sum / quotient) follows the same proof-local lifecycle: no compute result enters the fact store or registry, receives an id, changes the domain, survives replay, or triggers forward chaining. Compute atoms are query-only; assertions and rules containing executable compute are rejected before an id is allocated, while quoted abstraction content remains opaque. The reference names exponential/logarithm are query-only as assertions even before registration, and registering a corpus relation while live stored facts or rules reference its canonical name is refused with the blocking ids named — registration order cannot strand a stored fact. The numeric comparisons (greater / less / num_equal) are query-only on the same terms whenever an operand could be a number: they decide a verdict and filter witnesses, but a rule may not carry one, so there is no numeric threshold rule. That is a decision rather than a gap — a comparison in a rule would be looked up in a store that never holds one, which is inert as a positive guard and, under ~, succeeds for every binding. A comparison between two named things (greater(Alis, Bob), “taller than”) is an ordinary relational fact and asserts normally. Each top-level query recomputes or redispatches; repeated identical external checks may share a transient within-query memo only to keep the verdict and proof consistent. A backend error is always UNKNOWN (backend-unavailable), even after an earlier successful query or when an ordinary fact has the same tuple. Any conclusion that uses a successful external check is only as sound as that oracle.

The stock external-compute path is deliberately low-assurance: plaintext, unauthenticated JSON Lines over TCP, with no identity, integrity, request binding, version, freshness/replay, revocation, or audit receipt. Any parseable Boolean received in stream order is trusted, so a valid forged, replayed, stale, or mismatched reply is not detectable. Stronger admission belongs in a custom native dispatcher, custom component host, or external secured transport; the stock :backend setting only selects an address. See WASM, host & compute.

Where the full story lives

• GUARANTEES.md — differential oracles (Vampire / clingo), Lean proofs, determinism, mutation baseline.
• LOGIC_IR.md — the FOL intermediate form the reasoner consumes.
• CI: just ci, just verify-soundness, just verify-proofs.