Глушков: програма «алгоритм очевидності»

У «Кібернетиці» 1970 року (№ 2, березень–квітень) Віктор Глушков опублікував статтю про проблеми теорії автоматів і штучного інтелекту, у якій, за ретроспективами його учнів, сформулював програму «алгоритм очевидності»: формальна мова, близька до мови математичних статей, пошук доведення на основі машинного поняття очевидного кроку, що зростає з досвідом системи, і допомога людини в пошуку.

Сторінок статті 1970 року, де описано сам алгоритм очевидності, не прочитано: відкриті лише дві перші сторінки англійського перекладу (Cybernetics, т. 6, № 2, с. 17–27), і вони про теорію автоматів. Зміст програми взято з ретроспектив учасників: Лялецького й Вершиніна (2010), Лялецького (2020), де наведено цитату Глушкова 1970 року в українському перекладі — постійне вдосконалення алгоритму очевидності рано чи пізно зробить усі відомі теореми очевидними для машини. За тими самими ретроспективами: перша група з автоматизації доведень склалася в Інституті кібернетики 1962 року; першу публічну демонстрацію російськомовної системи зроблено на симпозіумі в Києві 28–30 листопада 1978 року; назву «Система автоматизації доведень» (САД) Глушков дав 1980 року; англомовну SAD показали на конференції CADE-21 у Бремені в липні 2007 року. Чого запис не стверджує: точних формулювань статті 1970 року; що в ній уперше вжито вираз «автоматизоване доведення» замість «автоматичне», як пише ретроспектива 2010 року; будь-яких вимірів системи САД.