Logo des Repositoriums
 
Konferenzbeitrag

Evidential paradigm and intelligent mathematical text processing

Lade...
Vorschaubild

Volltext URI

Dokumententyp

Text/Conference Paper

Zusatzinformation

Datum

2004

Zeitschriftentitel

ISSN der Zeitschrift

Bandtitel

Verlag

Gesellschaft für Informatik e.V.

Zusammenfassung

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.

Beschreibung

Lyaletski, Alexander; Doroshenko, Anatoly; Paskevich, Andrei; Verchinine, Konstantin (2004): Evidential paradigm and intelligent mathematical text processing. Information systems technology and its applications, 3rd international conference ISTA'2004. Bonn: Gesellschaft für Informatik e.V.. PISSN: 1617-5468. ISBN: 3-88579-377-6. pp. 205-211. Regular Research Papers. Salt Lake City, Utah, USA. June 15-17, 2004

Schlagwörter

Zitierform

DOI

Tags