Struct TheoremTrace 

pub struct TheoremTrace {
    pub verified: bool,
    pub premises: Vec<String>,
    pub goal: String,
    pub trace: Option<String>,
    pub error: Option<String>,
}

An English theorem proved, with its FOL and a human-readable PROOF TRACE — the “English in → proof out, see the trace” path. Parsing yields the premises and goal as FOL; the kernel-certified backward chainer yields the derivation, which renders as an indented step-by-step proof.

Fields

verified: bool

Whether the goal was proved (kernel-certified).

premises: Vec<String>

The premises, rendered as FOL — what the English compiled to.

goal: String

The goal, rendered as FOL.

trace: Option<String>

The derivation rendered as an indented proof trace (└─ [Rule] conclusion per step). None when no derivation was found.

error: Option<String>

The verification error, when proving failed.

Trait Implementations

impl Clone for TheoremTrace

fn clone(&self) -> TheoremTrace

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TheoremTrace

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

Formats the value using the given formatter.