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. This is the exhaustive entailment check; the single-assignment premisesHoldConclusionFalse fact is a weaker, reader-relative statement and not a countermodel.

Premise-set satisfiability is computed once before the row loop and threaded into each row, since the generated assignments carry no operator decisions and the premise set never varies.

Grounded claim-bound variables — axiomatic and citation — are excluded from the enumeration and pinned true on every row, so an argument with g of them enumerates 2^(k - g) assignments and no counterexample can rest on a cited claim reading false. Evaluation is deliberately different: it answers the reader's question, where a citation is only seeded true and remains assignable.

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.

Derives a default truth-value assignment for every variable in the argument, from claim type and immediate support structure alone. Values are true or null (unknown) — never false.

D(claim) for the variable backing claim c:

1. c is a citation or axiomatic claim → true.
2. c is a normal claim: locate its derivation premise (the inference whose consequent is c's variable). Seed each variable referenced in that premise's immediate antecedent true iff it is itself bound to a citation/axiomatic claim, else null, and Kleene-evaluate the antecedent once. Antecedent true → true; otherwise null. No recursion — only the immediate antecedent claims' types are inspected, never their own supports.
3. Anything else (no derivation premise, naked-Q derivation, a premise-bound variable) → null.

The returned map is variable-keyed; use getVariableIdForClaim / getClaimIdForVariable to translate to/from claimId.

Consistency with the axiomatic pre-pass: evaluate force-sets axiomatic-bound variables true and rejects any explicit assignment for them (AXIOM_VARIABLE_ASSIGNMENT_FORBIDDEN). This map reports those same variables as true (the two agree), but the axiom keys must not be passed to evaluate directly. Feed the map through evaluateWithDefaults (which drops them), or strip axiomatic-bound keys before calling evaluate yourself.

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 assigned true, false, or null (unknown). Evaluation reports a fourth value, CONTESTED, for anything the reader's assignments and the steps they granted force both true and false; null still means indeterminate. isAdmissibleAssignment, survivingSupportingPremisesTrue, conclusionTrue and premisesHoldConclusionFalse all range over the four values; premiseSetSatisfiable stays three-valued, since it is a classical search over the premise set alone.

The result is a set of orthogonal facts, not a single outcome. In particular survivingSupportingPremisesTrue is vacuously true when every supporting premise is struck, so whether the argument reached its conclusion is conclusionAttribution.reachedWithoutAssertion and never that field. A rejected operator strikes its whole premise and asserts nothing.

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.

Axiomatic-bound variables are forced true by this method's pre-pass and passed down as forcedTrueVariableIds, so they are never read back as reader assertions and never enter the reached-without-assertion counterfactual. A caller's own forcedTrueVariableIds is unioned with that set, never substituted for it.

The premise-set satisfiability search is given a wider set — satisfiabilityForcedTrueVariableIds, every grounded variable, citation as well as axiomatic. Whether the premises can hold together is a question about the argument, so a cited claim is taken at its source's word there, exactly as checkValidity does. The two sets are separate because the narrower one also decides what counts as the reader's own assertion, and a reader may disagree with a source: a citation belongs in the satisfiability question and not in that one.

Convenience: merge caller overrides over deriveDefaultAssignment() and evaluate in one call. Default-sourced axiomatic-bound keys are dropped before evaluation — the engine's pre-pass force-sets them true and rejects explicit axiom assignments, so passing the default true through would throw AXIOM_VARIABLE_ASSIGNMENT_FORBIDDEN. Dropping them keeps deriveDefaultAssignment (which reports axioms as true) and the pre-pass in agreement without double-applying. An override that names an axiomatic variable is left intact, so evaluate still enforces the one-way rule.

Citations are different from axioms. The engine does not force citation-bound variables true and does not reject an explicit citation assignment — a citation is a free variable, so its default true is kept here (dropping it would leave the citation unknown at evaluation). Both citations and axioms read as true under defaults, but only the axiom true comes from the engine; the citation true is supplied by this map. That also makes citation defaults reviewer- overridable, whereas axioms stay locked.

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 claimId a claim-bound variable is bound to, or undefined when the variable is unknown or premise-bound (premise-bound variables have no claim). Inverse of getVariableIdForClaim.

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 the ID of the lowest-id claim-bound variable bound to claimId in this argument, or undefined if no variable is. Pure lookup — it never creates a variable (contrast ensureClaimBoundVariable).

The engine's evaluation surface is variable-keyed, but consumers key their review/UI state by claimId; this accessor (with its inverse getClaimIdForVariable) is the documented seam for translating between the two.

It answers for one variable, and a claim may bind several. The pick is deterministic and snapshot-stable — variables enumerate sorted by id — but arbitrary with respect to the claim: it is not "the authored one" or "the one an evaluation settled". When a claim may bind more than one and losing the others would be wrong, use getVariableIdsForClaim.

Returns the IDs of every claim-bound variable bound to claimId in this argument, in the engine's id-sorted variable order, or [] when none is. Pure lookup — it never creates a variable (contrast ensureClaimBoundVariable).

A claim may bind more than one variable: addVariable enforces no per-claim uniqueness, so an argument can carry several variables standing for the same proposition, each reached — and valued — independently by evaluation. Any translation that must not lose one of them (reading propagated values back onto a claim, say) belongs here rather than on the singular accessor.

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, and marks the expression dirty — callers cannot patch without marking (stale checksum) or mark without patching (no-op). A field whose value is undefined is deleted rather than assigned, so clearing one restores the shape and the checksum the entity had before it was set.

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.