Interface: ProofConclusionDto
@kortexya/reasoninglayer / ProofConclusionDto
Interface: ProofConclusionDto
Section titled “Interface: ProofConclusionDto”Defined in: src/types/inference.ts:46
The conclusion a proof node established, as a structured term.
Remarks
Section titled “Remarks”The same shape the term read routes answer with: a sort id, a sort name and typed feature values in the tagged ValueDto encoding, where a reference carries its term id. It is present whether or not the conclusion was ever stored, so a client never parses ProofDto.goalDisplay to learn the sort or a feature of a derived conclusion.
The features are the term’s data features (no _-prefixed engine feature, no
when / constraints, no rule machinery), with every variable resolved
through the node’s substitution. A feature whose variable the derivation left
unbound (an open-world head) is Uninstantiated, never dropped. goalDisplay
can omit such a feature, so conclusion is the complete record and
goalDisplay is not.
Properties
Section titled “Properties”features
Section titled “features”features:
Record<string,ValueDto>
Defined in: src/types/inference.ts:48
Feature name to typed value, in the tagged ValueDto encoding.
sortId
Section titled “sortId”sortId:
string
Defined in: src/types/inference.ts:50
The conclusion’s sort id (UUID).
sortName?
Section titled “sortName?”
optionalsortName?:string
Defined in: src/types/inference.ts:55
The conclusion’s sort name in the caller’s lattice. Absent only when the lattice does not hold the sort; a name is never invented.
termId?
Section titled “termId?”
optionaltermId?:string
Defined in: src/types/inference.ts:62
The stored term this conclusion is, equal to the node’s
ProofDto.goalTermId and fetchable from client.terms.getTerm().
Absent when the conclusion was never materialised (a proof with no
preceding CHAIN); the sort and features are present either way.