Дослідження · серпень 1956 р.
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 років. Місяць приблизний.
Записи, що посилаються на цей
- Спирається на Універсальний розв'язувач задач
GPS відокремлює стратегію пошуку від предметної області, відпрацьовану в Logic Theorist.
Report on a General Problem-Solving Program - Пов’язано Комп'ютери і мислення
Збірник передрукував ключові статті Ньюелла, Шоу і Саймона.
- Протиставляє Хао Ван: «Principia» за хвилини
Ван прямо зіставляє свої програми з Logic Theorist: 52 теореми, які обрали Ньюелл, Шоу й Саймон, його програма довела менш ніж за 5 хвилин, і він протиставляє повні алгоритми їхнім евристикам.
Toward Mechanical Mathematics (Hao Wang), IBM Journal of Research and Development 4(1), 2-22 - Пов’язано Automath: мова, у якій машина перевіряє математику
Logic Theorist шукав доведення сам; Automath пропонує інше завдання — машина перевіряє кожен рядок доведення, яке написала людина.