Бойєр і Мур: індукція без підказок людини
У серпні 1973 року на IJCAI в Стенфорді Роберт Бойєр і Джей Стротер Мур з Единбурзького університету описали програму, що сама доводить теореми про рекурсивні функції LISP математичною індукцією: серед доведеного — що REVERSE є оберненою до самої себе і що певна програма сортування правильна. На ICL 4130 кожна теорема коштувала в середньому 8 секунд.
Чому це важливо
Машина сама будувала формулу індукції для функцій, яких раніше не бачила: за статтею, від користувача потрібні лише визначення функцій, і більше нічого. Доведення правильності програми, як-от сортування, стало задачею для машини без людської підказки.
Програма бере на вхід вираз LISP, запускає його інтерпретатором і з того, як інтерпретатор не справляється, виводить формулу індукції; до неї додано прості правила переписування LISP і евристику узагальнення теореми. Від користувача, за статтею, потрібні лише визначення функцій. Середні 8 секунд на теорему виміряно на ICL 4130 мовою POP-2. Додаток B перелічує доведені теореми. Чого запис не стверджує: скільки теорем у додатку — стаття їх не рахує.