The work being carried out on the development of Ukrainian and Russian versions of the ForTheL formal natural language, which is the input language of the SAD system for automated deduction (http://nevidal.org/sad.en.html) and simulates the structure of sentences of ordinary English, is described. The implementation of these versions will permit to do a remote access to the SAD system for solving tasks of theorem proving and mathematical text veri cation for a user who speaks only one of the three languages (English, Russian or Ukrainian). This con rms a perspectivity of providing human mathematical activity with a computer support in languages that, on the one hand, are formal, but, on the other hand, are as close to the languages used by people in their daily practice as possible.
The emergence of the Internet and cloud technologies has reinforced the urgency of the problem of multi-language support of a remote human interaction with a particular computer system. This also applies to various automated reasoning systems that are either already hosted or, potentially, can be hosted in the Internet. As a rule, communication with such systems is performed in a single language, most often in English. However, it is obvious that along with an existing input language of a system, it is desired to have an ability to do such interaction with the system in other languages that are, from a certain point of view, more user-friendly than the existing one.
Existing approaches to solving this problem are usually reduced to the
problem of computer understanding of an ordinary human language, which has not
yet found a good enough practical solution. That is why the approach proposed
by V.M. Glushkov [
1. An example of a successful enough actions in this direction is the ForTheL
language [
Suppose that we wanted to write in ForTheL a proof of the proposition that S is the empty set if and only if S is a subset of any set, and did so in the form of the ForTheL-text, located at the page \http://nevidal.org/cgibin/sad.cgi?ty=txt&ln=en&link=small/emptyset.ftl", a part of which is given below and which, being put in a mathematical environment containing all necessary notions and propositions, are easily veri ed by the SAD system. Leaving aside the veri cation process itself, we pay attention to the natural presentation of the veri ed text having the form of an ordinary English text.
De nition DefSubset. A subset of S is a set T such that every element of T belongs to S.
De nition DefEmpty. S is empty i S has no elements.
Axiom ExEmpty. There exists an empty set.
Proposition. S is a subset of every set i S is empty.
Proof.
Case S is empty. Obvious.
Case S is a subset of every set.
Take an empty set E.
Let z be an element of S.
Then z is an element of E.
We have a contradiction.
end. qed. 2. Such closeness of a ForTheL-text to an ordinary English text is explained by the fact that the syntax of a ForTheL sentence follows the rules of the English grammar. It is based on the notion of a section.
ForTheL sections are: sentences, sentences with proofs, cases, and top-level sections: axioms, signature extensions, de nitions, lemmas, and theorems. A toplevel section is a sequence of assumptions concluded by an a rmation.
There exist three kinds of sentences in ForTheL: assumptions, selections, and a rmations. Assumptions serve to declare variables or to provide some hypotheses for a subsequent text. For example, \Any subset of any set is a set." and \Assume that m is less than n." are typical assumptions. Selections state the existence of representatives of notions and also can be used to declare variables. An example of a selection is: \Take an even prime number N.". A rmations are simply statements, e.g. \If p divides n+p then p divides n".
Sentences are constructed from such syntactical units as statements, predicates, notions (that denote classes of objects) and terms (that denote individual entities). Units are composed of syntactical primitives: nouns which form notions (e.g., \subgroup of") or terms (e.g., \closure of"), verbs, and adjectives, which form predicates (such as \belongs to", \compact" and others), symbolic primitives using a concise symbolic notation for predicates and functions and allowing to construct usual rst-order formulas in the form of ForTheL-statements. Naturally, just a little fragment of English is formalized in the syntax of ForTheL.
Like a usual mathematical text, a ForTheL-text consists of de nitions,
assumptions, a rmations, theorems, proofs, etc. (see details in [
3. The proposed languages uaForTheL and ruForTheL have a similar structure and grammars admitting, in particular, the translation of uaForTheLand ruForTheL-texts into rst-order language formulas. As a result, the current versions of uaForTheL and ruForTheL allow one to write the abovegiven text as follows (giving the ability to set tasks for the SAD system in di erent languages with the possibility to translate them from one into another language in the case of the implementation of uaForTheL and ruForTheL). ae Æ Ł
S „ Ł . - Œ ¤ Ł Ł i S
T Œ
ø Œ „ º Ł Ł i S „ ae i .
Ł . ae ¤ Ł . ˛ Ł Æ Ł Ł.
Ł . - Œ ¤
We see that the uaForTheL- and ruForTheL-texts being formal can be considered as texts written in ordinary Ukrainian and Russian. Therefore, we can say that we have at least partially achieved our aim. Besides, there appears the possibility to construct the next bidirectional translators from one formal natural language to another: ForTheL-texts $ uaForTheL-texts, ForTheL-texts $ ruForTheL-texts, and uaForTheL-texts $ ruForTheL-texts, which leads to the multi-language interface both with the SAD system and with a computer service requiring a user-friendly interaction in di erent languages.
The above-said shows that on the basis of the proposed approach, it is possible to achieve a su ciently good solution of the problem under consideration. Additionally, it can be noted that the outlined approach can be used not only in the case of solving tasks of automated theorem proving and veri cation of mathematical texts, presented in di erent languages, but also in the case of a multi-language support of (e-)learning and testing a knowledge gained by a person in the process of studying mathematical disciplines.
Finally, the authors hope that this research will give an impulse to the development of ForTheL-like languages and lead to the creation of an info-structure for the remote multilingual presentation and complex processing of mathematical knowledge and it will be useful in both academic and teaching daily activities of a person.