Module engine 

Backward chaining proof engine.

“The machine that crawls backward from the Conclusion to the Axioms.”

This module implements the core proof search algorithm. It takes inference rules and hunts for proofs using backward chaining and unification.

Backward Chaining Strategy

1. Start with the goal we want to prove
2. Find rules whose conclusions unify with our goal
3. Recursively prove the premises of those rules
4. Build the derivation tree as we succeed

Example

Goal: Mortal(socrates)

Knowledge Base:
  - Human(socrates)
  - ∀x(Human(x) → Mortal(x))

Search:
  1. Goal matches conclusion of ∀x(Human(x) → Mortal(x)) with x=socrates
  2. New subgoal: Human(socrates)
  3. Human(socrates) matches knowledge base fact
  4. Build derivation tree: ModusPonens(UniversalInst, PremiseMatch)

Structs

BackwardChainer

The backward chaining proof engine.