Logic Theorist は、1955年から1956年にかけてアレン・ニューウェル、ハーバート・サイモン、J・C・ショーが開発したコンピュータプログラム。人間の問題解決能力を真似するよう意図的に設計された世界初のプログラムであり、「世界初の人工知能プログラム」と称された[注 1]。ホワイトヘッドとラッセルの『プリンキピア・マテマティカ』の冒頭の52の定理のうち38を証明してみせ、一部については新たなもっと洗練された証明方法を発見している[2]。
歴史

1955年、ニューウェルとサイモンが Logic Theorist の開発を始めたころ、人工知能はまだ学問分野として確立していなかった。「人工知能 (artificial intelligence)」という用語ができたのも翌年の夏のことである[注 2]。

ハーバート・サイモンは政治学者で、これ以前に官僚制についての研究や限定合理性の理論構築で知られていた（限定合理性の研究でノーベル賞を受賞）。企業組織の研究と人工知能の研究はかけ離れているように見えるが、どちらも人間の問題解決能力と判断力の性質への洞察を必要とする。サイモンは1950年代初めにランド研究所でコンサルタントとして働いており、普通の文字や記号を使ってプリンターで地図を描いたのを見ている。そこから彼は記号を処理できる機械なら意思決定をシミュレートできるだろうし、人間の思考過程すらシミュレートできるのではないかと考えた[4][5]。

その地図をプリントアウトするプログラムを書いたのがランド研究所で物流と組織論を研究していた科学者アレン・ニューウェルだった。1954年にオリバー・セルフリッジがランド研究所を訪れてパターンマッチについてのプレゼンを行ったのが、ニューウェルにとっての転機となった。そのプレゼンを見たニューウェルは、単純なプログラム可能なユニット群の相互作用によって人間の知的活動を含む複雑な活動を実現できると直観した。後に彼は「ある日の午後、突然ひらめいた」と述べている[1][6]。それは科学的閃きが訪れる滅多にない瞬間だった。

「それが新たな道であり、私にはそれを辿っていくべきだという明晰な感覚があった。そのような感覚が訪れたことはほとんどない。私は慎重な性質で、普通はひらめきで決断しないが、そのときは違っていた」[7]

ニューウェルとサイモンは、機械に考えることを学ばせる可能性について話し合った。彼らの最初のプロジェクトは、バートランド・ラッセルとアルフレッド・ノース・ホワイトヘッドの『プリンキピア・マテマティカ』で使われているような数学的定理の証明をするプログラムの開発である。ランド研究所にいたプログラマのJ・C・ショーの助けを得て、そのプログラムの開発を行った。ニューウェルは、「3人の中で本物の計算機科学者はショーだけだった」と述べている[8]。

最初のバージョンは人間によるシミュレートだった。サイモンによればプログラムをカードに書いたという。

1956年1月、我々は私の妻と3人の子、さらには大学院生を何人か集めた。そして各人にカードを一枚ずつ渡し、コンピュータプログラムのコンポーネントの役目をしてもらった。…いわば、自然を擬似している技術を再び自然で擬似するという構図があった。[9]

そして、そのプログラムが有能な数学者のように定理を証明できると示すことに成功した。その後ショーがそのプログラムをランド研究所の持つコンピュータ上で動作させることができた。

1956年夏、ジョン・マッカーシー、マービン・ミンスキー。クロード・シャノン、ナサニエル・ロチェスターがいわゆる「人工知能」についての会議（ダートマス会議）を開催した（人工知能という呼称はマッカーシーがこのときに考案した）。ニューウェルとサイモンはその会議で Logic Theorist を意気込んで公開したが、反応が微妙だったため若干驚いた。パメラ・マコーダック（英語版）は「ニューウェルとサイモンは長期的観点で重要なことを達成したと感じていたが、記録によれば誰もそれを褒め称えなかった」と記している[10]。サイモンは後に「我々はたぶん非常に横柄だった」と述べ[11]、さらに次のように続けている。

彼らは我々から何か聞きたかったわけではなく、もちろん我々も彼らから何か聞きたいわけではなかった。我々には彼らに見せるものがあった！…我々は彼らが後に作ろうとしていたものの実例を既に完成させており、彼らは我々にあまり関心がなかったという点で、それは皮肉な結果となった。[12]

間もなく Logic Theorist は『プリンキピア・マテマティカ』の第2章にある52の定理のうち38を証明してみせた。定理 2.58（二等辺三角形の定理）の証明は、ラッセルとホワイトヘッドが同書に掲載したものより洗練されていた。サイモンはその証明をラッセル自身に見せており、ラッセルは喜んだという[2]。彼らは Logic Theorist による新たな証明を The Journal of Symbolic Logic 誌に送ったが、初等数学の定理の新たな証明は注目に値しないとして受理されなかった。どうも、執筆者の1人がコンピュータプログラムだという点を見過ごされたようである[13][2]。

ニューウェルとサイモンはその後も協力関係が続き、カーネギーメロン大学に人工知能研究所を創設し、その後も一連の人工知能プログラム（GPS、Soar）を開発し、理論（認知の統一理論）を提唱した。
その後の人工知能への影響

Logic Theorist はその後のAI研究の中核となるいくつかの概念を生み出した。
探索としての推論
Logic Theorist は探索木を探査する。その根は初期の仮説であり、それぞれの分枝は論理規則に基づいた演繹を表している。最終的にどこかの葉ノードがゴール、すなわちプログラムが証明しようとしている命題である。ゴールまでの枝の連なりが証明の流れとなっている。証明の個々の文は論理規則から演繹されたもので、それによって仮説から証明すべき命題へとたどり着く。
ヒューリスティクス
ニューウェルとサイモンは、単純に論理規則を適用していくと探索木が指数的爆発を起こすことを発見した。そこで経験則を使って正解にたどり着きそうにない枝を判定して枝刈りをし、木が大きくなりすぎないようにした。彼らはポーヤ・ジェルジの証明に関する古典的著作『いかにして問題をとくか』で使われている用語を採用し、この場当たり的な規則を「ヒューリスティクス」と呼んだ。ニューウェルはスタンフォード大学でポーヤのコースを受講していた[14]。ヒューリスティクスは人工知能研究で重要な分野となり、特に指数的に探索空間が広がっていくのを防ぐ手段として重要となっている。
リスト処理
Logic Theorist をコンピュータ上で実装するため、彼らはプログラミング言語 IPL を開発した。その記号的リスト処理はジョン・マッカーシーが後に開発したLISPでも基盤として採用され、LISPは今でもAI研究で重要な言語となっている[15][16]。
哲学的意味

パメラ・マコーダックは Logic Theorist について「かつては知的で創造的で人間にしかなしえないとされていたことを機械でもできることを証明した」と評している[2]。そのため、人工知能の歴史の中でも重要な位置を占めており、知性一般についての我々の理解という意味でも重要である。

サイモンは1956年1月の大学院生への講義で「クリスマスの間、ニューウェルと私は思考する機械を発明した」と述べ[17][18]、次のように記している。