導出原理
読み方：どうしゅつげんり
【英】：resolution principle
【英】：resolution principle
ロビンソン (J.A. Robinson) により1965年に提案された定理証明技法の1つである. 節形式で表現された論理式に対し, 導出規則と呼ばれる1つの推論規則を適用することで定理証明を行うもので, 導出規則のみを用いた定理証明は完全であることが証明されている. 完全な推論規則で, かつ, 単純であるため, 計算機上での実現性に非常に優れている. その後, 支持集合導出, 入力導出, 意味導出など様々な効率的証明戦略が提案されている.
「OR事典」の他の用語
| 近似・知能・感覚的手法： | 可変近傍法 多スタート局所探索 定性推論 導出原理 局所探索法 支配関係に基づくラフ集合 最大カット問題 |
導出原理
(resolution principle から転送)
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/10/21 06:25 UTC 版)
導出原理（どうしゅつげんり、英: resolution principle）とは、ジョン・アラン・ロビンソンにより1965年に提案された[1]原理または手法を言う。
- ^ J. Alan Robinson, A Machine-Oriented Logic Based on the Resolution Principle. JACM, Volume 12, Issue 1, pp. 23–41. 1965.
- ^ Buss, Samuel R., "On Herbrand's Theorem", in Maurice, Daniel; Leivant, Raphaël, Logic and Computational Complexity, Lecture Notes in Computer Science, Springer-Verlag, pp. 195–209. 1995.
- ^ a b Martin Davis. The Early History of Automated Deduction. in Handbook of Automated Reasoning, Volume I, Alan J.A. Robinson and Andrei Voronkov(ed), 2001. ISBN 9780444829498
- ^ Wolfgang Bibel. Early History and Perspectives of Automated Deduction. in Advances in Artificial Intelligence, Lecture Notes in Computer Science, Springer-Verlag Berlin, 2007. ISBN 9783540745648
- ^ Lawrence Wos, G.A. Robinson, D.F. Carson. Efficiency and Completeness of the Set of Support Strategy in Theorem Proving. Journal of the ACM, Volume12, Issue 4, pp.536-541. 1965.
- ^ James Slagle. Automatic Theorem Proving With Renamable and Semantic Resolution. Journal of the ACM, Volume14, Issue 4, pp.687-697. 1967.
[続きの解説]
- resolution principleのページへのリンク
