By the end of 1960s Academician V. Glushkov advanced a programme on investigating automated theorem proving, which was later called the Evidence Algorithm, EA (first mentioned in "Kibernetika", 2, 1970). V. Glushkov proposed to make investigation simultaneously into formalized languages for presenting mathematical texts in the form most appropriate for a user, formalization and evolutional development of computermade proof step, EA information environment having an influence on a current evidence of computermade proof step, and interactive manassistant search of proof.
As a result, the System for Automated Deduction (SAD) appeared.
Theses of the EA programme promise to be helpful in attacking such problems
as distributed automated theorem proving, verification of mathematical
texts, remote training in mathematical disciplines, and construction of
databases for mathematical theories.  
