Evidence algorithm and SAD systems: Past and possible future

Abstract

The paper is devoted to the Evidence Algorithm programme on automated reasoning initiated by Academician Glushkov in 1970 and found its expression in the form of the Russian-language and English-language SAD systems intended for automated deduction. Some of their characteristic peculiarities and features are described. Examples demonstrating the possibility of their use for solving mathematical and common problems that require deductive constructions are supplied. Possible ways of the further development of the English-language SAD system are given.

Роботу присвячено програмі "Алгоритм Очевидності", що була ініційована академіком В. М. Глушковим у 1970 р. і знайшла своє втілення у вигляді російськомовної та англомовної систем SAD, призначених для автоматизованого проведення дедукції. Надано опис їхніх характерних рис та особливостей. Наведено приклади, які демонструють можливість їх використання для розв'язання математичних і повсякденних задач, що потребують виконання дедуктивних побудов. Описано можливі шляхи подальшого розвитку англомовної системи SAD.

Работа посвящена программе «Алгоритм Очевидности», инициированной академиком В.М. Глушковым в 1970 г. и нашедшей свое воплощение в виде русскоязычной и англоязычной систем SAD, предназначенных для автоматизированного проведения дедукции. Дано описание их характерных черт и особенностей. Приведены примеры, демонстрирующие возможность их использования для решения математических и повседневных задач, требующих выполнения дедуктивных построений. Описаны возможные пути дальнейшего развития англоязычной системы SAD.