Backward chaining


Backward chaining is an inference method described colloquially as working backward from the goal. It is used in automated theorem provers, inference engines, proof assistants, and other artificial intelligence applications.
In game theory, researchers apply it to subgames to find a solution to the game, in a process called backward induction. In chess, it is called retrograde analysis, and it is used to generate table bases for chess endgames for computer chess.
Backward chaining is implemented in logic programming by SLD resolution. Both rules are based on the modus ponens inference rule. It is one of the two most commonly used methods of reasoning with inference rules and logical implications – the other is forward chaining. Backward chaining systems usually employ a depth-first search strategy, e.g. Prolog.

How it works

Backward chaining starts with a list of goals and works backwards from the consequent to the antecedent to see if any data supports any of these consequents. An inference engine using backward chaining would search the inference rules until it finds one with a consequent that matches a desired goal. If the antecedent of that rule is known to be true, then it is added to the list of goals.
For example, suppose a new pet, Fritz, is delivered in an opaque box along with two facts about Fritz:
The goal is to decide whether Fritz is green, based on a rule base containing the following four rules:
  1. If X croaks and X eats flies – Then X is a frog
  2. If X chirps and X sings – Then X is a canary
  3. If X is a frog – Then X is green
  4. If X is a canary – Then X is yellow
With backward reasoning, an inference engine can determine whether Fritz is green in four steps. To start, the query is phrased as a goal assertion that is to be proved: "Fritz is green".
1. Fritz is substituted for X in rule #3 to see if its consequent matches the goal, so rule #3 becomes:
If Fritz is a frog – Then Fritz is green
Since the consequent matches the goal, the rules engine now needs to see if the antecedent can be proved. The antecedent therefore becomes the new goal:
Fritz is a frog
2. Again substituting Fritz for X, rule #1 becomes:
If Fritz croaks and Fritz eats flies – Then Fritz is a frog
Since the consequent matches the current goal, the inference engine now needs to see if the antecedent can be proved. The antecedent therefore becomes the new goal:
Fritz croaks and Fritz eats flies
3. Since this goal is a conjunction of two statements, the inference engine breaks it into two sub-goals, both of which must be proved:
Fritz croaks
Fritz eats flies
4. To prove both of these sub-goals, the inference engine sees that both of these sub-goals were given as initial facts. Therefore, the conjunction is true:
Fritz croaks and Fritz eats flies
therefore the antecedent of rule #1 is true and the consequent must be true:
Fritz is a frog
therefore the antecedent of rule #3 is true and the consequent must be true:
Fritz is green
This derivation therefore allows the inference engine to prove that Fritz is green. Rules #2 and #4 were not used.
Note that the goals always match the affirmed versions of the consequents of implications and even then, their antecedents are then considered as the new goals, which ultimately must match known facts ; thus, the inference rule used is modus ponens.
Because the list of goals determines which rules are selected and used, this method is called goal-driven, in contrast to data-driven forward-chaining inference. The backward chaining approach is often employed by expert systems.
Programming languages such as Prolog, Knowledge Machine and ECLiPSe support backward chaining within their inference engines.