Evidence Algorithm and System for Automated Deduction: A Retrospective View

TL;DR

This paper reviews the development of the Evidence Algorithm and the associated automated deduction systems over four decades, highlighting their role as powerful theorem-proving assistants.

Contribution

It provides a retrospective analysis of the Evidence Algorithm and the SAD system, emphasizing their historical significance and technological evolution in automated deduction.

Findings

Development of the Evidence Algorithm over 40 years

Creation of Russian and English versions of SAD system

SAD as a powerful theorem-proving assistant

Abstract

A research project aimed at the development of an automated theorem proving system was started in Kiev (Ukraine) in early 1960s. The mastermind of the project, Academician V.Glushkov, baptized it "Evidence Algorithm", EA. The work on the project lasted, off and on, more than 40 years. In the framework of the project, the Russian and English versions of the System for Automated Deduction, SAD, were constructed. They may be already seen as powerful theorem-proving assistants.