Class ArgumentEngine<TArg, TPremise, TExpr, TVar, TClaim>

Current engine behavior setting. Controls whether the auto-normalization (AN) rule set runs as a post-hook after every successful Structural mutation. See the JSDoc on TLogicEngineOptions.behavior for the full contract.

Registers a propositional variable for use across all premises.

Adds a premise-bound variable that references another argument's conclusion premise.

Adds a premise-bound variable that references a premise in a different argument.

Registers a premise-bound propositional variable whose truth value is derived from another premise's evaluation.

Builds a Map keyed by a caller-supplied function over all variables. Useful for indexing by extension fields (e.g. statementId). The caller should cache the result — this is O(n) per call.

Override point for subclasses to prevent forking. When this returns false, forkArgument will throw.

Enumerates all 2^n variable assignments and checks for counterexamples.

A counterexample is an admissible assignment where all supporting premises are true but the conclusion is false. The argument is valid if no counterexamples exist.

Calls validateEvaluability() (including derivation pre-flight) before enumeration. If the argument is not evaluable, returns early with an appropriate result rather than throwing.

Clears the conclusion designation.

Invariant guard (1.0.2): A non-empty argument always has a conclusion designated (E-7). On an argument with one or more premises this method is a no-op — it returns the current (unchanged) role state with an empty changeset rather than leaving the engine in an E-7-violating state. The only path to legitimately end up with no conclusion designated is to remove every premise first. On a zero-premise argument the call still clears (vacuously satisfies the invariant).

Collects all variables referenced by expressions across all premises, indexed both by variable ID and by symbol.

Creates a new premise with an auto-generated UUID and registers it with this engine.

Two call styles are supported:

• Typed-bag (preferred, since 0.11.0):

  engine.createPremise({
      type: "freeform",        // or "derivation"
      derivedClaimId: claimId, // required when type === "derivation"
      extras: { label: "P1" },
      symbol: "P1",
  })
  Copy

• Legacy positional (kept for compatibility):

  engine.createPremise(extras, symbol)  // creates a freeform premise
  Copy

When type === "derivation", the engine looks up derivedClaimId in the claim library, materializes a claim-bound variable for it (via ensureClaimBoundVariable) if one does not already exist, and initializes the premise's expression tree to the naked-Q form — a single variable expression at the root referencing the consequent.

Creates a premise with a caller-supplied ID and registers it with this engine. Mirrors createPremise exactly, but accepts an explicit id as the first argument instead of generating one.

Two call styles are supported:

• Typed-bag (preferred, since 0.11.0):

  engine.createPremiseWithId(id, {
      type: "freeform",        // or "derivation"
      derivedClaimId: claimId, // required when type === "derivation"
      extras: { label: "P1" },
      symbol: "P1",
  })
  Copy

• Legacy positional (kept for compatibility):

  engine.createPremiseWithId(id, extras, symbol)  // creates a freeform premise
  Copy

When type === "derivation", the same derivation initialization as createPremise runs: variable materialization and naked-Q tree setup.

Repair primitive: resolve D-3 violations (mixed-grounding antecedent — axioms + citations in one derivation) by deleting every axiom-bound variable expression from the offending antecedent subtree. The remaining citation-bound variables stay, giving the derivation a homogeneous citation-grounded antecedent.

User-initiated; never auto-runs. Respects behavior. In 'assistive' mode, AN may collapse a resulting single-child OR via AN-3; in 'permissive' the OR may persist with one child (a downstream D-2 violation — follow up with removeOrphanOperators() if desired).

Ensures a claim-bound variable for the given claim exists in this argument. If one already exists, returns it. Otherwise creates a new claim-bound variable with a fresh UUID, the current version of the claim from the ClaimLibrary, and an auto-generated symbol.

Evaluates the argument under a three-valued expression assignment.

Variables may be true, false, or null (unknown). All result flags (isAdmissibleAssignment, isCounterexample, etc.) are three-valued: null means indeterminate due to unknown variable values.

Calls validateEvaluability() internally before evaluation; if the argument is not structurally ready (including derivation pre-flight), the method returns early with { ok: false } and the validation details. Do not bypass evaluate to avoid this check.

Returns the PremiseEngine containing the given expression, or undefined.

Forces recomputation of all dirty checksums in the hierarchy.

Returns all expressions across all premises, sorted by ID.

Returns a shallow copy of the argument metadata with checksum attached.

Look up a claim by (id, version) in the engine's claim library. Returns undefined if the claim is not present. Exposed for repair primitives and other tooling that needs to inspect a claim's type discriminator at a particular version pinned by a claim-bound variable.

Returns the checksum for a named descendant collection. Null if collection is empty.

Returns the conclusion premise, or undefined if none is set.

Returns an expression by ID from any premise, or undefined if not found.

Returns the premise ID that contains the given expression, or undefined.

Returns all expressions that reference the given variable ID, across all premises.

Returns the argument's extra metadata record (all fields except id, version, and checksums).

Returns the premise with the given ID, or undefined if not found.

Returns the current role assignments (conclusion premise ID only; supporting is derived).

Returns the current reactive snapshot for external store consumption.

Returns the variable with the given ID, or undefined if not found.

Returns the variable with the given symbol, or undefined if not found.

Returns all registered variables sorted by ID.

Returns all premise-bound variables whose boundPremiseId matches the given premise ID. This is a linear scan over all variables.

Returns true if an expression with the given ID exists in any premise.

Returns true if a premise with the given ID exists.

Returns true if a variable with the given ID exists.

Returns all premise IDs in lexicographic order.

Returns all premises in lexicographic ID order.

Returns the root expression from each premise that has one.

Returns all supporting premises (derived: inference premises that are not the conclusion) in lexicographic ID order.

Global normalize pass per spec §6. Runs the AN rule set (AN-1..AN-4) everywhere it can fire, converging the argument toward tier (defaults to 'presentable').

normalize is non-destructive in the logical-meaning sense — it does not delete variables, change claim references, or modify operator semantics. Recovery from Evaluable or Derivable violations requires user intent and is exposed via the repair primitives.

In v1.0 every AN rule targets a Presentable invariant, so calls with tier ∈ {'structural', 'evaluable', 'derivable'} are effectively no-ops. The parameter exists as forward-compatible API surface for a future submit/finalize gate.

Bypasses behavior. normalize() is user-initiated (the UI invokes it after the user confirms a Tidy / Normalize action), so cleanup runs regardless of whether the engine is in 'assistive' or 'permissive' mode. The engine's behavior setting is not mutated by this call.

Patches application-specific fields onto an expression across all premises, then marks the expression and its ancestors dirty so the next checksum flush recomputes from the patched values.

This is the public API for consumers that need to attach app-level metadata (e.g. creatorId, createdOn) to expressions synthesized by the engine's auto-normalization. It resolves the owning premise internally, applies the patch in place via Object.assign, and marks the expression dirty — callers cannot patch without marking (stale checksum) or mark without patching (no-op).

Mirror of populateFromCitations for axiom connections. Same factory contract: naked-Q-only, no throw on already-populated.

Construct (or no-op on) the per-claim derivation premise's antecedent from a citation lookup. Factory + naked-Q-only:

• 0 connections → no-op (naked-Q stays).
• 1 connection → IMPLIES(citation-var, Q).
• ≥ 2 connections → IMPLIES(OR(c1, …, cn), Q). In 'assistive' mode the per-mutation AN-1 post-hook inserts a formula buffer between IMPLIES and OR; in 'permissive' the OR sits directly under IMPLIES (a P-1 violation surfaces via validate('presentable')).

No throw on already-populated. Per the Structural-only mutation throw rule, if the target derivation premise is not in the naked-Q form the factory returns { kind: 'no-op', state: <existing> } without mutating. UI/caller is responsible for explicit user consent + clearing the antecedent via a repair primitive before re-calling. Preserves the no-changes-without- consent principle.

Throws only when no derivation premise exists for the given derivedClaimId (legitimate entity-not-found Structural check).

Repair primitive: resolve E-6 violations (claim has > 1 derivation premise) by keeping one premise per derivedClaimId and deleting the rest. Strategy controls which premise is kept:

• 'keep-first' (default): keep the premise with the lexicographically smallest id; delete the rest. Deterministic and snapshot-stable.
• 'keep-largest-antecedent': keep the premise whose antecedent subtree has the most claim-bound variable expressions; tie-break by id.

User-initiated; never auto-runs. Respects behavior.

Repair primitive: resolve E-1 violations (operators with < 2 children) by running the AN-3 cleanup pass globally. Returns the violations resolved. The repair is non-meaning-changing — it only removes empty operators and promotes single-child operators — but lives alongside normalize() so the UI can present a focused "Remove N orphan operators" action with a precise return value.

User-initiated; never auto-runs. Bypasses behavior — cleanup runs even in permissive mode (the user has already accepted the action by clicking the repair button).

Removes a premise and reassigns any role assignments that reference it.

Invariant guard (1.0.2): when the removed premise was the conclusion AND other premises remain after the delete, the conclusion role is atomically reassigned to the lowest-id remaining premise (sorted lexicographically) rather than left undefined, preserving the engine-level invariant that a non-empty argument always has a conclusion designated (E-7). When the removed premise was the conclusion AND no premises remain, the role is cleared as before (vacuous invariant on the empty argument). Consumers that want a different reassignment policy (e.g., server-side createdOn ordering or a UI-defined sibling position) should issue their own setConclusionPremise(...) call immediately after this method returns — the post-mutation E-7 will continue to pass because a conclusion stays designated throughout.

Repair primitive: resolve E-3 violations by deleting each unresolvable claim- or premise-bound variable, cascading the removal across all premises. Returns the violations resolved (for UX confirmation / undo / "we made N changes" feedback).

User-initiated; never auto-runs. Respects behavior: in 'assistive' mode, the AN post-hook fires after each cascade mutation; in 'permissive' no AN runs.

Removes a variable and cascade-deletes all expressions referencing it across every premise (including their full subtrees). As of v1.0 operator collapse on the surviving parents is the AN-3 post-mutation hook's responsibility in assistive behavior; in permissive behavior the un-collapsed shape stays and surfaces via engine.validate('presentable').

Restores the engine to a previously captured snapshot state.

Switches the engine's behavior at runtime. Going permissive → assistive does not auto-run a global normalize() pass; the UI is expected to prompt the user before invoking normalize() explicitly.

As of v1.0 behavior is enforced entirely via the AN post-mutation hook in runAssistiveNormalization — the legacy per-flag grammarConfig plumbing that bridged behavior to premise-level enforcement is gone. Switching permissive → assistive makes the next successful Structural mutation trigger the AN pass; switching the other direction stops the AN pass from running until the user opts back in.

Designates a premise as the argument's conclusion.

Replaces the argument's extra metadata record.

Returns a serializable snapshot of the full engine state.

Registers a listener that is called after every mutation.

Renders the entity as a human-readable string.

Shallow-merges updates into the argument's existing extras.