Gesellschaft fr Informatik e.V.

Lecture Notes in Informatics

Information Systems Technology and its Applications, 3rd International Conference ISTA'2004, June 15-17, 2004, Salt Lake City, Utah, USA P-48, 205-211 (2004).

GI, Gesellschaft für Informatik, Bonn


Terry A. Halpin, Stephen W. Liddle, Heinrich C. Mayr Anatoly E. Doroshenko (eds.)

Copyright © GI, Gesellschaft für Informatik, Bonn


Evidential paradigm and intelligent mathematical text processing

Alexander Lyaletski , Anatoly Doroshenko , Andrei Paskevich and Konstantin Verchinine


This paper presents the evidential paradigm of computer-supported mathematical assistance in “doing” mathematics and in reasoning activity. At present, the evidential paradigm is implemented in the form of System for Automated Deduction (SAD). The system is based on the methods of automated theorem proving and is intended for intelligent mathematical text processing. It proves mathematical theorems, verifies validity of self-contained mathematical texts and can be used for inference search in first-order sequent-based logic as well. For human-like representation of mathematical knowledge, SAD exploits an original formal language close to natural languages of scientific publications. Since the problem of automated text verification is of great importance for industrial applications (checking specifications, proving safety properties of network protocols, etc), the paper illustrates some principles and peculiarities of the evidential paradigm by means of exemplifying the verification of a part of a non-trivial mathematical text.

Full Text: PDF

GI, Gesellschaft für Informatik, Bonn
ISBN 3-88579-377-6

Last changed 24.01.2012 21:46:09