Home Latest Advanced Search By Year By Division 

Not Logged in. Login 
Evidence Algorithm and Processing Formalized Mathematical TextsVershinin, 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 07472315 Full text not available from this repository. AbstractThe 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 selfcontained 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 sequenttype 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 
Accessibility  Terms and Conditions  Last Modified 01 November 2007 
© 2007 DCS, King's College London, Strand, London WC2R 2LS, England, United Kingdom. Tel +44 (0)20 7836 5454 