Editing Backward chaining (section)

{{Short description|Method of forming inferences}}
{{distinguish|Backward chaining (applied behavior analysis)|Back-chaining}}
'''Backward chaining''' (or '''backward reasoning''') is an [[inference]] method described colloquially as working backward from the goal. It is used in [[automated theorem prover]]s, [[inference engine]]s, [[proof assistant]]s, and other [[artificial intelligence]] applications.<ref>{{cite book|last=Feigenbaum|first=Edward|title=The Rise of the Expert Company|url=https://archive.org/details/riseofexpertcomp00feig|url-access=registration|year=1988|publisher=Times Books|isbn=0-8129-1731-6|page=[https://archive.org/details/riseofexpertcomp00feig/page/317 317]}}</ref>

In [[game theory]], researchers apply it to (simpler) [[subgame]]s 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 endgame]]s 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 rule]]s and [[Logical consequence|logical implications]] – the other is [[forward chaining]]. Backward chaining systems usually employ a [[depth-first search]] strategy, e.g. [[Prolog]].<ref name="CheinMugnier2009">{{cite book|author1=Michel Chein|author2=Marie-Laure Mugnier|title=Graph-based knowledge representation: computational foundations of conceptual graphs|url=https://books.google.com/books?id=iz3y6WK2EMEC&pg=PA297|year=2009|publisher=Springer|isbn=978-1-84800-285-2|page=297}}</ref>