主な証明システム
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2019/11/13 06:25 UTC 版)
Boyer-Moore Theorem Prover (Nqthm) LISPで構築された完全自動の定理証明機。ジョン・マッカーシーと Woody Bledsoe の影響を受けた設計である。1971年、スコットランドのエジンバラで開発が始まった。次のような特徴がある。LISPにより論理を構築 すべてを再帰関数で定義することを基本としている。 「記号評価」と書き換えを多用。 記号評価の失敗に基づいた帰納的ヒューリスティックを使用 HOL Light OCamlで書かれており、論理的基盤が単純かつ明快になるよう設計され、実装もきれいである。古典的高階論理の証明を支援する。 Coq フランスで開発された証明支援システムで、仕様記述から実行可能なプログラムを自動生成できる（生成するソースコードはOCamlまたはHaskell）。仕様記述や証明の記述に使われる言語は Calculus of Inductive Constructions (CIC) と呼ばれている。
※この「主な証明システム」の解説は、「自動推論」の解説の一部です。
「主な証明システム」を含む「自動推論」の記事については、「自動推論」の概要を参照ください。
ウィキペディア小見出し辞書の「主な証明システム」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- 主な証明システムのページへのリンク
