導出原理

【どうしゅつげんり (resolution principle)】

ロビンソン (J.A. Robinson) により1965年に提案された定理証明技法の1つである. 節形式で表現された論理式に対し, 導出規則と呼ばれる1つの推論規則を適用することで定理証明を行うもので, 導出規則のみを用いた定理証明は完全であることが証明されている. 完全な推論規則で, かつ, 単純であるため, 計算機上での実現性に非常に優れている. その後, 支持集合導出, 入力導出, 意味導出など様々な効率的証明戦略が提案されている.