Хао Ван: «Principia» за хвилини
У січні 1960 року Хао Ван описав в IBM Journal програми для IBM 704, що довели понад 200 теорем числення висловлень із перших п'яти розділів «Principia Mathematica» менш ніж за 3 хвилини чистого часу, а з предикатної частини — 139 із 158 теорем. Програми він написав улітку 1958 року в лабораторії IBM у Покіпсі.
Чому це важливо
Розділи «Principia», які Logic Theorist долав евристиками й лише частково, повна алгоритмічна процедура пройшла цілком за хвилини. Ван сам ставить це проти евристичного підходу Ньюелла, Шоу й Саймона: машинне доведення з цього часу має два шляхи — евристичний пошук і повні методи.
Увесь прогін числення висловлень тривав близько 37 хвилин, але 12/13 часу пішло на введення й друк. 52 теореми, обрані Ньюеллом, Шоу й Саймоном, програма довела менш ніж за 5 хвилин. Серед теорем *9–*13 числення предикатів із рівністю, разом 158, програма III у тому вигляді довела 139; у примітці при коректурі 10 листопада 1959 року Ван повідомляє, що покращена програма довела всі 158 приблизно за чотири хвилини. Чого запис не стверджує: де працював Ван на час публікації — підпис статті належності не має; робота, за самим текстом, виконана в лабораторії IBM.