Evidence Algorithm and System for Automated Deduction: A Retrospective View

2010/05/24 by Lyaletski, Alexander, Verchinine, Konstantin
#01-02 (Primary) 68T15 #03B35 (Secondary) #Artificial Intelligence (cs.AI) #F.4.1 #FOS: Computer and information sciences #I.2.4 #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1005.4447

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.

Related

• 05431 Executive Summary – Deduction and Applications
• Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematics
• The Theorem Prover Museum -- Conserving the System Heritage of Automated Reasoning
• Top-down Automated Theorem Proving (Notes for Sir Timothy)
• Automatic Proof Checking and Proof Construction by Tactics