|Home Latest Advanced Search By Year By Division|
|Not Logged in. Login|
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.
Repository Staff Only: item control page