The current version of the System for Automated Deduction (SAD system) was designed and implemented in the framework of the so-called evidential paradigm [1] intended for the presentation and complex processing of formal mathematical knowledge [2] and being a current vision of the Evidence Algorithm programme (EA) initiated by V.M. Glushkov [3] 1 .
By now there were implemented two versions of the SAD system: the Russian and English versions. Firstly the Russian SAD system appeared (it was announced in 1978 and published in [6]) and much later, in 2002, its English modification was first presented at the IIS'2002 symposium [7]. English SAD can be considered as the further development of ideas laid in Russian SAD oriented to automated theorem proving and possessing such additional property as the ability to verify formalized mathematical texts. Also note that opposite to Russian SAD having a restricted (formal) Russian as its input language (called TL [8]), English SAD is equipped with a restricted formal English as its input language (called ForTheL [9]).
The current version of the English SAD system is implemented on the Linux platform and can be reached via Internet (http://nevidal.org/sad.en.html).
The objective of this communication is to outline briefly the current state of the English SAD system and discus some of the possible ways of the development of its linguistic and deductive tools.
While building the English SAD system, the architecture given in Fig. 1 and reflecting the current state of English SAD was designed. Note that in the design process, the objective was to construct a system able to accept and analyze formalized natural texts, translate them into first-order formulas, and, after this, solve the automated theorem proving/verification tasks by using a native prover or one of the famous first-order provers and/or computer algebra systems. This architecture can be considered as a tree level structure containing internal (native) linguistic, reasoning, and deductive modules and having possibility to use external theorem-proving (TPS) and computer algebra (CAS) systems.
At the first (linguistic) level, the parser module (ForTheL) first analyzes an input ForTheL-text, its structure defined with the help of ForTheL markups, and its logical content encoded in ForTheL-statements. After this, it translates the text into its internal presentation. The result of translation gives a series of goal statements for deducing them from their predecessors. FOL denotes a parser for a "dialect" of the first-order language, which can be used for solving the task of establishing the deducibility of a first-order formula/sequent in classical logic in the case of necessity. The module TPTP provides the ability to connect with the famous library TPTP (Thousand Problems for Theorem Provers) [10], if a SAD user will decide to try to solve one of the TPTP problems.
At the second (reasoning) level, the goal statements are processed one-by-one by the foreground reasoner Reason. This module is intended to reduce a given proof task to a number of subtask for a prover. It works in a dialog with the prover: It may split the main goal to several simpler subgoals or propose an alternative subgoal. This module becomes redundant when English SAD solves a task connected with automated theorem proving.
Inference search tasks are resolved by the background native prover Moses at the third (deductive) level. Moses is based on a special goal-driven sequent calculus for classical first-order logic with equality. The original notion of an admissible substitution used in the calculus permits to preserve the initial signature of a task under consideration so that accumulated equations can be sent to a specialized solver, e.g. an external computer algebra system. Note that English SAD was implemented in such a way that at present time it can be connected with one of first-order prover, such as Otter [11], SPASS [12], or Vampire [13].
English SAD reports the result of its work after completing it. The protocol of its successful or unsuccessful work can be printed as desired by a user.
The above-given description of the English SAD system demonstrates that the system has original possibilities and satisfies the existing approaches and requirements to intelligent computer services intended for the complex processing of formalized mathematical knowledge. But its trial operation as well as a number of investigations made in automated reasoning last years have shown the desirability and possibilities of improving the capabilities of English SAD in the following directions (studied and not implemented).
On the linguistic level. The nearest objective is to incorporate the existing Englsh ForTheL language into the LaTeX-environment in order to reach the reading of ForTheL-texts in the form closest to usual mathematical texts. (Now this task is under consideration.) Besides, there are drafts of the Russian and Ukrainian versions of the (English) ForTheL language. Therefore, there exists the possibility to construct the next bidirectional translators: English ForTheLtexts ↔ Russian ForTheL-texts, English ForTheL-texts ↔ Ukrainian ForTheLtexts, and Russian ForTheL-texts ↔ Ukrainian ForTheL-texts, which will give the opportunity for using such a multilingual extension of English SAD by a person who knows only one or two of three just-mentioned languages, as well as for making automatic translation of a ForTheL-text written in one of these languages into a ForTheL-text written in another. (Of course, one can try to construct a French, German, and/or other version of ForTheL language, thereby strengthening such a multilingual SAD component.)
On the reasoning level. It is planned to increase the heuristic possibilities of the system by incorporating in it the human-like reasoning methods depending on the subject domain under consideration concentrating main attention on inductive theorem proving methods. Besides, tools for interfacing with some of the famous computer algebra systems are going to be developed and implemented.
On the deductive level. On the basis of the research made on computeroriented proof search in classical and non-classical sequent logics (see, for example, [14]), one can try to construct a toolkit giving the possibility to "puzzle" one or another ("native") proof search method depending on a desire of a SAD user or a subject domain under consideration. (This possible feature of such an extended system will play an important in the case, when the application of non-classical reasoning becomes necessary element for successful decision of a task under consideration.) Finally, the authors hope that the described development of the English SAD system will lead to the creation on its basis of an info-structure for the remote multilingual presentation and complex processing of mathematical knowledge and it will be useful in both academical and teaching daily activity of a person.