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.

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. The 1970 paper's own words are quoted in the review by Letichevsky, Lyaletski and Morokhovets (2013): Glushkov calls the automation of theorem proofs in mathematics the best model problem for modelling logical thinking; the centre of gravity of the work is to be shifted from 'universal' proving programs to programming systems that allow one to program quickly the search for a proof of even a single hard theorem and to work in real time with the mathematician proving it; in its initial form the evidence algorithm may be limited to the simplest inference functions in the propositional calculus, supplemented by a search of the tree of constructions for a small number of steps. According to the same retrospectives: the first group on proof automation formed at the Institute of Cybernetics in 1962, and they trace the start to Glushkov's article of that year, which the 1975 bibliography of his works places in the Kyiv journal Radianska shkola, 1962, No. 2, pp. 87-91; 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 bibliographic records and one memoir say about the 1970 paper itself (none gives its text). The original is Kibernetika, 1970, No. 2, pp. 3-13, the first item of the issue's contents (next article: p. 14); the translation is pp. 17-27. An eleven-page offprint is held by the Vernadsky National Library of Ukraine. A paper of the same title, 31 pages, stands under 1968 in the 1975 bibliography of Glushkov's works, in the volume 'Theory of automata and methods of formalised synthesis of computing machines and systems', No. 6, from the Institute of Cybernetics' press; its relation to the journal text is not stated. 'Evidence algorithm' is already in the titles of two newspaper articles of 1969 (one of 17 July), not found. In N. M. Mishchenko's memoir (2013, p. 173) the paper is devoted to a general formulation of the problem of teaching language, based on Glushkov's own research (in a passage on teaching a machine to recognise meaningful sentences); a footnote on that page cites the 1968 volume; the evidence algorithm is not mentioned. The 1962 article. The 1975 bibliography and the museum's list of Glushkov's works give it alike: Radianska shkola, 1962, No. 2, pp. 87-91, no month, under a Russian title; the 2010 retrospective gives the English title 'Intelligent' machines and the mental activity of a human, marked 'In Russian'. The journal's 1962 volume in HathiTrust shows only page numbers and match counts. A search finds, among other places, Glushkov's name and the title words in Ukrainian ('Розумні', 'розумова діяльність людини') on p. 2 and p. 87 of what by scan order is No. 2, probably the contents page and the article's start. How that fits the Russian title is unclear. The hits say almost nothing of the content: on p. 90 'теорем' stands three times and 'теореми' once, while 'доведення' was not found on pp. 87-91 nor 'алгоритм' anywhere in the volume (whole words). The 2010 retrospective says the article analysed several simple proofs in group theory; the 2013 review cites it for proof-search research begun in 1962 in group theory; what has been read neither confirms nor refutes this. What the record does not claim: that the papers of 1970 and 1962 were read. The words of the first come from the 2013 review's quotations; the second is known by bibliographic entries and by the places of the author's name and title words in the journal's volume, without its text, month or whole title line; the 1968 volume and 1969 articles by title only. Nor that the 1970 text equals the 1968 one or shortens it, or that the paper is only about the evidence algorithm: the retrospectives describe proof automation in it, the memoir teaching language. Nor that the 1970 paper was the first to say 'automated' rather than 'automatic' theorem proving, as the 2010 retrospective writes: the quotations say 'automation of proofs' but do not show who said it first. Nor that 'evidence algorithm' first appeared in print in 1970, as the project site has it: the phrase is already in the titles of 1969 articles, whose content is unknown. Nor that the 1962 article treats proving theorems or automating it, still less proofs in group theory: 'теорем' on p. 90 does not show it. Any measurement of the SAD system.