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 computer-made proof step, EA information environment having an influence on a current evidence of computer-made proof step, and interactive man-assistant search of proof.

SAD system
Explanations
Download
Our Team

Since then, a lot of investigations were made in all the above spheres. Russian and English versions of the formalized mathematical languages were developed. Their syntactical analyzers were designed. At present time, a translator of the English-based Formal Theory Language (ForTheL) into the first-order language is implemented. A sequential formalism was developed for construction of an efficient technique of proof search in an initial theory (without preliminary skolemization). A special approach was offered for applying definitions and auxiliary propositions that takes into account the neighbourhood of the proposition to be proved. Basing on this formalism, a first-order prover was implemented.

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.