Backward chaining search

A search strategy for a Derivation of some Judgment that starts from the desired Judgment as the initial goal, picks a rule at each step with the conclusion as the current goal, adds its premises as subgoals into a queue & continues until all subgoals are Axioms.