Explicit negatives and validation reports

gestaltdb.reasoning.validation checks a finite typed closure against an explicit ValidationSuite and returns bounded Violation records with exact supporting facts and constraint identities. Validation never infers, never merges, and never explodes: the input closure stands unchanged, and a report is evidence — not a classical inconsistency and not a shape-validation certificate beyond the implemented checks.

from gestaltdb.reasoning.terms import Literal
from gestaltdb.reasoning.typed import TypedFact
from gestaltdb.reasoning.validation import Denial, ValidationSuite, validate

facts = [TypedFact("type", ["mallory", "Cat"]), TypedFact("type", ["mallory", "Dog"])]
suite = ValidationSuite("type", disjoint=[("Cat", "Dog")])
report = validate(facts, suite)
assert not report.clean
assert report.violations[0].kind == "disjoint-members"
assert report.violations[0].sources == ("disjoint:Cat:Dog",)

What is checked

• Denied positives: an explicit Denial(predicate, values) contradicting an identical ground fact. Absence of a fact is not a denial; only stated denials participate, so open-world silence never becomes a conflict.

• Disjoint membership: two membership facts sharing an entity under disjoint classes. Membership reads the suite’s explicit membership predicate (callers validating ontology closures pass the same predicate the compiler emits); no vocabulary is assumed.

• Reflexive loops: P(x, x) facts on properties declared irreflexive.

• Functional conflicts: two facts sharing subject and predicate with different remaining values. The pair is reported with a note that equality is not inferred — equality-generating functionality belongs to RE-11.

max_violations bounds the report; hitting it sets truncated instead of failing, and deterministic canonical order makes repeat runs identical. cancel cooperates during indexed input processing and raises without a report; input is fully buffered and sorted before those periodic checks. It does not interrupt a blocking input iterator. max_violations limits report size, not input memory. Violations reference supporting TypedFact values and stable constraint identities (disjoint:A:B, functional:age), so every conflict traces to exact logical input facts and a structural scope entry. These source strings are generated constraint labels, not caller-supplied axiom IDs or exact historical claim-version references.

What is not claimed

Domain and range axioms keep their entailment meaning in the compiler; they do not validate required fields, and validation never emits facts. Unsatisfiable classes (find_unsatisfiable) are a static schema check over subclass edges and disjointness pairs — no instance data is read, and anonymous constructions are out of scope. Full SHACL-style shapes, satisfiability beyond disjointness closure, probabilistic combination and classical explosion are explicitly deferred; the report vocabulary stays within the four implemented checks and fails closed on anything else. Ground Denial values are validation inputs, not polarity-aware rule premises: missing positive evidence cannot satisfy a denied premise. Generic rules support positive atoms and explicitly scoped absence, not signed-denial premises. Datatype shape/constraint checking is not provided by this suite; strict Literal construction is a separate contract.

Measured cost

The original small-workload measurement was about 70ms warm for 20,000 typed facts with 100 planted disjointness conflicts (single process). It is not a general complexity or release-performance guarantee: validation buffers the closure, sorts/deduplicates it, and some checks rescan it per constraint or conflict. See #200 (D6) for the indexing/cancellation follow-up; callers must bound their input independently.