Ontology v1 implementation contract

Development status

This is the ONTO-01 interface agreement for epic #131. The immutable reasoning contracts, standalone Datalog evaluator, ontology compiler, bounded witness explanations and pinned claims adapter shipped on main in 0.13.0rc1. See EPIC_REASONING_ENGINE.md in the repository for roadmap priorities and planning/reasoning-engine/release-readiness.md for release evidence.

Separation of concerns

gestaltdb.reasoning.model and gestaltdb.reasoning.protocols use only the standard library. Future core and ontology implementation must not import GraphDB, storage, serializers, Cypher, sampling or temporal version records. Adapters translate into these values, never the reverse. The existing package initializer still eagerly imports other subsystems; standalone architecture does not mean separate installation or a minimal top-level import footprint.

Fact(subject, predicate, object) contains three nonempty UTF-8 strings. There are no literals, blank-node generation, confidence weights or implicit IRI normalization. Local strings are opaque identifiers. Imported IRIs, if supported later, must preserve full identity. Variable(name) is the only variable form; '?x' remains a constant string, including in predicates.

Atom has a constant predicate and string/variable endpoint terms. A Rule has a nonempty ordered body and one head; all head variables must occur in the body. Ground heads are allowed. Program rejects duplicate rule IDs and sorts its catalog by ID. Its versioned structural digest includes rule IDs, variable names and body order: it is not a logical-equivalence digest or ontology revision. Nested collections are copied into immutable tuples.

DatalogEngine implements Evaluator.evaluate(program, facts, *, limits, collect_proofs=False). Inputs are Fact or Evidence values in an iterable, consumed under an input bound, not eagerly exhausted. Duplicate evidence does not multiply logical facts. EvaluationResult represents complete closure including input facts, with distinct facts in canonical subject/predicate/object order. Optional proof data does not introduce persistence coupling.

Ontology compilation

The profile is named gestalt-core-v1. Class membership is encoded as Fact(entity, 'http://www.w3.org/1999/02/22-rdf-syntax-ns#type', class_id). The ontology compiler reserves that predicate for membership; object-property axioms using it are rejected. The general Datalog kernel has no reserved terms. Adapters must apply an explicit mapping; native labels and relationship types are not automatically interpreted as ontology identifiers.

Let T(x, C) denote membership and P(x, y) an object-property assertion. The supported compilation templates are:

• SubClassOf(C, D): T(x, C) -> T(x, D).

• SubPropertyOf(P, Q): P(x, y) -> Q(x, y).

• Named class/property equivalence: the two corresponding implications.

• Domain(P, C): P(x, y) -> T(x, C).

• Range(P, C): P(x, y) -> T(y, C).

• InverseOf(P, Q): P(x, y) -> Q(y, x) and the converse.

• Symmetric(P): P(x, y) -> P(y, x).

• Transitive(P): P(x, y) AND P(y, z) -> P(x, z).

• PropertyChain(Q, R, P): Q(x, y) AND R(y, z) -> P(x, z).

• IntersectionSubClassOf((C1, C2), D): T(x, C1) AND T(x, C2) -> T(x, D).

• UnionSubClassOf((C1, C2), D): T(x, C1) -> T(x, D) and T(x, C2) -> T(x, D).

• Reflexive(P, C): T(x, C) -> P(x, x).

Multiple inheritance and cycles are legal and terminate under set semantics. Named equivalence does not merge individuals. Multiple domain or range axioms infer every stated class, not a union choice. Stable axiom identities and compiler rule origins are available in ONTO-03; immutable revision identity is separate from the kernel’s program digest. Hierarchy schema facts themselves are not automatically included in instance closure; future schema lookups must state their semantics.

Unsupported axiom shapes must fail before evaluation. Disjointness, equality, functionality, cardinality, datatypes, negation and existential generation are deferred, as are union superclasses and unscoped reflexivity. There is no claim of complete RDFS/OWL-RL/OWL-EL/OWL-DL support. Domain and range infer types; they do not validate required fields. Conflicts never entail arbitrary facts, and missing is not false.

Limits, proofs and failure

ReasoningLimits requires positive integers (not booleans):

• max_input_facts: yielded input values, including duplicates. Consume at most the limit plus one value to detect overflow. Reject values other than Fact or Evidence explicitly. Evidence entries count separately, even for the same fact.

• max_rules: input program size, checked before evaluation.

• max_iterations: executed delta rounds. Zero rounds are allowed for inputs requiring no rule evaluation; exceeding the bound fails, not truncates.

• max_candidate_rows: cumulative attempted candidate fact/partial-binding joins, including failed unifications, across all rounds. Check while joining, not after allocating an unbounded intermediate result.

• max_facts: distinct asserted plus derived closure facts.

• max_proof_nodes: stored fact-witness records. Truncate proofs explicitly if necessary without claiming incomplete logical closure.

• max_proof_edges: stored ordered premise occurrences plus input-reference occurrences. This additional bound prevents one long rule body from exceeding the proof-storage budget even when the node count is small.

Inference-counter exhaustion raises ReasoningLimitError. No partial successful closure is returned and no publication occurs. Malformed input raises ReasoningError. Limits are deterministic work/storage counters, not an exact wall-clock or process-memory sandbox; arbitrary input iterators can themselves perform unbounded work. Compilation and construction of already-materialized program values are outside evaluator resource accounting.

Proofs must be shared finite DAGs linking facts, rules, axiom revisions and input evidence. A bounded witness is not a complete support index for deletion; no incremental maintenance guarantee is made in v1. Logical facts are deduplicated independently of multiple evidence references.

Adapter lifecycle and temporal semantics

FactSource exposes one immutable InputContext and an evidence iterator. The adapter preserves a caller-provided pinned view during its own iteration lifetime; it does not create or close the caller’s graph/view. Iteration must not repin or mix contexts. Each Evidence carries a ground fact and opaque immutable reference ID. Many references may support one fact. The source adapter and consumer must bound evidence consumption before collecting it in memory.

InputContext identifies the input context, world, ontology revision, source policy and mapping. These identifiers do not authenticate themselves; the adapter must verify the underlying read provenance and reject incompatible snapshots. A context identity must include its selected valid-time point and pinned system visibility. The engine receives plain facts; it cannot establish that the caller has honestly selected a compatible world or source policy.

The claims adapter is read-only, selecting positive entity-object claims at one valid-time point in one world under a pinned visible commit prefix. Agent/source selection is explicit and part of policy identity. Recognized engine-produced claims are excluded by default to avoid treating derived output as independent evidence. Opting into derived inputs must be deliberate and recorded in policy. Explicit negative claims do not participate, but do not suppress positive support for the same proposition. Confidence does not alter Boolean inference.

Results must remain tied to their context and ontology revision. They are not validity intervals and are never automatically written as claims or current graph records. Combining snapshots, worlds or temporal/current data planes requires a separate explicit adapter policy. Publication, deletion maintenance and historical interval inference are post-v1 work.

Standalone evaluator (ONTO-02)

The evaluator is stateless across calls and has no database, filesystem, clock, ontology-catalog or evidence-source access. A minimal executable example:

from gestaltdb.reasoning.engine import DatalogEngine
from gestaltdb.reasoning.model import (
    Atom, Fact, Program, ReasoningLimits, Rule, Variable,
)

x, y = Variable("x"), Variable("y")
program = Program([
    Rule("parent-is-ancestor", [Atom(x, "parent", y)], Atom(x, "ancestor", y)),
])
result = DatalogEngine().evaluate(
    program,
    [Fact("alice", "parent", "bob")],
    limits=ReasoningLimits(),
)
assert Fact("alice", "ancestor", "bob") in result.facts
assert result.program_digest == program.digest

Evaluation uses synchronous semi-naive rounds: every join variant anchors one body atom in the previous round’s delta; other atoms use the current full closure. Every distinct body atom is a possible anchor. Identical repeated atoms need only one anchor, but retain their body positions. Facts from a round are added together after all its variants finish, so catalog order does not change round semantics. Variants can revisit the same logical binding; conclusion set semantics remove duplicates, and all attempted candidate joins still count toward the work bound.

Predicate, predicate/subject and predicate/object indexes restrict candidates. Fully bound atoms use exact membership. After the delta anchor, remaining atoms are selected by the smallest indexed bucket, with original body order breaking ties. Traversal is iterative depth-first; no unbounded intermediate join table or recursive Python call chain is constructed. Index bucket order is deterministic for a fixed logical input, independent of input ordering or hash seed.

One iteration means an executed delta round with at least one scheduled rule variant. An exhausted input, empty program or delta with no relevant variants requires no further round. A recursive final round that produces no new facts still counts. Proof data is collected only when collect_proofs=True; proof budgets never change this closure or iteration semantics.

Input iterators and constructing already-materialized program/limit values remain caller responsibilities. Exceptions raised by an input iterator propagate; invalid yielded values raise ReasoningError. Limit failures do not change the program or input collections and do not affect subsequent calls on the same engine.

Immutable ontology compilation (ONTO-03)

Import Ontology and the nine supported axiom classes from gestaltdb.ontology.model. Import compile_ontology from gestaltdb.ontology.compiler. Compilation does not invoke an evaluator, access a database, install rules or merge entity identities.

from gestaltdb.ontology.compiler import compile_ontology
from gestaltdb.ontology.model import Domain, Ontology, SubClassOf, TYPE_PREDICATE
from gestaltdb.reasoning.engine import DatalogEngine
from gestaltdb.reasoning.model import Fact, ReasoningLimits

ontology = Ontology("organization", [
    Domain("worksFor", "Researcher"),
    SubClassOf("Researcher", "Person"),
])
compiled = compile_ontology(ontology)
result = DatalogEngine().evaluate(
    compiled.program,
    [Fact("alice", "worksFor", "acme")],
    limits=ReasoningLimits(),
)
assert Fact("alice", TYPE_PREDICATE, "Person") in result.facts
assert compiled.revision_id == ontology.revision_id

Ontology copies an explicit list/tuple of axioms, rejects unknown shapes (including unimplemented subclasses), removes duplicate axioms and sorts them canonically. Equivalence/inverse pairs normalize their endpoint order because those axiom forms are symmetric. Identifiers otherwise retain their exact string identity, including strings beginning with ?; the compiler uses typed variables internally, so such identifiers cannot become variables.

Each axiom has a versioned SHA-256 content identity. The ontology revision digest also includes the ontology ID and profile. Reordering or repeating axioms does not change identity; changing ontology ID does change revision identity. Logically equivalent but structurally different axiom sets need not have equal revision IDs. These identities are content addresses, not persisted catalog versions or signed provenance. There is no implicit system time, valid time or network import.

CompiledOntology retains the immutable source ontology, its executable program and a canonical origins tuple. Every generated rule has exactly one RuleOrigin(rule_id, axiom_id), and every source axiom is represented. The source ontology’s revision scopes that table; callers can resolve exact axiom values without a storage lookup. Bidirectional axioms have separate forward and reverse rule IDs, including reflexive cases, so provenance is not erased by a logical simplification. Compilation currently emits templates directly rather than materializing hierarchy closure or collapsing strongly connected components. Cycles terminate through the evaluator’s set semantics and resource bounds.

Result lookups and witness explanations (ONTO-04)

fact in result performs binary-search membership without a second full fact index. result.match(subject=..., predicate=..., object=...) returns immutable canonical matches. A subject filter narrows the scan using binary-search bounds; predicate/object-only lookups scan the result and are not index-backed.

Proof collection is disabled by default. Enable it explicitly; proof budgets apply only to stored witnesses, independently of inference counters. Exceeding an inference bound still raises and returns no partial successful result.

from gestaltdb.ontology.compiler import compile_ontology
from gestaltdb.ontology.model import Domain, Ontology, SubClassOf, TYPE_PREDICATE
from gestaltdb.reasoning.engine import DatalogEngine
from gestaltdb.reasoning.model import Fact, ReasoningLimits
from gestaltdb.reasoning.protocols import Evidence

ontology = Ontology("organization", [
    Domain("worksFor", "Researcher"),
    SubClassOf("Researcher", "Person"),
])
compiled = compile_ontology(ontology)
result = DatalogEngine().evaluate(
    compiled.program,
    [Evidence(Fact("alice", "worksFor", "acme"), "claim-version:1")],
    limits=ReasoningLimits(max_proof_nodes=100, max_proof_edges=200),
    collect_proofs=True,
)
root = Fact("alice", TYPE_PREDICATE, "Person")
explanation = result.explain(root, max_nodes=10)
assert root in result
assert result.match(subject="alice", predicate=TYPE_PREDICATE)
assert not explanation.truncated
assert len(explanation.nodes) == 3
origins = {origin.rule_id: origin.axiom_id for origin in compiled.origins}
axioms = {axiom.axiom_id: axiom for axiom in compiled.ontology.axioms}
used_axioms = {
    axioms[origins[node.rule.rule_id]]
    for node in explanation.nodes if node.rule is not None
}
assert used_axioms == set(ontology.axioms)

The core never imports the ontology layer. A caller resolves witness rule IDs through its compiled ontology’s origin table and retains that source revision. Named input evidence is an opaque caller-supplied reference, not an authenticated claim version; source validation and snapshot context belong to ONTO-05.

FactWitness stores a fact and either an asserted-input witness or its exact Rule and ordered premises. Premises retain original body positions even if join planning reorders evaluation or a body repeats an atom. Only the first deterministically discovered derivation is kept for a new fact. Asserted facts are never replaced by cyclic derived support. Synchronous rounds guarantee that a derived witness depends on earlier-round facts, producing a finite DAG.

For a named input fact, one lexicographically smallest supplied evidence reference is retained, independent of stream order. Alternative sources and derivations are intentionally not enumerated; omitting alternatives does not set truncated. This is a witness policy, never an all-supports index or deletion-maintenance API. An ordinary Fact input can have an input witness without any external reference.

ProofTrace retains its immutable program and canonical, topologically ordered witness nodes, breaking ties by fact order. Constructors validate rule membership, ground rule applications, unique facts and acyclicity. Rule values are shared with the existing program, not copied per derivation. Source/reference strings do not create any database access. The trace is bounded by both witness-node count and premise/reference count; these remain counters, not a byte-accurate RSS bound.

Input witness selection uses a bounded streaming pool of the smallest facts. If input facts fill the node budget, no derived witnesses may fit; increase the budget or accept explicit truncation. When edge space runs out, named evidence may be omitted and a derived witness may be absent entirely. Later stored witnesses may refer to absent earlier witnesses, with explicit truncation. Logical closure remains complete regardless of these proof omissions.

result.proofs.truncated conservatively reports any storage omission and is propagated to every explanation, even if a particular leaf was fully retained. result.explain(fact, max_nodes=...) also bounds the reachable subgraph’s fact-witness records using an iterative, deduplicated traversal. Query truncation does not change the stored trace. A known fact with no stored witness yields an empty, truncated explanation; a fact outside the closure raises KeyError. Explaining a known fact when collection was disabled raises ReasoningError. The lower-level trace alone does not establish that an unstored fact is entailed; use the result wrapper for that distinction.

Pinned temporal claims (ONTO-05)

Import PinnedClaimSource, ClaimSelection, ClaimMapping and ClaimSourceLimits from gestaltdb.reasoning.adapters.claims. Only this adapter layer depends on GraphDB and temporal/provenance records; the standalone core and ontology compiler never import it.

The caller first obtains a temporal GraphReadView through the existing graph.read_view(valid_time=..., system_time=...) context manager. Database creation/opening and any identity initialization happen outside extraction. The adapter requires an already initialized, verifiable source, and does not initialize identity, rebuild stale indexes or write any records or claims.

For example, this helper accepts an existing view and a compiled ontology:

from gestaltdb.reasoning.adapters.claims import (
    ClaimMapping, ClaimSelection, ClaimSourceLimits, PinnedClaimSource,
)
from gestaltdb.reasoning.model import ReasoningLimits

def reason_over_claims(view, compiled, *, world):
    with PinnedClaimSource(
        view,
        world=world,
        ontology_revision=compiled.revision_id,
        selection=ClaimSelection(),  # Explicitly all agents and sources.
        mapping=ClaimMapping(),      # Preserve all claim predicates.
        limits=ClaimSourceLimits(max_scanned_claims=10_000),
    ) as source:
        return source.evaluate(
            compiled, limits=ReasoningLimits(), collect_proofs=True,
        )

ClaimSelection normalizes explicit agent/source collections into immutable canonical tuples. None means all, an empty collection means none, and sources=(None,) means only claims with no source. These distinct policies have distinct fingerprints. include_derived=False excludes recognized gestaltdb:rules / gestaltdb.rules and gestaltdb:ontology / gestaltdb.ontology agent/derivation-marker pairs. Opt-in is explicit and changes policy/context identity. These metadata conventions do not authenticate the original asserting agent or defend against untrusted Python implementations.

Only positive entity-object claims participate, in exactly one selected world at the view’s valid-time point and commit prefix. A negative assertion does not suppress independent positive support. Confidence is not propagated. Half-open validity, corrections and retractions use existing claim/as-of semantics. The adapter yields exact canonical historical version IDs as evidence; multiple versions/sources for one proposition do not multiply logical facts. The core’s single-witness policy still retains at most one canonical evidence reference.

ClaimMapping(predicate_aliases=((source, target), ...)) maps predicates only. The empty mapping preserves identifiers exactly; no native node label, edge type, IS_A predicate or other local spelling is implicitly assigned ontology meaning. For a local membership predicate, explicitly map it to TYPE_PREDICATE. Unmapped predicates, subjects and objects remain unchanged. Duplicate alias sources are rejected, even if their targets agree. Mapping identity records this preserve-unmapped policy and canonical aliases.

PinnedClaimSource.context fingerprints verified source provenance, world, ontology revision, source policy and mapping. The adapter captures a validated provenance copy and fixed point, never silently advancing to new commits. Later appends/corrections may change the live graph but not this view. Mutating or rebinding the original view’s graph, provenance or default time is rejected. Private read-view/identity accesses are confined to this adapter boundary.

Verification checks persisted identity as well as the handle’s cached identity, backend/serializer identity and the selected commit-visibility digest. It runs before and after iteration and after inference. Cheap per-item checks catch view rebinding while consuming records. This detects inconsistency with a source view; tokens/content digests are not cryptographic attestations of caller-supplied data.

max_scanned_claims counts candidates yielded by the underlying positive, entity-object, selected-world query, before agent/source/derived filtering. It detects overflow after at most the limit plus one candidate, even when none pass policy. ReasoningLimits.max_input_facts separately bounds yielded evidence consumed by the engine, including duplicate logical facts. Backend-internal index scans/candidate-ID materialization and commit-prefix verification are outside these counters. Neither counter promises a total query-time or RSS ceiling.

Use source.evaluate(compiled, ...) for a complete result verified after inference. A direct, partially consumed iter_evidence() stream is not an atomic authenticated batch and does not itself bind an arbitrary external engine result to context. Do not manually concatenate streams from incompatible contexts.

ClaimReasoningResult retains immutable input context, provenance, compiled ontology, policy/mapping and the core result. It checks their revision, policy, mapping and program consistency; even two ontology IDs with identical generated programs remain distinct contexts. facts, membership, match and explain delegate to the core result. verify_source(graph) can recheck the original source identity/prefix later; it does not rerun inference or authenticate a manually constructed result. Results remain usable after the source is closed, have no database handle, and make no interval-validity or materialization guarantee.

Closing the source invalidates its outstanding and future iteration/evaluation without closing the borrowed graph/view. Keep the caller’s graph open for the duration of extraction/evaluation. Stale temporal indexes fail closed and require an explicit caller-managed rebuild outside this read-only workflow.

Conformance and isolation gates (ONTO-06)

The conformance suite is tests/test_ontology_conformance.py. It combines focused hierarchy/property fixtures and twelve deterministic generated schemas. Every case is checked against a finite grounding oracle that enumerates safe substitutions independently of the indexed evaluator. It also checks proof origins, input-order invariance, positive monotonicity and stateless recomputation after removing all independent support from a cycle.

Optional differential tests use RDFLib/OWL-RL as an independent ontology oracle. The fixtures encode the nine supported axiom forms as standard RDF/OWL triples, with separate individual, class and property vocabularies. Comparison projects onto named-individual property assertions and memberships in the fixture’s named classes. Extra vocabulary/schema, datatype and sameAs consequences are outside that projection. There are no negative claims, equality-inducing axioms or inconsistent ontologies in these oracle fixtures: the oracle is not a validator for GestaltDB’s temporal or conflict-tolerant semantics.

This is selected-fragment differential testing, not a complete W3C conformance suite or a claim to implement OWL-RL. The independently grounded kernel tests, single-axiom/mixed compiler tests and temporal adapter isolation/failure tests remain required even when the optional oracle is absent.

Run the oracle gate explicitly (versions used for this slice):

uv run --with "owlrl==7.6.2" --with "rdflib==7.6.0" pytest tests/test_ontology_conformance.py -q

Without those packages, only the twenty oracle comparisons skip; the reference, architecture and isolated execution checks still run. Do not count oracle skips as an executed differential gate. These packages are test-only and are not added to runtime requirements. Run the whole suite with the same --with options to exercise the gate alongside regressions; add installed backend extras as needed.

.github/workflows/ontology.yml runs these feature/reference/oracle gates on Python 3.10-3.13 for relevant PRs and pushes to onto-dev and main. It installs the optional oracle and LMDB/LevelDB explicitly, so an absent oracle cannot silently turn the differential gate into skips. The existing general test workflow targets main; this dedicated workflow also covers epic integration before that release. The optional PyRex cases may still skip when that backend is not installed.

Static import checks inspect every reasoning-core and ontology module, excluding the explicit adapter subtree. They require standard-library or inward relative imports and reject dynamic import hooks. An isolated python -I -S subprocess loads the whole compile/evaluate/explain pipeline without site packages, storage, the GestaltDB initializer or the adapter layer. This proves implementation-layer independence, not separate packaging or removal of the existing eager root imports.