| dbpprop:abstract
|
- Backward chaining (or backward reasoning) is an inference method used in automated theorem provers, 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. Backward chaining is implemented in logic programming by SLD resolution. Both rules are based on the modus ponens inference rule. Backward chaining starts with a list of goals and works backwards from the consequent to the antecedent to see if there is data available that will support any of these consequents. An inference engine using backward chaining would search the inference rules until it finds one which has a consequent (Then clause) that matches a desired goal. If the antecedent (If clause) of that rule is not known to be true, then it is added to the list of goals (in order for one's goal to be confirmed one must also provide data that confirms this new rule). For example, suppose that the goal is to conclude the color of my pet Fritz, given that he croaks and eats flies, and that the rule base contains the following four rules: If X croaks and eats flies – Then X is a frog If X chirps and sings – Then X is a canary If X is a frog – Then X is green If X is a canary – Then X is yellow This rule base would be searched and the third and fourth rules would be selected, because their consequents (Then Fritz is green, Then Fritz is yellow) match the goal (to determine Fritz's color). It is not yet known that Fritz is a frog, so both the antecedents (If Fritz is a frog, If Fritz is a canary) are added to the goal list. The rule base is again searched and this time the first two rules are selected, because their consequents (Then X is a frog, Then X is a canary) match the new goals that were just added to the list. The antecedent (If Fritz croaks and eats flies) is known to be true and therefore it can be concluded that Fritz is a frog, and not a canary. The goal of determining Fritz's color is now achieved (Fritz is green if he is a frog, and yellow if he is a canary, but he is a frog since he croaks and eats flies; therefore, Fritz is green). Note that the goals always match the consequents of implications, even though they are searched first; thus, the inference rule which is used is modus ponens, not modus tollens. 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.
- Eine Rückwärtsverkettung bezeichnet in der Logik eine Inferenz- bzw. Schlussfolgerungs-Strategie der Form: wenn Bedingung, dann Faktum Das Gegenmodell ist die Vorwärtsverkettung. Bedeutung haben diese Verkettungen beispielsweise im Bereich der künstlichen Intelligenz für Inferenzmaschinen. Ebenso wie die Vorwärtsverkettung basiert die Rückwärtsverkettung auf einer transitiven Verknüpfung von Regeln. Man geht dabei jedoch vom Zielobjekt aus und prüft nur die Regeln, die das Ziel in der Konklusion haben. Falls der Wert eines Objektes in der Prämisse einer solchen Regel unbekannt ist, wird versucht, diesen aus anderen Regeln herzuleiten. Gelingt dieses nicht, so wird der Wert schließlich vom Benutzer erfragt. Man nennt dieses Verfahren auch zielorientierte Inferenz.
- 後向き連鎖（Backward chaining）は、（人工知能において）推論規則を使う時の二種類の主要な推論手法のひとつである。もう一方は前向き連鎖である。 後向き連鎖はゴール(または仮説)のリストによって起動して後向きに作業し、いずれかのゴールが正しいことを補強するのに使用可能なデータがあるかどうかを確かめる後向き連鎖を使う。 推論エンジンは推論規則を検索し、帰結部（THEN節）がゴールにマッチする規則を探す。その規則の条件部（IF節）が真かどうか不明な場合、それもゴールのリストに追加され（つまり、仮説の一部とされ）、それを立証するデータをさらに提供しなければならない。 例として、以下の二つの規則を持つルールベースと、フリッツは蛙であるというゴール（仮説）と、それが弾むというデータがあるとする。 IF節：フリッツははずむ — THEN節：フリッツは緑色である IF節：フリッツは緑色である — THEN節：フリッツは蛙である このルールベースが検索されると、帰結部（THEN節）がゴール（フリッツは蛙である）とマッチしている規則(2)が選択される。フリッツが緑色かどうかは不明なので、条件部（IF節）はゴールのリストに追加される（フリッツが蛙であるためには、緑色でなければならない）。ルールベースは再び検索されて、THEN節がリストに追加された新しいゴール（フリッツは緑色である）とマッチする規則(1)が選択される。その規則の条件部（フリッツは弾む）が真であることは予め分かっているので、フリッツは蛙であると結論付けられる（フリッツは弾むので緑色であるに違いない、フリッツが緑色なので蛙に違いない）。 ゴールのリストが、どの規則が選ばれて使われるかを決定するので、この方法はゴール駆動型と呼ばれる。一方、前向き連鎖による推論はデータ駆動型と呼ばれる。このようなボトムアップ型アプローチは、しばしばエキスパートシステムで使用される。 プログラミング言語Prologは後向き連鎖をサポートしている。
- Wnioskowanie w tył - działanie regresywne (Modus Tollendo Tollens). Polega na tym, że wychodzimy od tego, co chcemy udowodnić i idziemy w kierunku aksjomatów. Czyli żeby udowodnić <math>X</math>, udowadniamy <math>Y \supset X</math>, <math>Z \supset Y</math> i tak dalej, aż dojdziemy do aksjomatów. Oczywiście nie wiemy czy idziemy w dobrym kierunku, ale ponieważ aksjomaty znamy z góry, możemy zaplanować algorytm tak, żeby raczej zachowywał odpowiedni kierunek. Jest to duża przewaga nad wnioskowaniem w przód, jako że w tamtym przypadku znajomość aksjomatów okazuje się niewystarczająca do skutecznej optymalizacji. Wnioskowanie w tył często stosuje się w systemach ekspertowych do automatycznego dowodzenia twierdzeń.
|
| rdfs:comment
|
- Backward chaining (or backward reasoning) is an inference method used in automated theorem provers, 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. Backward chaining is implemented in logic programming by SLD resolution. Both rules are based on the modus ponens inference rule.
- Eine Rückwärtsverkettung bezeichnet in der Logik eine Inferenz- bzw. Schlussfolgerungs-Strategie der Form: wenn Bedingung, dann Faktum Das Gegenmodell ist die Vorwärtsverkettung. Bedeutung haben diese Verkettungen beispielsweise im Bereich der künstlichen Intelligenz für Inferenzmaschinen. Ebenso wie die Vorwärtsverkettung basiert die Rückwärtsverkettung auf einer transitiven Verknüpfung von Regeln.
- Wnioskowanie w tył - działanie regresywne (Modus Tollendo Tollens). Polega na tym, że wychodzimy od tego, co chcemy udowodnić i idziemy w kierunku aksjomatów. Czyli żeby udowodnić <math>X</math>, udowadniamy <math>Y \supset X</math>, <math>Z \supset Y</math> i tak dalej, aż dojdziemy do aksjomatów.
|
![[RDF Data]](/statics/sw-cube.png)
