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

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

Сторінок статті 1970 року, де описано сам алгоритм очевидності, не прочитано: відкриті лише дві перші сторінки англійського перекладу (Cybernetics, т. 6, № 2, с. 17–27), і вони про теорію автоматів. Зміст програми взято з ретроспектив учасників: Лялецького й Вершиніна (2010), Лялецького (2020), де наведено цитату Глушкова 1970 року в українському перекладі — постійне вдосконалення алгоритму очевидності рано чи пізно зробить усі відомі теореми очевидними для машини. Дослівні уривки статті 1970 року наводить огляд Летичевського, Лялецького й Мороховець (2013): найкращою модельною задачею для моделювання логічного мислення Глушков називає автоматизацію доведень теорем у математиці; центр ваги роботи треба змістити від «універсальних» програм-доводжувачів до систем програмування, які дають швидко запрограмувати пошук доведення навіть однієї важкої теореми й працювати в реальному часі з математиком, що її доводить; у початковому вигляді алгоритм очевидності можна обмежити найпростішими функціями виведення в численні висловлювань, доповненими перебором дерева конструкцій на невелику кількість кроків. За тими самими ретроспективами: перша група з автоматизації доведень склалася в Інституті кібернетики 1962 року, і початок вони ведуть від статті Глушкова того року, яку покажчик його праць 1975 року записує в київському журналі «Радянська школа», 1962, № 2, с. 87–91; першу публічну демонстрацію російськомовної системи зроблено на симпозіумі в Києві 28–30 листопада 1978 року; назву «Система автоматизації доведень» (САД) Глушков дав 1980 року; англомовну SAD показали на конференції CADE-21 у Бремені в липні 2007 року. Що про саму статтю 1970 року відомо з бібліографічних записів і одного спогаду (тексту вони не дають). Оригінал: «Кібернетика», 1970, № 2, с. 3–13, перша стаття номера за змістом журналу (наступна — зі с. 14); переклад — с. 17–27. Відбиток на одинадцять сторінок є в Національній бібліотеці України імені Вернадського в Києві. Стаття з такою самою назвою на 31 сторінку стоїть у покажчику праць Глушкова 1975 року під 1968 роком, у збірнику «Теорія автоматів і методи формалізованого синтезу обчислювальних машин і систем», № 6, виданому видавництвом Інституту кібернетики; як вона співвідноситься з журнальним текстом, у прочитаному не сказано. Вираз «алгоритм очевидності» є вже в назвах двох газетних статей 1969 року (однієї від 17 липня), яких не знайдено. У спогаді Н. М. Міщенко (2013, с. 173) стаття присвячена загальному формулюванню проблеми навчання мови на основі досліджень самого Глушкова (йдеться про навчання машини розпізнавати осмислені речення); виноска на тій самій сторінці посилається на збірник 1968 року; про алгоритм очевидності там не сказано. Стаття 1962 року. Покажчик 1975 року й список праць у віртуальному музеї Глушкова подають її однаково: «Радянська школа», 1962, № 2, с. 87–91, без місяця, під російською назвою; ретроспектива 2010 року позначає статтю як російськомовну. Том журналу за 1962 рік у HathiTrust показує лише номери сторінок і кількість збігів слова, без тексту. Пошук, серед інших місць, знаходить прізвище Глушкова й слова назви українською («Розумні», «розумова діяльність людини») на с. 2 і с. 87 номера, що за порядком сканів є другим, — ймовірно, на сторінці змісту й на першій сторінці статті; як це узгодити з російською назвою, не ясно. Про зміст пошук майже нічого не каже: на с. 90 слово «теорем» стоїть тричі, «теореми» раз, а «доведення» на с. 87–91 і «алгоритм» у всьому томі не знайдено (шукали цілі слова). За ретроспективою 2010 року стаття розбирала кілька простих доведень у теорії груп; огляд 2013 року посилається на неї для досліджень з автоматизації пошуку доведень, які 1962 року почалися саме в теорії груп; прочитане цього ні підтверджує, ні спростовує. Чого запис не стверджує: що статті 1970 і 1962 років прочитано. Слова першої взято з цитат в огляді 2013 року; друга відома за бібліографічними записами та місцями прізвища й слів назви в томі журналу, без тексту, місяця й назви цілим рядком; видання 1968 року й газетні статті 1969 року відомі лише за назвами. Що журнальний текст 1970 року збігається з виданням 1968 року або скорочує його, і що стаття присвячена лише алгоритму очевидності: ретроспективи описують у ній автоматизацію доведень, спогад — навчання мови. Що в статті 1970 року вперше вжито «автоматизоване доведення» замість «автоматичне», як пише ретроспектива 2010 року: у цитатах справді стоїть «автоматизація доведень», але першості вжитку вони не показують. Що вираз «алгоритм очевидності» вперше надруковано 1970 року, як подає сайт проєкту: він є вже в назвах статей 1969 року, а що в них, невідомо. Що стаття 1962 року говорить про доведення теорем чи їх автоматизацію, а тим більше розбирає доведення в теорії груп: слово «теорем» на с. 90 цього не показує. Будь-яких вимірів системи САД.