Logic Theorist

Програма Ньюелла, Шоу і Саймона доводила теореми з «Principia Mathematica», шукаючи не всі виводи, а правдоподібні.

Чому це важливо

Перша програма, що виконувала роботу, яку доти вважали суто людською, і робила це евристичним пошуком, а не перебором.

Logic Theorist довела 38 із перших 52 теорем другого розділу «Principia Mathematica», а для теореми 2.85 знайшла коротше доведення, ніж у Вайтхеда і Расселла. Journal of Symbolic Logic відхилив статтю зі співавторством програми. Для роботи Ньюелл і Шоу створили мову обробки списків IPL.

Відомості про подію

Дата події

серпень 1956 р. · Приблизна дата

Дата на часовій осі

Дата події

Перевірка

Джерела зібрано автоматично · 17 вересня 2026 р.

Лінії

ID

evt-0082

Перші машинні доведення отримано у серпні 1956 року на JOHNNIAC; частина результатів, зокрема коротше доведення теореми 2.85, належить до запусків кінця 1956 - початку 1957 років. Місяць приблизний.

Джерела

першоджерело The logic theory machine: A complex information processing system
IRE Transactions on Information Theory · Опубліковано вересень 1956 р.
вторинне The Quest for Artificial Intelligence (Nilsson), section 5.1 The Logic Theorist and Heuristic Search
Nils J. Nilsson, Cambridge University Press (author's Stanford copy) · Опубліковано 2010
архівна копія The Logic Theory Machine - A Complex Information Processing System (Feigenbaum papers, Stanford Special Collections)
Stanford University Libraries · Опубліковано 12 липня 1956 р.

Пов’язані події

Раніше

Спирається на Шахова машина Ньюелла 1955
Пошук, керований цілями, переніс з шахової задачі на доведення теорем.
- The logic theory machine: A complex information processing system · IRE Transactions on Information Theory

У той самий час

Пов’язано Дартмутський літній семінар 1956
Програму показували учасникам Дартмутського семінару того самого літа.

Пізніше

Спирається на Шахова програма з цілей, а не з чисел 1958посилається на цей запис
Стаття прямо пов'язує шахи з програмами, що знаходять докази теорем у символічній логіці: обидві задачі — міркування з евристиками в просторі, що росте експоненційно.
- A. Newell, J. C. Shaw, H. A. Simon, «Chess-Playing Programs and the Problem of Complexity», RAND Corporation paper P-1319, 4 September 1958 («To be published in the IBM Journal of Research and Development») · RAND Corporation (copy: bitsavers.org through the Internet Archive)
Спирається на Універсальний розв'язувач задач 1959посилається на цей запис
GPS відокремлює стратегію пошуку від предметної області, відпрацьовану в Logic Theorist.
- Report on a General Problem-Solving Program · RAND Corporation
Протиставляє Хао Ван: «Principia» за хвилини 1960посилається на цей запис
Ван прямо зіставляє свої програми з Logic Theorist: 52 теореми, які обрали Ньюелл, Шоу й Саймон, його програма довела менш ніж за 5 хвилин, і він протиставляє повні алгоритми їхнім евристикам.
- Toward Mechanical Mathematics (Hao Wang), IBM Journal of Research and Development 4(1), 2-22 · IBM (scan on bitsavers.org)
Пов’язано Комп'ютери і мислення 1963посилається на цей запис
Збірник передрукував ключові статті Ньюелла, Шоу і Саймона.
Пов’язано Automath: мова, у якій машина перевіряє математику 1968посилається на цей запис
Logic Theorist шукав доведення сам; Automath пропонує інше завдання — машина перевіряє кожен рядок доведення, яке написала людина.