In this paper, the approach to the development of deductive assistance based on the current state of the System for Automated Deduction, SAD, is described briefly. The SAD may be considered as a three-dimensional "shell" for deductive assistance in a formal natural language environment when solving a number of scientific and industrial tasks requiring automated theorem proving, verification of formal texts, construction of knowledge bases for formalized theories, integration of symbolic calculation with deduction, and so on.
Citation:
Anatoly Anisimov, Alexander Lyaletski, "The SAD System in Three Dimensions," synasc, pp.85-88, Eighth International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'06), 2006