Boyer-Moore Theorem Prover (Nqthm)
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2019/11/13 06:25 UTC 版)
「自動推論」の記事における「Boyer-Moore Theorem Prover (Nqthm)」の解説
LISPで構築された完全自動の定理証明機。ジョン・マッカーシーと Woody Bledsoe の影響を受けた設計である。1971年、スコットランドのエジンバラで開発が始まった。次のような特徴がある。
※この「Boyer-Moore Theorem Prover (Nqthm)」の解説は、「自動推論」の解説の一部です。
「Boyer-Moore Theorem Prover (Nqthm)」を含む「自動推論」の記事については、「自動推論」の概要を参照ください。
- Boyer-Moore Theorem Proverのページへのリンク