Бойєр і Мур: індукція без підказок людини

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

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