The talk is devoted to the issues of the implementation of an automated theorem proving program called Evidence Algorithm (EA) that was initiated by V.M. Glushkov for making investigation simultaneously into formalized languages for presenting mathematical texts in the form most appropriate for a user, formalization and evolutional development of a computer-made proof step, EA information environment having an influence on a current evidence of a computer-made proof step, and interactive man-assistant search of a proof.

Beginning with the middle of the 1960s and ending today, research on EA took place in different years with a distinguished success. There are two main stages in the implementation of EA. The first occupies the time between 1971 and 1983 and the second --- between 1998 and 2007. During the 1st period, the Russian(-language) SAD system was designed and implemented and during the second, the English( language) SAD partially based on the ideas used in Russian SAD was designed and implemented. Russian SAD was constructed as a theorem-proving system, while English SAD can be considered as a computer assistant possible to prove theorems and verify mathematical proofs embedded into a self-contained mathematical text.

Besides of this, the talk also contains some results on inference search in 1st-order logics that were carried out as a part of the investigation on EA or initiated by EA.