Loading article…
モデル消去法は、ドナルド・W・ラブランドが発明した一対の証明手順に付けられた名前で、最初のものは1968年にJournal of the ACMに掲載されました。その主な目的は、自動定理証明を実行することですが、より一般的な選言論理プログラミングを含む論理プログラミングに簡単に拡張できます。
モデル消去は、タブロー法の特性も持ちながら、解決と密接に関連しています。これは、 Prolog論理プログラミング言語で使用されるSLD 解決手順の元祖です。
解決定理証明器への注目と進歩によっていくぶん影を潜めているものの、モデル消去法は研究者やソフトウェア開発者の注目を集め続けています。現在、モデル消去法に基づく定理証明器がいくつか開発中です。
参考文献
- Loveland, DW (1968) モデル消去による機械的定理証明 Journal of the ACM, 15, 236—251.