Struct BackwardChainer 

pub struct BackwardChainer { /* private fields */ }

The backward chaining proof engine.

Searches for proofs by working backwards from the goal, finding rules whose conclusions match, and recursively proving their premises.

Implementations

impl BackwardChainer

pub fn new() -> Self

Create a new proof engine with empty knowledge base.

pub fn set_max_depth(&mut self, depth: usize)

Set the maximum proof search depth.

pub fn knowledge_base(&self) -> &[ProofExpr]

Get a reference to the knowledge base (for debugging).

pub fn add_axiom(&mut self, expr: ProofExpr)

Add an axiom/fact/rule to the knowledge base.

Event semantics are automatically abstracted to simple predicates for efficient proof search.

pub fn prove(&mut self, goal: ProofExpr) -> ProofResult<DerivationTree>

Attempt to prove a goal.

Returns a derivation tree if successful, explaining how the proof was constructed. Event semantics in the goal are automatically abstracted (but De Morgan is not applied to preserve goal pattern matching for reductio strategies).

pub fn prove_with_goal( &mut self, goal: ProofGoal, ) -> ProofResult<DerivationTree>

Prove a goal with pre-populated context assumptions.

This allows proving goals like “x > 5” given assumptions like “x > 10” in the context. The oracle (Z3) will use these context assumptions when verifying.

Trait Implementations

impl Default for BackwardChainer

fn default() -> Self

Returns the “default value” for a type.