Glushkov: the 'evidence algorithm' programme
In Kibernetika in 1970 (No. 2, March-April) Victor Glushkov published a paper on problems of automata theory and artificial intelligence in which, according to his students' retrospectives, he formulated the 'evidence algorithm' programme: a formal language close to that of mathematical papers, proof search built on a machine notion of an evident step that grows with the system's experience, and a person helping the search.
Why it matters
Kyiv framed proof automation as joint work of mathematician and machine rather than fully automatic search; following this programme the Institute of Cybernetics built by 1978 the SAD system, which was shown in public. This is an editorial assessment resting on the group's retrospectives.
The pages of the 1970 paper that describe the evidence algorithm itself were not read: only the first two pages of the English translation (Cybernetics, vol. 6, no. 2, pp. 17-27) are open, and they deal with automata theory. The programme's content is taken from participants' retrospectives: Lyaletski and Verchinine (2010) and Lyaletski (2020), who quotes Glushkov's 1970 text in Ukrainian translation: continuous improvement of the evidence algorithm will sooner or later make all known theorems evident to the machine. According to the same retrospectives: the first group on proof automation formed at the Institute of Cybernetics in 1962; the first public demonstration of the Russian-language system was at a symposium in Kyiv on 28-30 November 1978; Glushkov named it the System for Automated Deduction (SAD) in 1980; the English-language SAD was shown at CADE-21 in Bremen in July 2007. What the record does not claim: the exact wording of the 1970 paper; that it was the first to say 'automated' rather than 'automatic' theorem proving, as the 2010 retrospective writes; any measurement of the SAD system.