Interface: ProofDto

Defined in: src/types/inference.ts:167

Properties

aggregation?

optional aggregation?: AggregationEvidence

Defined in: src/types/inference.ts:272

Evidence for the arithmetic step that joins an aggregate’s contributor proofs. Present only on a node that computed an aggregate.

certainty

certainty: number

Defined in: src/types/inference.ts:256

Certainty of this proof step.

conclusion?

optional conclusion?: ProofConclusionDto

Defined in: src/types/inference.ts:245

The conclusion this node established, as a structured term. Read the sort and the features here, not from goalDisplay, which is a display convenience only. Absent on a node the engine reports no conclusion for.

goalDisplay?

optional goalDisplay?: string

Defined in: src/types/inference.ts:239

Human-readable rendering of the goal proven at this step — the conclusion, e.g. iam_permission(action: "view_file", object: "design.pdf", subject: "alice"). Lets a client render a readable proof tree without resolving term IDs.

goalTermId?

optional goalTermId?: string

Defined in: src/types/inference.ts:213

Term ID of the CONCLUSION this node proved.

Remarks

This is a fetchable id: it joins to client.query.findBySort() and client.terms.getTerm(). Two solutions of one goal carry the SAME id only when they prove the same conclusion — a goal with several solutions therefore reports several distinct ids.

ABSENT when no conclusion was materialised: a PROVE with no preceding CHAIN stores nothing. Read it as optional and fall back deliberately — ProofDto.goalDisplay renders the node without an id. When it is present it names a STORED term: a subsort conclusion proved under a parent goal from a tabled answer carries the id findBySort() lists for it, and so do the proof’s leaves.

With ProofDto.goalDisplay it is the conclusion’s identity: de-duplicate solutions by goalTermId when present, else by goalDisplay — never by ProofDto.ruleHeadTermId.

Before engine issue #281 this field named the rule’s instantiated head, so every solution of one goal shared one id and getTerm() answered 404 for it. That id is now ProofDto.ruleHeadTermId.

kind

kind: ProofKind

Defined in: src/types/inference.ts:188

How this goal was established. Always present — a client never has to infer it from the node’s shape.

Remarks

proved — a rule was applied, so ruleTermId and ruleLabel are filled. Either it fired in this search, or the goal was a conclusion a forward chain had materialised and the engine recovered the rule from its recorded derivation.
fact — a stored fact with no recorded derivation.
residuated — an open-world leaf: unknown, never false.
unattributed — a sound answer whose derivation the engine could not report.
truncated — established, but its derivation was not expanded: a depth or cycle bound, or an answer replayed from the tabling cache.

A goal carrying constraints is a CONJUNCTION: its root holds one subproof per clause and reports the strongest kind they carry — proved when any clause was proved by a rule, else fact.

residuated?

optional residuated?: boolean

Defined in: src/types/inference.ts:267

True iff this node is a residuated (suspended/unknown) leaf — an open-world antecedent with neither a witnessing fact nor a deriving rule.

Remarks

Unknown, never false: a residuated leaf means the engine could not decide the goal, not that the goal is refuted. Distinct from SolutionDto.residuatedSorts, which names the sorts of a solution’s residuated antecedents rather than marking an individual node of the proof tree.

ruleHeadTermId?

optional ruleHeadTermId?: string

Defined in: src/types/inference.ts:233

Term ID of the rule’s instantiated HEAD — the template the search unified with.

Remarks

Present only on a rule application, and only when it differs from ProofDto.goalTermId. It is rule scaffolding, NOT a fetchable id: client.terms.getTerm() refuses it deliberately.

It identifies the RULE’s head template, not one application of the rule: every solution one rule proves shares it. Solutions sharing a ruleHeadTermId were proved by the same rule — measured, four distinct unpaid(number: …) conclusions of one rule carried one id. It does not identify a conclusion and must not be used to de-duplicate solutions; the conclusion’s identity is ProofDto.goalTermId when present, else ProofDto.goalDisplay.

ruleLabel?

optional ruleLabel?: string

Defined in: src/types/inference.ts:250

Human-readable rendering of the rule applied at this step (its head Ψ-term). Absent for a stored fact / axiom (no rule was applied).

ruleTermId?

optional ruleTermId?: string

Defined in: src/types/inference.ts:215

The rule term ID used to prove this goal.

subproofs?

optional subproofs?: ProofDto[]

Defined in: src/types/inference.ts:254

Sub-proofs for intermediate goals.

substitution

substitution: HomoiconicSubstitutionDto

Defined in: src/types/inference.ts:252

The substitution applied at this proof step.