Forward chaining search backward chaining search

A search strategy for a Derivation of a Judgment form that keeps track of the currently derivable judgments (initially the Axioms) and tries to expand the set using the rules at each step.