Evidence Algorithm and System for Automated Deduction: A Retrospective View (In Honor of 40 Years of the EA Announcement)

摘要

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", EA1. 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. The paper gives a retrospective view to the whole history of the development of the EA and SAD. Theoretical and practical results obtained on the long way are systematized. No comparison with similar projects is made.