The purpose of this communication is to outline brie y the current state of the so-called SAD system (System for Automated Deduction), present its architecture, and discus some possible ways of its further development. At that, the main attention is paid to the development of multiple language support of the SAD system as well as to the construction of SAD proof search methods, toolkit, and engine for making deduction in di erent rst-order logics.
The current version of the System for Automated Deduction (SAD system)
was designed and implemented in the framework of the so-called evidential
paradigm [
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 [
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 brie y the current state of the English SAD system and discus some of the possible ways of the development of its linguistic and deductive tools. 2
While building the English SAD system, the architecture given in Fig. 1 and re ecting 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 rst-order formulas, and, after this, solve the automated theorem proving/veri cation tasks by using a native prover or one of the famous rst-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 rst (linguistic) level, the parser module (ForTheL) rst analyzes an
input ForTheL-text, its structure de ned 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 rst-order language, which can be used for solving the task
of establishing the deducibility of a rst-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) [
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 rst-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 rst-order prover, such as Otter [
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. 3
The above-given description of the English SAD system demonstrates that the system has original possibilities and satis es 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, [
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.