ロジック・セオリスト

ロジック・セオリストとは、1956年にニューウェルとサイモンらが開発した、世界初の AI プログラムとされる定理証明システムです。

数学の論理学の教科書に載っている定理を、コンピュータが自ら証明することに成功しました。記号を操作して論理を組み立てる、典型的な推論型 AI の先駆けです。

ダートマス会議でも紹介され、「機械が考えられる」ことを実例で示した点で、AI 史上の記念碑的なプログラムとされています。