Evidence Algorithm and System for Automated Deduction: A Retrospective View
Alexander Lyaletski (1), Konstantin Verchinine (2) ((1) Kiev National, Taras Shevchenko University, (2) Math-Info Department, Paris 12 University)

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMathematics, Computing, and Information Processing
