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 an expression-bound variable to a response: a variable that stands for one expression of the argument the response answers, either its truth (boundAspect: "statement") or whether its step holds ("inference"). Only a response may hold one, and it binds only into the argument and version named by respondsTo. A variable with the same referent — the same expression and aspect — is returned instead of a second one being added.

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.

Reads what a reader's answers on this response's links carry into the argument it answers, one step along a chain of answers. See TCarryResult and TNotCarriedReason.

Answers invalid, without carrying anything, when this argument is not a response, the snapshot is not the argument and version it answers, or validateLinks reports an error. It never throws on an answer it cannot carry.

Whether one link of this response follows from the response's other premises, read against the snapshot of the argument it answers. Each statement link is expanded into the expression it names, so the question is asked of what the links say rather than of the links as opaque values. See TLinkCheckResult for each answer.

Answers invalid, without searching, when the snapshot is not the argument and version this response answers or validateLinks reports a problem.

Whether all of this response's premises can hold at once, read against the snapshot of the argument it answers. Uses the same expansion as checkLink, so the two never disagree: when the premises cannot all hold, every link checks as incoherent.

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: 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).

A response is the exception: it has no conclusion (E-7 exempts it, E-8 reports one it was stored with), so the call always clears.

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 covers the argument's authored supporting premises — derivation premises are excluded, being engine wiring rather than authored support — and is vacuously true when every one of them 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.

operatorAssignments is passed to evaluate unchanged; without it no operator decision is made. Values carried from a response go in overrides and operatorAssignments through mergeCarriedInput, so the order is defaults, then carried values, then the reader's own.

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, checksums and respondsTo).

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

The argument this response answers, or undefined for a standard argument.

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 the premise-bound variables bound to the given premise of this argument. A variable bound into another argument is never included, even when that argument's premise has the same 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.

Whether this argument is a response: it carries respondsTo, the argument it answers pinned to one version, and has no conclusion.

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. In a response, which has no conclusion, it returns every premise that is not a link.

Global normalize pass. 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.

Every AN rule currently targets a Presentable invariant, so calls with tier ∈ {'structural', 'evaluable', 'derivable'} are effectively no-ops. The parameter is reserved so a future submit/finalize gate can add lower-tier rules without an API break.

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).

Moves a response to a newer version of the argument it answers.

The classification is computed again here, as classifyBindings computes it, from targetFrom, targetTo and options. Then:

• respondsTo becomes targetTo;
• every unchanged binding is re-pointed to targetTo;
• every changed or removed binding takes its decision from decisions.bindings: keep re-points it to the same expression, retarget to another expression of targetTo in the same aspect, and drop removes it with every premise its entry lists;
• the response's claim-bound variables are left alone, whether or not either version uses their claims.

Before returning, it checks that every expression-bound variable is bound to targetTo and names an expression present there, and that validateLinks against targetTo reports no fault, by code, variable and expression, that it did not report before. Any failure undoes the whole rebase. The changeset holds the argument with its new respondsTo and every variable re-pointed, added or removed.