feat(deductive): binary relations + multi-variable grounding (finite propositional)

Extends evals/deductive_logic/grounding.py from unary predicates / single-var rules to
binary relations + multi-variable universal rules, still by FINITE PROPOSITIONAL
grounding into the regime the ROBDD engine + the independent truth-table oracle both
decide. wrong==0 stays structural. This is the real capability step a RuleTaker/
ProofWriter-style mirror needs (the unary fragment alone is trivial).

- atom_n lowers pred(a,b) -> pred__a__b; arity-1 is byte-identical to the old atom, so
  the live unary panel lowers unchanged (proven by an exact-string back-compat test).
- multi-variable universal rules ground over n^k assignments — transitivity now decides.
- range-restriction: a rule with a head variable unbound in the body refuses (unsafe_rule)
  — it grounds soundly but is outside the clean regime real benchmarks use.
- typed refusals: arity>=3/functions, explicit quantifiers, variable-free rules, bounds.

Honest ceilings (documented in docs/analysis/relational-grounding-extension-2026-06-04.md):
- THE binding constraint is the GOLD, not the grammar: the truth-table oracle is
  O(2^atoms), so grounding refuses above MAX_GROUND_ATOMS=20 => binary problems cap at
  ~4 entities/predicate. A real lift needs a 2nd genuinely-independent sub-enumeration
  oracle (not built).
- OPEN-WORLD only: RuleTaker/ProofWriter's main splits are closed-world + NAF; a future
  adapter MUST refuse CWA/NAF (mapping CWA "False"->"refuted" is a wrong=0 breach).
- arity <= 2, function-free.

Validated: held-out differential fuzz (400 random binary problems, oracle-golded) = 0
engine/oracle mismatches; unary back-compat byte-identical; INV-25b reproducibility green;
deductive lane wrong=0 16/16; smoke 87.

docs/analysis/relational-grounding-extension-2026-06-04.md

@@ -0,0 +1,62 @@
+<!-- CANONICAL | docs/analysis/relational-grounding-extension-2026-06-04.md | 2026-06-04 | capability/grounding-extension | binary relations + multi-variable universal rules by finite propositional grounding, with the honest coverage ceilings | verified: held-out fuzz engine==oracle (0 mismatches), back-compat byte-identical, smoke green -->
+
+# Binary-relation + multi-variable grounding extension
+
+Extends the finite-entity grounding (`evals/deductive_logic/grounding.py`) from **unary
+predicates / single-variable rules** to **binary relations + multi-variable universal
+rules**, still by **finite propositional grounding** into the regime the ROBDD entailment
+operator and the independent truth-table oracle both decide. `wrong == 0` stays structural.
+This is the real capability step that makes a RuleTaker/ProofWriter-style mirror cover
+anything beyond the trivial unary fragment — the prerequisite the runway doc's PR-3 needs.
+
+## What landed
+
+- **Arity 1–2.** A literal is legacy unary `{predicate, entity|var, polarity}` OR general
+  `{predicate, args:[{entity|var: str}, ...], polarity}`. `atom_n` lowers
+  `predicate(a, b)` → `predicate__a__b`; arity-1 is byte-identical to the old `atom`, so
+  every pre-existing unary problem lowers unchanged (proven).
+- **Multi-variable universal rules**, grounded by enumerating every assignment of the
+  rule's variables to named entities (`n^k`). The canonical transitive rule
+  `∀x,y,z. bigger(x,y) ∧ bigger(y,z) → bigger(x,z)` now grounds and decides correctly.
+- **Range-restriction (safety).** A rule whose head contains a variable unbound in the
+  body (`p(x) → q(y)`) refuses (`unsafe_rule`) — it grounds soundly but is outside the
+  clean regime real benchmarks use. Narrowness is the firewall.
+- **Refusals** (typed): arity ≥ 3 / functions (`unsupported_predicate_arity`); explicit
+  quantifiers (`unsupported_quantifier`); a variable-free rule (`unsupported_quantifier`);
+  and the bounds below (`grounding_bound_exceeded`).
+
+## The honest ceilings (these are real limits, not hidden)
+
+1. **The binding constraint is the independent GOLD, not the grammar.** The INV-25 gold is
+   a truth-table oracle — **O(2^atoms)**. Binary relations explode the atom count
+   (`n` entities → up to `n²` atoms per binary predicate). So the grounding refuses above
+   `MAX_GROUND_ATOMS = 20` (2²⁰ ≈ 1e6 assignments, decidable). **Consequence: binary
+   problems cap at ~4 entities per predicate.** That is the true coverage ceiling — bigger
+   problems refuse. (A future lift would need a *second* sub-enumeration oracle that is
+   still genuinely independent of the ROBDD — non-trivial; not done.)
+2. **Open-world only.** The grounding decides classical (monotone, open-world) entailment:
+   underivable ⇒ `unknown`, not `false`. RuleTaker / ProofWriter's main splits are
+   **closed-world with negation-as-failure** (underivable ⇒ False). Any future benchmark
+   adapter **must refuse CWA/NAF cases** — mapping a CWA "False" to "refuted" would be a
+   `wrong=0` breach. Only the **OWA** split is honestly mirrorable.
+3. **Function-free, arity ≤ 2.** Ternary+ relations and functions refuse.
+
+## Validation (held-out, not hand-authored)
+
+- **Differential fuzz:** 400 randomly-generated binary problems (binary facts + a
+  transitive rule), gold computed by the **independent truth-table oracle**, decided by
+  the **ROBDD engine** — **0 engine/oracle mismatches** on every in-regime case. This is
+  the anti-overfit check: the gold is oracle-derived on data the grammar was not authored
+  against, so it is a real `wrong=0` signal, not a 15-case hand-authored echo.
+- **Back-compat:** the unary path lowers byte-identically; the committed finite-entity
+  gold is still reproduced by the independent oracle (INV-25b green); deductive lane
+  `wrong=0` unchanged; smoke green.
+
+## What this unblocks / what it does NOT claim
+
+- Unblocks: a ProofWriter-**OWA**, function-free, ≤2-arity, small-entity adapter (the
+  runway's PR-3) that can cover *relational/transitive* cases, not just the unary fragment.
+- Does **not** claim any benchmark number: the actual RuleTaker/ProofWriter data is **not
+  in the repo**. A real number requires obtaining the dataset (license-checked) and is
+  explicitly scoped to "the OWA function-free ≤2-arity small fragment," with everything
+  else refused — never "ProofWriter accuracy."

evals/deductive_logic/grounding.py

@@ -28,7 +28,9 @@ Sealed: no ``chat`` import, no serving path. Deterministic.
 from __future__ import annotations
 
 import re
+from collections.abc import Sequence
 from dataclasses import dataclass
+from itertools import product
 from typing import Any, Final
 
 # Closed refusal vocabulary for the grounding layer — distinct from the entailment
@@ -40,6 +42,14 @@ UNKNOWN_ENTITY: Final[str] = "unknown_entity"
 UNKNOWN_VARIABLE: Final[str] = "unknown_variable"
 MALFORMED_CASE: Final[str] = "malformed_case"
 EMPTY_CASE: Final[str] = "empty_case"
+# A rule whose head contains a variable not bound in its body (non-range-restricted /
+# "unsafe" in Datalog terms). It grounds soundly, but it is outside the clean regime
+# real rule benchmarks use; refuse rather than silently widen scope.
+UNSAFE_RULE: Final[str] = "unsafe_rule"
+# The independent gold is a truth-table oracle, O(2^atoms); the grounding refuses a
+# problem whose distinct-atom count (or entity/variable count) would make that gold
+# intractable, rather than emit something the wrong=0 arbiter cannot decide.
+GROUNDING_BOUND_EXCEEDED: Final[str] = "grounding_bound_exceeded"
 
 GROUNDING_REASONS: Final[frozenset[str]] = frozenset({
     UNSUPPORTED_PREDICATE_ARITY,
@@ -49,8 +59,25 @@ GROUNDING_REASONS: Final[frozenset[str]] = frozenset({
     UNKNOWN_VARIABLE,
     MALFORMED_CASE,
     EMPTY_CASE,
+    UNSAFE_RULE,
+    GROUNDING_BOUND_EXCEEDED,
 })
 
+# ---------------------------------------------------------------------------
+# Bounds (v1.5: binary relations + multi-variable rules by finite grounding).
+# ---------------------------------------------------------------------------
+# Arity ceiling — unary + binary only; arity >= 3 refuses (functions never).
+MAX_ARITY: Final[int] = 2
+# A rule grounds over n^k assignments (n entities, k distinct variables). These two
+# bound n and k so n^k cannot blow up before the atom bound below is even checked.
+MAX_ENTITIES: Final[int] = 8
+MAX_VARS_PER_RULE: Final[int] = 3
+# THE binding constraint: the independent truth-table oracle is O(2^atoms). The
+# lowered problem's distinct-atom count must stay small or the gold is intractable.
+# 2^20 ~ 1e6 assignments — decidable; binary relations therefore cap at ~4 entities
+# per predicate. This is the honest coverage ceiling of the binary extension.
+MAX_GROUND_ATOMS: Final[int] = 20
+
 _ATOM_SEPARATOR: Final[str] = "__"
 # A slug component: lowercase ASCII letters/digits/single underscores, no leading
 # digit, no empty, no double-underscore (would collide with the separator).
@@ -96,11 +123,21 @@ def atom(predicate: Any, entity: Any) -> str:
     return f"{slug(predicate)}{_ATOM_SEPARATOR}{slug(entity)}"
 
 
-def _literal(predicate: Any, entity: Any, polarity: Any) -> str:
+def atom_n(predicate: Any, entity_slugs: Sequence[str]) -> str:
+    """``predicate(arg1, ..., argk)`` → the canonical propositional atom.
+
+    Arity 1 is byte-identical to :func:`atom` (``predicate__entity``), so every
+    pre-existing unary problem lowers unchanged. The ``__`` separator between args
+    cannot collide with a slug (slugs reject ``__``), so the atom is injective in
+    ``(predicate, args)`` and arity-1 vs arity-2 atoms never alias.
+    """
+    return _ATOM_SEPARATOR.join([slug(predicate), *(slug(e) for e in entity_slugs)])
+
+
+def _lit_str(atom_str: str, polarity: Any) -> str:
     if not isinstance(polarity, bool):
         raise GroundingError(MALFORMED_CASE, f"polarity must be a bool, got {polarity!r}")
-    a = atom(predicate, entity)
+    return atom_str if polarity else f"~{atom_str}"
-    return a if polarity else f"~{a}"
 
 
 def _require(condition: bool, reason: str, detail: str = "") -> None:
@@ -108,94 +145,161 @@ def _require(condition: bool, reason: str, detail: str = "") -> None:
         raise GroundingError(reason, detail)
 
 
-def _check_unary(obj: dict[str, Any], *, allow_var: bool) -> None:
+# A term is ("entity", name) or ("var", name) — name is the raw case string.
-    """Reject any non-unary / relational / functional shape (v1 is unary only)."""
+_Term = tuple[str, str]
-    keys = set(obj)
+_NormLiteral = tuple[Any, tuple[_Term, ...], bool]
-    # A binary relation / function would carry extra argument keys.
+
-    extra = keys - {"predicate", "entity", "var", "polarity"}
+
-    _require(not extra, UNSUPPORTED_PREDICATE_ARITY, f"unexpected keys {sorted(extra)}")
+def _normalize_term(arg: Any, *, allow_var: bool) -> _Term:
-    has_entity = "entity" in obj
+    _require(isinstance(arg, dict), MALFORMED_CASE, f"arg not a mapping: {arg!r}")
-    has_var = "var" in obj
+    extra = set(arg) - {"entity", "var"}
-    if allow_var:
+    _require(not extra, MALFORMED_CASE, f"unexpected arg keys {sorted(extra)}")
-        _require(has_entity ^ has_var, MALFORMED_CASE, "literal needs exactly one of entity/var")
+    has_entity, has_var = "entity" in arg, "var" in arg
+    _require(has_entity ^ has_var, MALFORMED_CASE, "arg needs exactly one of entity/var")
+    if has_var:
+        _require(allow_var, UNKNOWN_VARIABLE, "free variable outside a rule")
+        v = arg["var"]
+        _require(isinstance(v, str) and bool(v.strip()), MALFORMED_CASE, "empty variable")
+        return ("var", v)
+    return ("entity", arg["entity"])
+
+
+def _normalize_literal(obj: Any, *, allow_var: bool) -> _NormLiteral:
+    """Normalize a literal — legacy unary ``{entity|var}`` OR general
+    ``{args:[{entity|var},...]}`` — to ``(predicate, terms, polarity)``. Refuses
+    arity 0 / > :data:`MAX_ARITY` (functions and ternary relations) with a typed reason.
+    """
+    _require(isinstance(obj, dict), MALFORMED_CASE, f"literal not a mapping: {obj!r}")
+    _require("predicate" in obj, MALFORMED_CASE, "literal missing predicate")
+    polarity = obj.get("polarity", True)
+    _require(isinstance(polarity, bool), MALFORMED_CASE, f"polarity must be bool: {polarity!r}")
+
+    if "args" in obj:
+        _require("entity" not in obj and "var" not in obj, MALFORMED_CASE,
+                 "use 'args' OR 'entity'/'var', not both")
+        extra = set(obj) - {"predicate", "args", "polarity"}
+        _require(not extra, UNSUPPORTED_PREDICATE_ARITY, f"unexpected keys {sorted(extra)}")
+        args = obj["args"]
+        _require(isinstance(args, list) and bool(args), MALFORMED_CASE, "args must be a non-empty list")
+        terms = tuple(_normalize_term(a, allow_var=allow_var) for a in args)
     else:
-        _require(has_entity and not has_var, UNKNOWN_VARIABLE, "free variable outside a rule")
+        extra = set(obj) - {"predicate", "entity", "var", "polarity"}
+        _require(not extra, UNSUPPORTED_PREDICATE_ARITY, f"unexpected keys {sorted(extra)}")
+        has_entity, has_var = "entity" in obj, "var" in obj
+        _require(has_entity ^ has_var, MALFORMED_CASE, "unary literal needs exactly one of entity/var")
+        if has_var:
+            _require(allow_var, UNKNOWN_VARIABLE, "free variable outside a rule")
+            v = obj["var"]
+            _require(isinstance(v, str) and bool(v.strip()), MALFORMED_CASE, "empty variable")
+            terms = (("var", v),)
+        else:
+            terms = (("entity", obj["entity"]),)
+
+    _require(1 <= len(terms) <= MAX_ARITY, UNSUPPORTED_PREDICATE_ARITY,
+             f"arity {len(terms)} outside 1..{MAX_ARITY}")
+    if not allow_var:
+        _require(all(k == "entity" for k, _ in terms), UNKNOWN_VARIABLE, "free variable outside a rule")
+    return obj["predicate"], terms, polarity
+
+
+def _collect_vars(literals: Sequence[_NormLiteral]) -> list[str]:
+    """Distinct variable names across a rule's literals, in first-seen order."""
+    names: list[str] = []
+    for _pred, terms, _pol in literals:
+        for kind, name in terms:
+            if kind == "var" and name not in names:
+                names.append(name)
+    return names
 
 
 def lower_case(case: dict[str, Any]) -> GroundedProblem:
     """Lower a finite-entity case to ``(premises, query)``. Refuse-first.
 
-    Schema (v1):
+    Schema (v1.5 — extends v1 with binary relations + multi-variable rules):
         {"entities": [str, ...],
-         "facts": [{"predicate": str, "entity": str, "polarity": bool}, ...],
+         "facts":    [<ground literal>, ...],
-         "rules": [{"if": [<unary literal with var>, ...],
+         "rules":    [{"if": [<literal-with-vars>, ...], "then": <literal-with-vars>}, ...],
-                    "then": <unary literal with var>}, ...],
+         "query":    <ground literal>}
-         "query": {"predicate": str, "entity": str, "polarity": bool}}
+
+    A literal is either legacy unary ``{"predicate","entity"|"var","polarity"}`` or
+    general ``{"predicate","args":[{"entity"|"var": str}, ...],"polarity"}`` of arity
+    1..2. Universal rules are grounded by enumerating every assignment of their
+    variables to named entities (``n^k``). Unary single-var problems lower
+    byte-identically to v1. Anything outside the regime or above the bounds refuses.
     """
-    if not isinstance(case, dict) or not case:
+    _require(isinstance(case, dict) and bool(case), EMPTY_CASE, "case is empty or not a mapping")
-        raise GroundingError(EMPTY_CASE, "case is empty or not a mapping")
 
     entities = case.get("entities")
-    if not (isinstance(entities, list) and entities):
+    if not (isinstance(entities, list) and entities):  # narrows for the type checker
         raise GroundingError(EMPTY_CASE, "no entities")
-    entity_set = {slug(e) for e in entities}  # also validates each entity slug
+    _require(len(entities) <= MAX_ENTITIES, GROUNDING_BOUND_EXCEEDED,
+             f"{len(entities)} entities > {MAX_ENTITIES}")
+    entity_slugs = [slug(e) for e in entities]  # validates each entity slug
+    entity_set = set(entity_slugs)
     _require(len(entity_set) == len(entities), MALFORMED_CASE, "duplicate entities after slugging")
-
+    _require("query" in case, MALFORMED_CASE, "no query")
-    if "query" not in case:
-        raise GroundingError(MALFORMED_CASE, "no query")
-
-    premises: list[str] = []
 
     facts = case.get("facts", []) or []
     rules = case.get("rules", []) or []
     _require(isinstance(facts, list), MALFORMED_CASE, "facts must be a list")
     _require(isinstance(rules, list), MALFORMED_CASE, "rules must be a list")
 
-    # Facts — ground unary literals over named entities.
+    premises: list[str] = []
-    for fact in facts:
+    atoms_seen: set[str] = set()
-        _require(isinstance(fact, dict), MALFORMED_CASE, f"fact is not a mapping: {fact!r}")
-        _check_unary(fact, allow_var=False)
-        _require(slug(fact["entity"]) in entity_set, UNKNOWN_ENTITY, str(fact.get("entity")))
-        premises.append(_literal(fact["predicate"], fact["entity"], fact.get("polarity", True)))
 
-    # Rules — single-variable universal rules, grounded by explicit entity expansion.
+    def emit(predicate: Any, resolved: list[str], polarity: bool) -> str:
+        a = atom_n(predicate, resolved)
+        atoms_seen.add(a)
+        _require(len(atoms_seen) <= MAX_GROUND_ATOMS, GROUNDING_BOUND_EXCEEDED,
+                 f"{len(atoms_seen)} distinct atoms > {MAX_GROUND_ATOMS} "
+                 "(the independent truth-table gold is O(2^atoms))")
+        return _lit_str(a, polarity)
+
+    def resolve(terms: tuple[_Term, ...], sigma: dict[str, str]) -> list[str]:
+        out: list[str] = []
+        for kind, name in terms:
+            if kind == "var":
+                out.append(sigma[name])  # already a validated entity slug
+            else:
+                s = slug(name)
+                _require(s in entity_set, UNKNOWN_ENTITY, str(name))
+                out.append(s)
+        return out
+
+    # Facts — ground literals (no variables).
+    for fact in facts:
+        predicate, terms, polarity = _normalize_literal(fact, allow_var=False)
+        premises.append(emit(predicate, resolve(terms, {}), polarity))
+
+    # Rules — universal, grounded over every assignment of variables to entities.
     for rule in rules:
         _require(isinstance(rule, dict), MALFORMED_CASE, f"rule is not a mapping: {rule!r}")
         _require("quantifier" not in rule and "exists" not in rule,
-                 UNSUPPORTED_QUANTIFIER, "only implicit single-var universal rules in v1")
+                 UNSUPPORTED_QUANTIFIER, "only implicit universal rules are supported")
         body = rule.get("if")
         head = rule.get("then")
-        if not (isinstance(body, list) and body):
+        _require(isinstance(body, list) and bool(body), MALFORMED_CASE, "rule body must be a non-empty list")
-            raise GroundingError(MALFORMED_CASE, "rule body must be a non-empty list")
+        _require(isinstance(head, dict), MALFORMED_CASE, "rule head must be a literal")
-        if not isinstance(head, dict):
+        body_norm = [_normalize_literal(lit, allow_var=True) for lit in body]
-            raise GroundingError(MALFORMED_CASE, "rule head must be a literal")
+        head_norm = _normalize_literal(head, allow_var=True)
-        var = _rule_variable(body, head)
+        var_names = _collect_vars([*body_norm, head_norm])
-        for ent in entities:
+        _require(bool(var_names), UNSUPPORTED_QUANTIFIER,
-            body_atoms = [_literal(lit["predicate"], ent, lit.get("polarity", True)) for lit in body]
+                 "a rule must contain at least one variable (a variable-free rule is just a fact)")
-            head_atom = _literal(head["predicate"], ent, head.get("polarity", True))
+        _require(len(var_names) <= MAX_VARS_PER_RULE, GROUNDING_BOUND_EXCEEDED,
-            body_conj = " & ".join(f"({b})" for b in body_atoms)
+                 f"{len(var_names)} variables > {MAX_VARS_PER_RULE}")
-            premises.append(f"({body_conj}) -> ({head_atom})")
+        # Range-restriction (safety): every head variable must be bound in the body.
-        _ = var  # validated; grounding is by explicit entity expansion, not by name
+        unbound = set(_collect_vars([head_norm])) - set(_collect_vars(body_norm))
+        _require(not unbound, UNSAFE_RULE, f"head variable(s) {sorted(unbound)} not bound in the body")
+        for assignment in product(entity_slugs, repeat=len(var_names)):
+            sigma = dict(zip(var_names, assignment, strict=True))
+            body_lits = [emit(p, resolve(ts, sigma), pol) for (p, ts, pol) in body_norm]
+            hp, hts, hpol = head_norm
+            head_lit = emit(hp, resolve(hts, sigma), hpol)
+            body_conj = " & ".join(f"({b})" for b in body_lits)
+            premises.append(f"({body_conj}) -> ({head_lit})")
 
-    query = case["query"]
+    # Query — a ground literal.
-    _require(isinstance(query, dict), MALFORMED_CASE, "query must be a literal")
+    qpred, qterms, qpol = _normalize_literal(case["query"], allow_var=False)
-    _check_unary(query, allow_var=False)
+    query_lit = emit(qpred, resolve(qterms, {}), qpol)
-    _require(slug(query["entity"]) in entity_set, UNKNOWN_ENTITY, str(query.get("entity")))
-    query_lit = _literal(query["predicate"], query["entity"], query.get("polarity", True))
 
     return GroundedProblem(premises=tuple(premises), query=query_lit)
-
-
-def _rule_variable(body: list[dict[str, Any]], head: dict[str, Any]) -> str:
-    """Confirm the rule is single-variable: every literal uses one shared var,
-    no named entities (those would make it not universal). Returns the var name."""
-    seen: set[str] = set()
-    for lit in (*body, head):
-        _require(isinstance(lit, dict), MALFORMED_CASE, f"rule literal not a mapping: {lit!r}")
-        _check_unary(lit, allow_var=True)
-        _require("var" in lit, MALFORMED_CASE, "rule literals must use a variable, not a named entity")
-        v = lit["var"]
-        _require(isinstance(v, str) and bool(v.strip()), MALFORMED_CASE, "empty variable")
-        seen.add(v)
-    _require(len(seen) == 1, UNSUPPORTED_QUANTIFIER, f"v1 allows one variable per rule, saw {sorted(seen)}")
-    return seen.pop()

tests/test_deductive_logic_finite_entity_grounding.py

@@ -17,9 +17,9 @@ import pytest
 from evals.deductive_logic.grounding import (
     MALFORMED_CASE,
     UNKNOWN_ENTITY,
+    UNSAFE_RULE,
     UNSAFE_SYMBOL,
     UNSUPPORTED_PREDICATE_ARITY,
-    UNSUPPORTED_QUANTIFIER,
     GroundingError,
     atom,
     lower_case,
@@ -125,14 +125,18 @@ def test_binary_relation_refuses_as_unsupported_arity() -> None:
     assert exc.value.reason == UNSUPPORTED_PREDICATE_ARITY
 
 
-def test_multi_variable_rule_refuses() -> None:
+def test_unsafe_rule_unbound_head_var_refuses() -> None:
+    """v1.5 supports multi-variable rules — but a rule whose HEAD variable is not
+    bound in the body is non-range-restricted (unsafe) and still refuses. (Range-
+    restricted multi-var rules like transitivity are exercised in
+    test_deductive_logic_relational_grounding.py.)"""
     case = {"entities": ["a"],
             "rules": [{"if": [{"predicate": "p", "var": "x", "polarity": True}],
                        "then": {"predicate": "q", "var": "y", "polarity": True}}],
             "query": {"predicate": "p", "entity": "a", "polarity": True}}
     with pytest.raises(GroundingError) as exc:
         lower_case(case)
-    assert exc.value.reason == UNSUPPORTED_QUANTIFIER
+    assert exc.value.reason == UNSAFE_RULE
 
 
 def test_empty_case_refuses() -> None:

tests/test_deductive_logic_relational_grounding.py

@@ -0,0 +1,237 @@
+"""Binary-relation + multi-variable grounding extension (deductive-logic runway #1).
+
+Extends the finite-entity grounding from unary predicates / single-var rules to
+binary relations and multi-variable universal rules, still by FINITE PROPOSITIONAL
+grounding into the regime the ROBDD entailment operator + the independent truth-table
+oracle both decide. wrong==0 stays structural: every committed case is checked
+engine==oracle==(open-world) gold, and anything outside the regime refuses.
+
+Two contracts this pins hard:
+- **back-compat**: existing unary problems lower byte-identically (no panel regression);
+- **the oracle-tractability ceiling**: the gold is O(2^atoms), so the grounding refuses
+  above a pinned distinct-atom bound (GROUNDING_BOUND_EXCEEDED) rather than emit a
+  problem the independent gold cannot decide.
+"""
+
+from __future__ import annotations
+
+import random
+
+import pytest
+
+from evals.deductive_logic.grounding import (
+    GROUNDING_BOUND_EXCEEDED,
+    UNSAFE_RULE,
+    UNSUPPORTED_PREDICATE_ARITY,
+    UNSUPPORTED_QUANTIFIER,
+    GroundingError,
+    MAX_GROUND_ATOMS,
+    atom_n,
+    lower_case,
+)
+from evals.deductive_logic.oracle import oracle_entailment
+from generate.proof_chain.entail import evaluate_entailment
+
+
+def _decide(case: dict) -> tuple[str, str]:
+    gp = lower_case(case)
+    engine = evaluate_entailment(gp.premises, gp.query).outcome.value
+    oracle = oracle_entailment(gp.premises, gp.query)
+    return engine, oracle
+
+
+# --- back-compat: unary lowers exactly as before ---------------------------
+
+
+def test_unary_back_compat_entailed():
+    case = {
+        "entities": ["cat", "dog"],
+        "facts": [{"predicate": "furry", "entity": "cat", "polarity": True}],
+        "rules": [{"if": [{"predicate": "furry", "var": "x", "polarity": True}],
+                   "then": {"predicate": "mammal", "var": "x", "polarity": True}}],
+        "query": {"predicate": "mammal", "entity": "cat", "polarity": True},
+    }
+    gp = lower_case(case)
+    # exact atom + clause strings the unary path produced before the extension
+    assert gp.query == "mammal__cat"
+    assert "furry__cat" in gp.premises
+    assert "((furry__cat)) -> (mammal__cat)" in gp.premises
+    assert "((furry__dog)) -> (mammal__dog)" in gp.premises
+    engine, oracle = _decide(case)
+    assert engine == oracle == "entailed"
+
+
+# --- binary relations ------------------------------------------------------
+
+
+def test_binary_atom_form():
+    assert atom_n("loves", ["a", "b"]) == "loves__a__b"
+    assert atom_n("furry", ["cat"]) == "furry__cat"  # arity-1 unchanged
+
+
+def test_binary_fact_and_query():
+    case = {
+        "entities": ["alice", "bob"],
+        "facts": [{"predicate": "loves", "args": [{"entity": "alice"}, {"entity": "bob"}],
+                   "polarity": True}],
+        "query": {"predicate": "loves", "args": [{"entity": "alice"}, {"entity": "bob"}],
+                  "polarity": True},
+    }
+    engine, oracle = _decide(case)
+    assert engine == oracle == "entailed"
+
+
+def test_transitivity_entailed():
+    """The canonical RuleTaker/ProofWriter shape: a 3-variable transitive rule."""
+    case = {
+        "entities": ["bear", "dog", "cat"],
+        "facts": [
+            {"predicate": "bigger", "args": [{"entity": "bear"}, {"entity": "dog"}], "polarity": True},
+            {"predicate": "bigger", "args": [{"entity": "dog"}, {"entity": "cat"}], "polarity": True},
+        ],
+        "rules": [{
+            "if": [
+                {"predicate": "bigger", "args": [{"var": "x"}, {"var": "y"}], "polarity": True},
+                {"predicate": "bigger", "args": [{"var": "y"}, {"var": "z"}], "polarity": True},
+            ],
+            "then": {"predicate": "bigger", "args": [{"var": "x"}, {"var": "z"}], "polarity": True},
+        }],
+        "query": {"predicate": "bigger", "args": [{"entity": "bear"}, {"entity": "cat"}], "polarity": True},
+    }
+    engine, oracle = _decide(case)
+    assert engine == oracle == "entailed"
+
+
+def test_transitivity_unknown_is_open_world():
+    """The reverse direction is NOT derivable → unknown under OPEN-world entailment
+    (NOT 'refuted' — this is exactly why CWA benchmark splits must refuse, not map here)."""
+    case = {
+        "entities": ["bear", "dog", "cat"],
+        "facts": [
+            {"predicate": "bigger", "args": [{"entity": "bear"}, {"entity": "dog"}], "polarity": True},
+            {"predicate": "bigger", "args": [{"entity": "dog"}, {"entity": "cat"}], "polarity": True},
+        ],
+        "rules": [{
+            "if": [
+                {"predicate": "bigger", "args": [{"var": "x"}, {"var": "y"}], "polarity": True},
+                {"predicate": "bigger", "args": [{"var": "y"}, {"var": "z"}], "polarity": True},
+            ],
+            "then": {"predicate": "bigger", "args": [{"var": "x"}, {"var": "z"}], "polarity": True},
+        }],
+        "query": {"predicate": "bigger", "args": [{"entity": "cat"}, {"entity": "bear"}], "polarity": True},
+    }
+    engine, oracle = _decide(case)
+    assert engine == oracle == "unknown"
+
+
+# --- regime refusals -------------------------------------------------------
+
+
+def test_arity_three_refuses():
+    case = {
+        "entities": ["a", "b", "c"],
+        "facts": [{"predicate": "between",
+                   "args": [{"entity": "a"}, {"entity": "b"}, {"entity": "c"}], "polarity": True}],
+        "query": {"predicate": "between",
+                  "args": [{"entity": "a"}, {"entity": "b"}, {"entity": "c"}], "polarity": True},
+    }
+    with pytest.raises(GroundingError) as exc:
+        lower_case(case)
+    assert exc.value.reason == UNSUPPORTED_PREDICATE_ARITY
+
+
+def test_unsafe_rule_refuses():
+    """A range-restricted multi-var rule (transitivity) is fine; an unsafe one — a
+    head variable unbound in the body — refuses."""
+    case = {
+        "entities": ["a", "b"],
+        "facts": [{"predicate": "p", "args": [{"entity": "a"}, {"entity": "b"}], "polarity": True}],
+        "rules": [{
+            "if": [{"predicate": "p", "args": [{"var": "x"}, {"var": "y"}], "polarity": True}],
+            "then": {"predicate": "q", "args": [{"var": "x"}, {"var": "z"}], "polarity": True},  # z unbound
+        }],
+        "query": {"predicate": "q", "args": [{"entity": "a"}, {"entity": "b"}], "polarity": True},
+    }
+    with pytest.raises(GroundingError) as exc:
+        lower_case(case)
+    assert exc.value.reason == UNSAFE_RULE
+
+
+def test_explicit_quantifier_refuses():
+    case = {
+        "entities": ["a"],
+        "rules": [{"exists": True, "if": [{"predicate": "p", "var": "x", "polarity": True}],
+                   "then": {"predicate": "q", "var": "x", "polarity": True}}],
+        "query": {"predicate": "q", "entity": "a", "polarity": True},
+    }
+    with pytest.raises(GroundingError) as exc:
+        lower_case(case)
+    assert exc.value.reason == UNSUPPORTED_QUANTIFIER
+
+
+def test_atom_bound_refuses_intractable_oracle():
+    """A binary rule over 6 entities grounds to 36 binary atoms > the bound: refuse
+    rather than hand the O(2^atoms) gold a problem it cannot decide."""
+    ents = ["e0", "e1", "e2", "e3", "e4", "e5"]
+    case = {
+        "entities": ents,
+        "facts": [{"predicate": "r", "args": [{"entity": "e0"}, {"entity": "e1"}], "polarity": True}],
+        "rules": [{
+            "if": [{"predicate": "r", "args": [{"var": "x"}, {"var": "y"}], "polarity": True},
+                   {"predicate": "r", "args": [{"var": "y"}, {"var": "z"}], "polarity": True}],
+            "then": {"predicate": "r", "args": [{"var": "x"}, {"var": "z"}], "polarity": True},
+        }],
+        "query": {"predicate": "r", "args": [{"entity": "e0"}, {"entity": "e5"}], "polarity": True},
+    }
+    with pytest.raises(GroundingError) as exc:
+        lower_case(case)
+    assert exc.value.reason == GROUNDING_BOUND_EXCEEDED
+
+
+# --- held-out differential fuzz: engine == oracle on random binary problems --
+
+
+def _random_binary_case(rng: random.Random) -> dict:
+    # One binary predicate over 2-3 entities → <=9 atoms, so the O(2^atoms) gold
+    # stays fast while still exercising binary facts + a multi-var transitive rule.
+    ents = [f"e{i}" for i in range(rng.randint(2, 3))]
+    facts = []
+    for a in ents:
+        for b in ents:
+            if rng.random() < 0.4:
+                facts.append({"predicate": "r", "args": [{"entity": a}, {"entity": b}],
+                              "polarity": rng.random() < 0.85})
+    rules = []
+    if rng.random() < 0.75:
+        rules.append({
+            "if": [{"predicate": "r", "args": [{"var": "x"}, {"var": "y"}], "polarity": True},
+                   {"predicate": "r", "args": [{"var": "y"}, {"var": "z"}], "polarity": True}],
+            "then": {"predicate": "r", "args": [{"var": "x"}, {"var": "z"}], "polarity": True},
+        })
+    qa, qb = rng.choice(ents), rng.choice(ents)
+    query = {"predicate": "r", "args": [{"entity": qa}, {"entity": qb}],
+             "polarity": rng.random() < 0.85}
+    return {"entities": ents, "facts": facts, "rules": rules, "query": query}
+
+
+def test_held_out_fuzz_engine_equals_oracle():
+    """wrong==0 on held-out (oracle-golded, never hand-authored) random binary problems.
+    The independent truth-table oracle is the gold; the ROBDD engine must match it on
+    every in-regime case. A single mismatch is a soundness breach."""
+    rng = random.Random(20260604)
+    decided = 0
+    mismatches: list[str] = []
+    for _ in range(400):
+        case = _random_binary_case(rng)
+        try:
+            gp = lower_case(case)
+        except GroundingError:
+            continue  # out-of-regime / over-bound → refused, not scored
+        engine = evaluate_entailment(gp.premises, gp.query).outcome.value
+        oracle = oracle_entailment(gp.premises, gp.query)
+        decided += 1
+        if engine != oracle:
+            mismatches.append(f"{engine}!={oracle} :: {gp.premises} |- {gp.query}")
+    assert decided >= 50, f"too few in-regime cases ({decided}) — fuzz is near-vacuous"
+    assert not mismatches, f"{len(mismatches)} engine/oracle mismatches; first: {mismatches[:3]}"
+    assert MAX_GROUND_ATOMS <= 24  # the oracle stays tractable