Backward chaining

It is used in automated theorem provers, inference engines, proof assistants, and other artificial intelligence applications.

It is one of the two most commonly used methods of reasoning with inference rules and logical implications – the other is forward chaining.

Since this goal is a conjunction of two statements, the inference engine breaks it into two sub-goals, both of which must be proven: 4.

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.

Programming languages such as Prolog, Knowledge Machine and ECLiPSe support backward chaining within their inference engines.