Menu_Home Home   Menu_Latest Latest   Menu_Search Advanced Search   Menu_Browse_by_Year By Year   Menu_Browse_by_Division By Division
Screen decoration graphicsLogo

Evidence Algorithm and Processing Formalized Mathematical Texts

Vershinin, Konstantin and Degtyarev, Anatoli and Lyaletski, Alexander and Morokhovets, Marina and Paskevich, Andrey (2002) Evidence Algorithm and Processing Formalized Mathematical Texts. Journal of Automation and Information Sciences, 34 (10). ISSN 0747-2315

Full text not available from this repository.


The goal of a research programme Evidence Algorithm is a development of an open system of automated proving that is able to accumulate mathematical knowledge and to prove theorems in a context of a self-contained mathematical text. By now, the first version of such a system called a System for Automated Deduction, SAD, is implemented in software. The system SAD possesses the following main features: mathematical texts are formalized using a specific formal language that is close to a natural language of mathematical publications; a proof search is based on special sequent-type calculi formalizing natural reasoning style, such as application of definitions and auxiliary propositions. These calculi also admit a separation of equality handling from deduction that gives an opportunity to integrate logical reasoning with symbolic calculation.

Item Type:Article
Additional Information:12 pages
ID Code:905
Deposited By:Dr Anatoli Degtyarev
Deposited On:08 Nov 2007 15:05
Last Modified:08 Nov 2007 15:05

Repository Staff Only: item control page