Struct DerivationTree 

pub struct DerivationTree {
    pub conclusion: ProofExpr,
    pub rule: InferenceRule,
    pub premises: Vec<DerivationTree>,
    pub depth: usize,
    pub substitution: Substitution,
}

The “Euclidean Structure” - A recursive tree representing the proof.

This is the object returned by the Prover. It allows the UI to render a step-by-step explanation (Natural Language Generation).

Structure

Each node contains:

• conclusion: The proposition proved at this step
• rule: The logical rule applied (how we know the conclusion)
• premises: Sub-proofs justifying the rule’s requirements
• substitution: Variable bindings from unification

See Also

• BackwardChainer::prove - Creates derivation trees
• InferenceRule - The rules that justify each step
• ProofExpr - The conclusion type
• certifier::certify - Converts trees to kernel terms
• hints::suggest_hint - Suggests next steps when stuck

Fields

conclusion: ProofExpr

The logical statement proved at this node.

rule: InferenceRule

The rule applied to justify this conclusion.

premises: Vec<DerivationTree>

The sub-proofs that validate the requirements of the rule. Example: ModusPonens will have 2 children (The Implication, The Antecedent).

depth: usize

The depth of the tree (used for complexity limits).

substitution: Substitution

Substitution applied at this step (for unification-based rules).

Implementations

impl DerivationTree

pub fn new( conclusion: ProofExpr, rule: InferenceRule, premises: Vec<DerivationTree>, ) -> Self

Constructs a new Proof Node. Automatically calculates depth based on children.

pub fn leaf(conclusion: ProofExpr, rule: InferenceRule) -> Self

A leaf node (usually a Premise, Axiom, or Oracle result).

pub fn with_substitution(self, subst: Substitution) -> Self

Set the substitution for this derivation step.

pub fn display_tree(&self) -> String

Renders the proof as a text-based tree (for debugging/CLI).

Trait Implementations

impl Clone for DerivationTree

fn clone(&self) -> DerivationTree

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for DerivationTree

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for DerivationTree

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.