Optionalconfig: TLogicEngineOptionsProtectedexpressionsProtectedgrammarProtectedpremiseProtectedrootProtectedvariablesAdds an expression to this premise's tree.
If the expression has parentId: null it becomes the root; only one
root is permitted per premise. All structural rules (implies/iff
root-only, child limits, position uniqueness) are enforced.
When the wrapInsertFormula flag is enabled (either directly via
TAutoNormalizeConfig or via autoNormalize: true), operator nesting
violations are auto-corrected by inserting a formula buffer between
the parent operator and the non-not operator child, rather than
throwing. The same flag also controls auto-insertion in
insertExpression and wrapExpression.
The expression to add, including position and parent assignment.
The added expression (with checksum) and changeset.
Adds an expression immediately before or after an existing sibling, with position computed automatically.
When the repositionOnCollision auto-normalize flag is enabled,
sibling positions are automatically redistributed if the computed
midpoint position would collide with an existing sibling. Only the
minimal set of nodes is repositioned. Repositioned siblings appear
in changes.expressions.modified.
The ID of the existing sibling expression.
Whether to insert "before" or "after"
the sibling.
The expression to add (position is auto-assigned).
The added expression (with checksum) and changeset.
Adds an expression as the last child of the given parent, with
position computed automatically. If parentId is null, the
expression becomes the root.
When the repositionOnCollision auto-normalize flag is enabled,
sibling positions are automatically redistributed if the computed
position would collide with an existing sibling. Repositioned
siblings appear in changes.expressions.modified.
The parent expression ID, or null for root.
The expression to add (position is auto-assigned).
The added expression (with checksum) and changeset.
ProtectedassertProtectedassertChanges the operator type of an existing operator expression.
Handles three structural cases automatically:
newOperator. Dissolves the current operator and
reparents its children under the parent.sourceChildId and
targetChildId into a new sub-operator of type newOperator,
inserting a formula buffer if required by grammar enforcement.The operator expression to change.
The target operator type.
OptionalsourceChildId: stringFirst child to include in a split (required when >2 children).
OptionaltargetChildId: stringSecond child to include in a split (required when >2 children).
OptionalextraFields: Partial<TExpr>Optional partial expression fields merged into any newly created expressions (formula buffer, new sub-operator). Structural fields (id, type, operator, parentId, position, premiseId, argumentId, argumentVersion) cannot be overridden.
result — For simple change: the updated operator expression. For merge: null (operator was dissolved). For split: the newly created sub-operator expression. changes — Full changeset with correct hierarchical checksums.
Returns the meta checksum — derived from entity data only.
Returns the combined checksum — hash(checksum + descendantChecksum), or equals checksum if no descendants.
Deletes all expressions that reference the given variable ID, including their subtrees. Operator collapse runs after each removal.
The variable ID whose referencing expressions should be removed.
The removed expressions and changeset.
Returns the descendant checksum — derived from children's combinedChecksums. Null if no children.
Evaluates the premise under a three-valued expression assignment.
Variable values are looked up using Kleene three-valued logic
(null = unknown). Missing variables default to null. For
inference premises (implies/iff), an inferenceDiagnostic is
computed with three-valued fields unless the root is rejected.
The variable assignment and optional rejected expression IDs.
Optionaloptions: {Optional evaluation options.
OptionalrequireExactCoverage?: booleanIf true, the assignment must
cover exactly the referenced variables.
Optionalresolver?: (variableId: string) => boolean | nullOptionalstrictUnknownKeys?: booleanIf true, unknown variable keys
in the assignment cause an error.
The premise evaluation result.
Forces recomputation of all dirty checksums in the hierarchy.
Returns the child expressions of the given parent, sorted by position.
The parent expression ID, or null for root-level
children.
An array of child expression entities.
Returns the checksum for a named descendant collection. Null if collection is empty.
Returns the operator expressions a reviewer can accept or reject, in pre-order depth-first tree order.
Excludes "not" operators (NOT is flipped via a render-time flag,
not voted on) and skips formula nodes (they are traversed but never
emitted). Returns [] for empty premises and premises with no
operators.
Order is stable across calls on the same PremiseEngine instance;
callers typically rely on index for step-queue construction.
An array of decidable operator expression entities.
Returns an expression by ID, or undefined if not found in this
premise.
The expression ID to look up.
The expression entity, or undefined.
Returns the premise's extra metadata record.
The extras record.
Returns the premise ID.
The premise ID string.
Returns the set of variable IDs referenced by expressions in this
premise. Only variables that appear in type: "variable" expression
nodes are included.
A Set of referenced variable ID strings.
Returns the root expression, or undefined if the premise is empty.
The root expression entity, or undefined.
Returns the ID of the root expression, or undefined if the premise
is empty.
The root expression ID, or undefined.
Returns all argument-level variables (from the shared VariableManager) sorted by ID. Since the VariableManager is shared across all premises, this returns every registered variable — not just those referenced by expressions in this premise.
An array of variable entities.
Splices a new expression between existing nodes in the tree. The new
expression inherits the tree slot of the anchor node
(leftNodeId ?? rightNodeId).
The expression to insert, including position and parent assignment.
OptionalleftNodeId: stringThe existing node to become the left child of the new expression.
OptionalrightNodeId: stringThe existing node to become the right child of the new expression.
The inserted expression (with checksum) and changeset.
Returns true if this premise does not have an inference operator at
its root. Equivalent to !isInference().
Whether this premise is a constraint.
Returns true if the root expression is an implies or iff
operator, meaning this premise expresses a logical inference
relationship.
Whether this premise is an inference.
Loads expressions in BFS order with the nesting check bypassed. Bypasses all PremiseEngine validation (ownership, variable existence, circularity) since restoration paths trust existing data completely.
Invalidates the cached checksum so the next call recomputes it.
Performs a full normalization sweep on this premise's expression tree.
Collapses unjustified formulas, operators with 0/1 children, and inserts
formula buffers where needed. Works regardless of autoNormalize setting.
One-shot helper that builds the antecedent of this derivation premise from the current global support (citations + axiom invocations) of the derived claim.
Behavior by total support count n = citations + axioms:
IMPLIES(VarExpr(S1), Q).IMPLIES(formula(OR(VarExpr(S1), …, VarExpr(Sn))), Q).
Citations come first, axioms second; source order preserved within
each. The formula buffer between IMPLIES and OR is auto-inserted by
the engine's standard grammar. A supporting claim referenced by
multiple connections — for example, two citations from this derived
claim to the same supporting claim — appears exactly once in the
antecedent, at its first source-order position.Materializes a claim-bound variable for each supporting claim via
argumentEngine.ensureClaimBoundVariable(supportingClaimId).
Tree construction approach: Mutations are performed via super.*
calls, bypassing this class's overrides (which call assertWellFormed()
after every mutation and would reject intermediate states during
multi-step construction). Standard grammar is used throughout — the
engine's wrapInsertFormula rule inserts a formula buffer between
IMPLIES and OR for n ≥ 2 automatically. assertWellFormed() is called
at the end to validate the final state.
Removes an expression and optionally its entire descendant subtree, then collapses any ancestor operators with fewer than two children.
The ID of the expression to remove.
Whether to remove all descendants as well.
The removed root expression, or undefined if not found.
Sets a callback that runs full argument-level invariant validation.
Injected by ArgumentEngine so the premise can delegate to the
argument-level validator.
A function returning the invariant validation result,
or undefined to clear.
Sets a callback that checks whether adding a variable-expression to a
premise would create a circular binding. Injected by ArgumentEngine
to enable cross-premise cycle detection. If not set, only the direct
check (within the premise itself) runs.
A function that returns true if adding the variable
to the premise would create a cycle, or undefined to clear.
Sets a callback that checks whether a premise-bound variable's target
premise has an empty expression tree. Injected by ArgumentEngine to
enable cross-premise validation. Used during validateEvaluability.
A function that returns true if the variable's bound
premise has no root expression, or undefined to clear.
Replaces the premise's extra metadata record.
The new extras record.
The new extras record and a changeset with the modified premise.
Overrides the grammar config for both this premise engine and its internal expression manager. Used by restoration paths when the caller's grammar config should override the snapshot's config.
Sets a callback invoked after every mutation, or undefined to
clear.
The mutation callback, or undefined to remove.
Sets a callback that returns the full set of variable IDs registered
in the argument. Injected by ArgumentEngine.
A function returning the set of registered variable
IDs, or undefined to clear.
Returns a serializable snapshot of the premise's owned state.
The premise engine snapshot.
Renders the entity as a human-readable string.
A human-readable display string.
Toggles negation on an expression. If the expression's parent is a NOT operator, removes the NOT (promoting the expression). Otherwise, wraps the expression with a new NOT operator.
When the target is already a NOT expression and collapseDoubleNegation
is enabled, removes the existing NOT (promoting its child) instead of
wrapping in another NOT — preventing NOT(NOT(x)).
When the target is a non-not operator and negationInsertFormula is
enabled, auto-inserts a formula buffer between the new NOT and the
target to satisfy the operator nesting restriction. Throws if the flag
is disabled and enforceFormulaBetweenOperators is true.
The ID of the expression to toggle negation on.
OptionalextraFields: Partial<TExpr>Optional additional fields to merge into newly created expressions (NOT and formula nodes). Structural fields (id, type, operator, parentId, position, premiseId, argumentId, argumentVersion) cannot be overridden.
The new NOT expression when adding negation, or null when
removing it, along with the changeset.
Returns a serializable premise representation containing only
identity/metadata and checksum. Use getRootExpressionId(),
getExpressions(), getReferencedVariableIds() for runtime state.
The premise data entity.
Updates mutable fields of an existing expression. Only position,
variableId, and operator may be updated.
The ID of the expression to update.
The fields to update.
The updated expression and changeset.
Shallow-merges updates into the premise's existing extras.
Key-value pairs to merge into the current extras.
The merged extras record and a changeset with the modified premise.
Run invariant validation on this premise and its expression tree.
Validates that this premise is structurally ready for evaluation.
A validation result with any issues found.
Walks the premise's expression tree, invoking the visitor for each node,
and returns the visitor's result for the root. Returns the result of
visitor.empty() when the premise has no root expression.
Callbacks for each expression node type.
The visitor's result for the root node, or visitor.empty()
if the premise is empty.
ProtectedwithWraps an existing expression with a new operator and a new sibling in a single atomic operation.
The operator takes the existing node's slot in the tree. Both the
existing node and the new sibling become children of the operator.
Exactly one of leftNodeId / rightNodeId must be provided — it
identifies the existing node and which child slot it occupies.
The new operator expression to wrap with.
The new sibling expression to add alongside the existing node.
OptionalleftNodeId: stringThe existing node to place as the left child.
OptionalrightNodeId: stringThe existing node to place as the right child.
The inserted operator (with checksum) and changeset.
StaticfromRestore a ManagedDerivationPremiseEngine from a serialized snapshot,
applying both derivation-type and structural validation. Throws on
tampered or structurally invalid snapshots.
Delegates to PremiseEngine.fromSnapshot for the full restoration logic
(including the private rebuildVariableIndex pass), then upgrades the
prototype and validates. TypeScript's static methods do not support
super, so the parent is called by name and the result is recast.
OptionalexpressionIndex: Map<string, string>OptionalgrammarConfig: TGrammarConfigOptionalgenerateId: () => string
A managed engine for derivation premises that enforces structural rules from the v0.11.0 spec on construction and on snapshot restoration.
Construction validates the premise type (
DERIVATION_TYPE_MISMATCHif the premise isn'ttype: "derivation"). Full expression-tree structural validation (DERIVATION_STRUCTURE_INVALID) runs infromSnapshot— after expressions are loaded — and will be called from mutation overrides in Task 6.Note: The constructor only validates the premise type, not the expression tree, because
PremiseEngineis always constructed before expressions are loaded (expressions are added separately via mutations orloadExpressions). Structural validation at the end offromSnapshotcatches tampered snapshots, and Task 6 mutation overrides will enforce it on every change.The classic
PremiseEngineis permissive and allows mutations that leave a derivation premise temporarily or permanently invalid. The managed engine wraps it for safe, structurally-enforced editing.Use
ManagedDerivationPremiseEngine.fromSnapshot(...)to restore from a serialized snapshot — the validation pass catches tampered snapshots.