Struct ProofGoal 

pub struct ProofGoal {
    pub target: ProofExpr,
    pub context: Vec<ProofExpr>,
}

The Goal State for the Backward Chainer.

Represents a “hole” in the proof that needs to be filled. During backward chaining, goals are decomposed into subgoals until they match known facts.

Fields

• target - What we are trying to prove
• context - Local assumptions (e.g., antecedents of implications we’ve entered)

See Also

• BackwardChainer::prove - Takes a goal and produces a derivation tree
• DerivationTree - The result of successfully proving a goal
• ProofExpr - The target type

Fields

target: ProofExpr

What we are trying to prove right now.

context: Vec<ProofExpr>

The local assumptions available (e.g., inside an implication).

Implementations

impl ProofGoal

pub fn new(target: ProofExpr) -> Self

pub fn with_context(target: ProofExpr, context: Vec<ProofExpr>) -> Self

Trait Implementations

impl Clone for ProofGoal

fn clone(&self) -> ProofGoal

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofGoal

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

Formats the value using the given formatter.