П'ятдесят років тому, в 1970 році, академік В. М. Глушков опублікував статтю, в якій разом із обговоренням деяких проблем штучного інтелекту сформулював науково-дослідницьку програму під назвою Алгоритм очевидності, що описує його бачення проблеми комп'ютерної підтримки людської діяльності в пошуку ним доведення теорем. В. М. Глушков запропонував зосередити увагу на побудові системи автоматизації пошуку доведень теорем, виконуючи для цього одночасні дослідження у створенні формальних природних мов для запису математичних текстів у звичній для людини формі, побудуванні процедури пошуку доведень на основі машинного поняття очевидності комп'ютерного шагу доведення, яке еволюційно розвивається, використанні знань, заздалегідь відомих або отриманих системою за час її роботи та надання користувачеві інтерфейсних можливостей надати допомогу системі у процесі пошуку нею доведення. З моменту опублікування АО було здійснено дві серйозні спроби реалізації цієї програми. Перша призвела до появи в 1978 році російськомовної системи автоматизації пошуку доведень САД, а друга - до появи в 2002 році її англомовної модифікації під назвою System for Automated Deduction (SAD). Якщо розробку та пробну експлуатацію системи САД було припинено в 1992 році після вилучення з експлуатації ЄС ЕОМ, на яких їх було реалізовано, система SAD, розміщена на веб-сайті nevidal org, зараз все ще доступна в онлайновому режимі. Тобто у поточний час можна проводити з нею різноманітні експерименти та вирішувати за її допомогою різні задачі, які вимагають точних математичних міркувань. Ця робота присвячена стислому хронологічному опису досліджень із реалізації програми АО за весь період її існування та висвітленню як особливостей систем САД та SAD, так і їх загальних рис та відмінностей. Наведено деякі можливі шляхи подальшого розвитку системи SAD.

• Лялецький Олександр Вадимович (технічні науки)

  Якщо, ви не знайшли інформацію про автора(ів) публікації, маєте бажання виправити або відобразити більш докладну інформацію про науковців України запрошуємо заповнити "Анкету науковця"