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

ナビゲーションに移動 検索に移動
曖昧さ回避する必然性がないので改名提案を単純に「導出原理」と提案する。
(曖昧さ回避する必然性がないので改名提案を単純に「導出原理」と提案する。)
{{改名提案|導出原理 (数理論理学)|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]]などの[[論理プログラミング]]言語の基礎となった。

案内メニュー