Interface: ProofDto
@kortexya/reasoninglayer / Inference / ProofDto
Interface: ProofDto
Defined in: src/types/inference.ts:34
Recursive proof tree node.
Represents a step in the proof derivation, potentially with sub-proofs for intermediate goals.
Properties
certainty
certainty:
number
Defined in: src/types/inference.ts:55
Certainty of this proof step.
goalDisplay?
optionalgoalDisplay:string
Defined in: src/types/inference.ts:44
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
goalTermId:
string
Defined in: src/types/inference.ts:36
The goal term ID that was proved at this step.
residuated?
optionalresiduated:boolean
Defined in: src/types/inference.ts:66
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.
ruleLabel?
optionalruleLabel:string
Defined in: src/types/inference.ts:49
Human-readable rendering of the rule applied at this step (its head Ψ-term). Absent for a stored fact / axiom (no rule was applied).
ruleTermId?
optionalruleTermId:string
Defined in: src/types/inference.ts:38
The rule term ID used to prove this goal.
subproofs?
optionalsubproofs:ProofDto[]
Defined in: src/types/inference.ts:53
Sub-proofs for intermediate goals.
substitution
substitution:
HomoiconicSubstitutionDto
Defined in: src/types/inference.ts:51
The substitution applied at this proof step.