「導出原理」の版間の差分

冒頭の説明文を項目名に合わせて書き直した。
m (I.hidekazu がページ「導出」を「導出原理」に移動しました: 一般名詞「導出」に対して、ロビンソンの導出原理に基づく手法をその内容としているため。)
(冒頭の説明文を項目名に合わせて書き直した。)
'''導出'''(どうしゅつ、{{lang-en-short|''resolution''}})とは、[[数理論理学]]における1つの[[演繹]]方法で、三段論法を一般化した導出規則と呼ばれるただ1つの推論規則を用いる。[[命題論理]]、[[述語論理]]のいずれにも使う事ができ、導出を繰り返すことで証明したい論理式の否定から空節が導かれることにより証明を行う。導出規則と[[単一化]]に基づく'''導出原理'''(どうしゅつげんり、{{lang-en-short|''resolution principle''}}){{仮リンク|ジョン・アラン・ロビンソン|en|John Alan Robinson}}により1965年に提案され<ref name=Robinson1965>J. Alan Robinson, ''A Machine-Oriented Logic Based on the Resolution Principle''. JACM, Volume 12, Issue 1, pp. 23–41. 1965.</ref>原理または手法を言う。
{{改名提案|導出原理|t=ノート:導出|date=2013年10月}}
 
'''導出'''(どうしゅつ、{{lang-en-short|''resolution''}})とは、[[数理論理学]]における1つの[[演繹]]方法で、三段論法を一般化した導出規則と呼ばれるただ1つの推論規則を用いる。[[命題論理]]、[[述語論理]]のいずれにも使う事ができ、導出を繰り返すことで証明したい論理式の否定から空節が導かれることにより証明を行う。導出規則と[[単一化]]に基づく'''導出原理'''(どうしゅつげんり、{{lang-en-short|''resolution principle''}})は{{仮リンク|ジョン・アラン・ロビンソン|en|John Alan Robinson}}により1965年に提案され<ref name=Robinson1965>J. Alan Robinson, ''A Machine-Oriented Logic Based on the Resolution Principle''. JACM, Volume 12, Issue 1, pp. 23–41. 1965.</ref>、
導出原理を元とする導出の手法は、その後の[[定理自動証明]]に大きな影響を与え、また[[Prolog]]などの[[論理プログラミング]]言語の基礎となった。
 
== 背景 ==