Logic Conformance

• Slice: logic
• Source: slices/core/logic/design/LOGIC-CONFORMANCE.md

GMEOW Logic — Conformance Corpus and Preservation Contract

Status: implementation contract for logic:. This is the conformance member of the GMEOW Logic document set, and the piece future implementations will actually obey. It defines the language-neutral conformance corpus (the artifact that enforces engine parity) and the loss-ledger preservation contract (what a projection guarantees, not just what it drops). The engine under test is in LOGIC-RUNTIME.md; the semantics it must satisfy are in LOGIC-SEMANTICS.md.

Why a corpus

The Python oracle and the Rust core — and any future port — certify against one shared, language-neutral corpus of cases: static files, not re-derived assertions. This is the contract that lets the slow, correct reference and the fast Rust engine coexist and provably agree (Principle 7), exactly as GTS conformance design promotes the GTS §18 vectors into a conformance/ directory so any implementation certifies against the same files. The reasoning corpus is that contract for logic:, and it is the executable specification of the design's hardest invariants — no engine can drift from them without a red build.

Corpus layout

The corpus lands under conformance/logic/ once the logic: vocabulary exists (cases cannot be authored before the surface syntax does). Its shape:

conformance/logic/
  cases/<category>/<case>/
    input.logic.ttl          # logic: source (+ optional adapter owl:* / gufo:)
    profile.json             # declared semantic + world-types + requested mode + expected decidability class
    queries/<q>.logic        # goal-resolution / counterfactual queries (optional)
    expected/
      materialized.nq        # derived quads; worlds are named graphs
      verdicts.json          # world-indexed truth/modality + reasoning_lint-equivalent verdicts
      witnesses.nq           # contradiction witnesses as GMEOW statement graphs
      projections/           # OWL-DL / OWL-EL / Datalog / N3 / gUFO downcast + the preservation ledger
      explanation/<q>.md     # prose-explanation skeletons (faithful-by-construction)
      answers/<q>.json       # expected goal/counterfactual answer sets
  runner/                    # the language-neutral runner contract
  README.md

Categories and their verification contract

Each row is the material the design grounds, as input artifact → the expected-output check that gates engine parity. The four highlighted properties (lint-equivalence, the no-occurrence gate, no base-world leakage, explanation faithfulness) are the design's load-bearing invariants.

Runner contract

An engine implements one adapter — run(input, mode) → {materialized, verdicts, witnesses, projections, explanations, answers} — and the runner diff-compares each output to expected/. The Python oracle implements it first (the executable spec); the Rust core must pass the identical corpus; a JS/Go port self-certifies the same way. It wires into a make conformance target and, once the engine lands, into make check.

Determinism and comparison. No case may depend on iteration order. RDF outputs (materialized.nq, witnesses.nq, projections) compare by graph isomorphism; verdicts.json and answers/ compare as canonical JSON (sorted keys, normalized literals); explanations compare on the cited-IRI and rule-IRI skeleton, never the surface prose — a language model may vary the wording, never the set of axioms, rules, and sources it cites (the faithful-by-construction property from LOGIC-RUNTIME.md).

The loss ledger and preservation polarity

Loss is explicit and machine-readable, reusing the convention already in the mapping layer rather than inventing a vocabulary. gmeow:lossyDrop (dsl/mappings/vocabulary.ttl:237) records, per target, what structure a projection drops; the mapping compiler already aggregates such notes into projection headers (ProfileBinding.lossy_drops, src/gmeow_tools/mapping_dsl.py:151,493; mapping_compile.py:1778). generated/logic/projection-report.ttl aggregates these across every logic and foundation projection.

For reasoning projections, "lossy" is not enough. A consumer needs to know what a projection guarantees about answers, not only what it omits. The ledger therefore records, per projection, both a complexity/decidability class (EL → PTIME, DL → decidable/N2EXPTIME, Datalog → terminating/PTIME-data) and a preservation polarity:

The vocabulary:

logic:preservationKind
  logic:ExactPreservation ;
  logic:SoundUnderApproximation ;
  logic:CompleteOverApproximation ;
  logic:ValidationOnly ;
  logic:InconsistencyPreserving ;
  logic:InconsistencyReflecting .

A projection report entry can then say not just "dropped modality," but, for example: "OWL-EL is a logic:SoundUnderApproximation for subclass entailments under profile X; PTIME." This is what lets the BFO/DOLCE bridge views (LOGIC-MIGRATION.md) be labelled honestly: a bridge view is typically logic:ValidationOnly or carries no preservation claim at all, never logic:ExactPreservation, unless a specific subfragment is certified. The projections/ corpus category checks that each emitted projection matches its declared preservation kind and complexity class — overclaiming preservation is a red build, exactly like dropping a fact silently.