Interface TArgumentEvaluation

What a reader's answers on this response's links carry into the argument it answers, one step along a chain of answers. Only agree answers carry, and each agreed link carries exactly what it says or is reported in notCarried with the reason it cannot (see TNotCarriedReason).

• A statement link carries fixed claim values when what it says about its expression, read with every claim free, is exactly a set of fixed values; contradicting Q ∧ R is not.
• A reinforce carries accepted only at a premise root that is implies or iff; an undercut carries rejected wherever evaluation honours a rejection.
• Into another response, the result is answers on that response's links.

Merge the result into the reader's own input with mergeCarriedInput.

Whether one link of this response follows from its other premises, read against the snapshot of the argument it answers. Each statement link is expanded into the expression it names and claims are merged into one column each, so the question is about what the links say. Answers follows, asserted, incoherent, undetermined or invalid; see TLinkCheckResult.

Whether all of this response's premises can hold at once, over the same expanded premise set as checkLink, so the two never disagree. When they cannot, gives a minimal set of premises that cannot.

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.

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): a citation/axiomatic claim's variable → true; a normal claim's variable → true iff its derivation premise's immediate antecedent Kleene-evaluates true when each immediately-referenced claim is seeded true iff citation/axiomatic (else null) — one level, no recursion; everything else → null.

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

The map reports axiomatic-bound variables as true in agreement with evaluate's force-true pre-pass, but those keys must not be passed to evaluate directly (it rejects explicit axiom assignments). Use evaluateWithDefaults, or strip axiomatic-bound keys first.

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.

Merges caller overrides over deriveDefaultAssignment() and evaluates in one call. Default-sourced axiomatic-bound keys are dropped before evaluation (the engine force-sets them true), so the defaults and the pre-pass agree without tripping AXIOM_VARIABLE_ASSIGNMENT_FORBIDDEN. An override naming an axiomatic variable is preserved so evaluate still enforces the rule.

Returns the claimId a claim-bound variable is bound to, or undefined when the variable is unknown or premise-bound. Inverse of getVariableIdForClaim.

Returns the ID of the lowest-id claim-bound variable bound to claimId, or undefined if none exists. Pure lookup — never creates a variable (contrast ensureClaimBoundVariable). The documented seam, with its inverse, for translating between the variable-keyed evaluation surface and consumers' claimId-keyed state.

A claim may bind several variables. The pick among them is deterministic (variables enumerate id-sorted) but arbitrary with respect to the claim — reach for getVariableIdsForClaim when that matters.

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

A claim may bind more than one variable — addVariable enforces no per-claim uniqueness — and each is valued independently by evaluation. Use this, not the singular accessor, wherever dropping the others would be wrong.

Returns the derivation-specific subset of validateEvaluability checks as an invariant result. Only derivation premises are inspected; freeform premises are ignored.

Use this to pre-check derivation structure before entering the full evaluation pipeline, without requiring a conclusion or complete role state.

Derivation premises with broken trees produce violations with code DERIVATION_STRUCTURE_INVALID. Naked-Q (single-variable root) is a valid Derivable state and is not flagged here — it is skipped by evaluation rather than thrown.

Validates that this argument is structurally ready for evaluation: a conclusion must be set, all role references must point to existing premises, variable ID/symbol mappings must be consistent, every premise must be individually evaluable, and all derivation premise structures must be well-formed (naked-Q invariant; since 0.11.0).

Derivation premises with structurally broken trees are flagged with DERIVATION_STRUCTURE_INVALID. Use validateDerivationStructures() to isolate derivation checks without running the full evaluability sweep.

Naked-Q derivation premises (single-variable root) are not flagged — they are a valid Derivable state and are skipped by evaluation rather than throwing.