Investigations on the design and creation of high-performance information systems based on a number of paradigms supporting a human activity in formalized text processing were started in the beginning of 1960s { the time of the appearance of computers of such a high performance that programming of complex intelligent processes became possible. The so-called evidential paradigm is among them and it can be considered as a certain way of the integration of all reasonable paradigms intended for the development of languages for presenting formalized text in the form most appropriate for a user, formalization and evolutional development of a computer-made proof step, information environment having an in uence on a current evidence of a computer-made proof step, and interactive man-assistant search of a proof. This paper contains a short description of the evidential paradigm and its implementation in the form of systems for presenting and processing formal knowledge.
The term \arti cial intelligence" cannot be reduced only to the creation of devices or their components that completely or partially simulate the physical activity of humans; it also touches questions relating to the ability of a human to do reasoning in the framework of formalized languages. Investigations in this direction as well as in the direction of design and creation of high-performance intelligent information systems, now called automated reasoning systems and computer algebra systems started in the beginning of 1960s { the time of the appearance of computing machines of such a high speed, information capacity, and exibility, that the programming of complex intelligent processes became possible. As a result, several di erent paradigms of the intelligent processing of computer formalized knowledge have appeared.
- 26
E cient processing of formalized knowledge presupposes carrying out deep investigations in the elds of automated reasoning and construction of linguistic tools intended for supporting daily mental activity of a human, which presupposes an auspicious combination of theory and practice.
Attempts to nd a reasonable balance between theory and practice have lead to creation and development of a number of certain paradigms re ected in intelligent systems such as automated theorem-proving and computer algebra systems.
In Ukraine, such investigations were initiated by Academician V.M.Glushkov
in the end of 1960s, who announced the Evidence Algorithm (EA) programme in
[
The implementation of Glushkov's approach in the framework of the evidential paradigm has found its partial re ection in the form of the so-called SAD system (System for Automated Deduction) intended for the presentation and processing of (formalized) mathematical texts in English and accessible at http://nevidal.org/. This paper is devoted to a short description of the peculiarities and features of the evidential paradigm and SAD. 2
Some remarks on formalized knowledge processing Let us consider some of the issues, with which computer science is constantly dealing in solving problems associated with the formalized knowledge processing based on the following paradigms: numerical, analytical (symbolic), deductive, inductive and integrative.
The numerical paradigm re ects tools and methods for nding approximate or exact solutions of problems of pure or applied mathematics. It is based on constructing nite sequences of numerical calculations and actions over nite sets of numbers.
The symbolic (analytical) paradigm is based on the ability of computers to perform complex symbolic transformations, do numerical calculations, plot functions, construct mathematical models of certain processes, and so on. It is focused on the construction and use of computer algebra systems and appeared as an alternative to the numerical paradigm in the middle of 1960s, when computers with high enough performance were constructed.
The deductive paradigm re ects the declarative way of the representation and
processing of computer knowledge. It is based on the fact that existing knowledge
is represented in the form of certain formal texts or their pieces (usually axioms,
1 A detailed enough description of EA and the investigations connected with it can
be found in [
The inductive paradigm is based: in the natural sciences { on the transition from individual observations to general conclusions, while in mathematics { on the induction method used for the \checking" of a selected property for partially or fully ordered objects.
The integration paradigm \brings together" all of the above-mentioned paradigms. It can be divided into two types:
{ integration at the design phase, when the ability of hierarchical building-in new components and subsystems into a designed system and connecting it to available computer services is provided during the design time of the system and { integration at the operation stage, i.e. combining existing computer services into one (new) system (a special interest to the development of such services has been caused by a wide use of the Internet for the date exchange and transition of a necessary information, which, in its turn, led to the creation of relevant data exchange standards).
As to the integration at the operation stage, there can be mentioned Open
Mechanized Reasoning Systems [
The most famous representatives of the approach to the integration at the
design stage are the QED [
As for the Evidence Algorithm, it can be considered as the rst representative of the integration paradigm at the design stage, which gave a reason for calling it by the evidential paradigm. 3
The evidential paradigm is developed for mainly solving such problems of formalized text processing as proving a theorem under consideration or verifying a given proof of a theorem.
According to the evidential paradigm, the scheme of the processing of
formalized (non necessary mathematical) texts is as follows (a more detailed description
can be found in [
Text prepared by a user for proving/verifying a theorem =========> (using a parser) A rst-order self-contained text =========>A computer{made proof/ve(using a prover) ri cation =========>Text in a form comprehensible for a human (using an editor)
- 28
Thus, the following problems arise in the framework of the evidential paradigm: creation of formal mathematical languages, construction of deductive methods and tools, creation and usage of information environment, and development of interactive modes.
Let us brie y describe each of them and some of the ways used for solving them. Naturally, the main attention will be paid to the linguistic and deductive tools satisfying the evidential paradigm requirements. In this connection, the other tools are only slightly contoured. 3.1
The following requirements were formulated for a language that should be constructed in the framework of the evidential paradigm.
Its syntax and semantics should be formalized. It should allow writing the axioms of a theory under consideration as well as auxiliary propositions, lemmas, theorems, and their proofs to ensure the self-containedness of a text and wording of de nitions. The language thesaurus should be extensible and separated from the language grammar. In addition, it should be close to the languages of mathematical publications in order to provide convenience and comfort to a user in creating and processing a text in interactive mode. Besides, it should give the possibility to write formulas of the rst-order language. Moreover, it should allow to formulate tasks that are not directly related to the deduction search.
The rst sketch of such a language appeared in 1970 [
In 2000, a new, improved, English-language version of TL called ForTheL
(FORmal THEory Language) was constructed [
Like any usual mathematical text, a ForTheL text consists of de nitions, assumptions, a rmations, theorems, proofs, etc. The syntax of a ForTheL sentence follows the rules of the English grammar. Sentences are built of units: 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. \subset of") or terms (\closure of"), verbs and adjectives which form predicates (\belongs to", \compact"), symbolic primitives that use a concise symbolic notation for predicates and functions and allow to consider usual quanti er-free rst-order formulas as ForTheL statements. Of course, just a little fragment of English is formalized in the syntax of ForTheL.
There are three kinds of sentences in the ForTheL language: assumptions, selections, and a rmations. Assumptions serve to declare variables or to provide some hypotheses for the subsequent text. For example, the following sentences are typical assumptions: \Let S be a nite set.", \Assume that m is greater than n.". Selections state the existence of representatives of notions and can be used to declare variables, too. Here follows an example of a selection: \Take an even prime number X.". Finally , a rmations are simply statements: \If p - 29 divides n p then p divides n". The semantics of a sentence is determined by a series of transformations converting a ForTheL statement to the corresponding rst-order formula for processing it by the deductive tools of SAD.
ForTheL sections are: sentences, sentences with proofs, cases, and top-level sections: axioms, de nitions, signature extensions, lemmas, and theorems. A toplevel section is a sequence of assumptions concluded by an a rmation. Proofs attached to a rmations and selections are simply sequences of low-level sections. 3.2
From the very beginning of its appearance, EA has paid great attention to developing machine proof search methods suitable for the various elds of mathematics and taking into account (informal) human reasoning techniques.
Deductive tools should satisfy the following requirements: (1) the syntactical form of an original task under consideration should be preserved; (2) deduction should be carried out within the signature of an initial theory (i.e. without applying skolemization); (3) proof search should be goal-driven; (4) equality (equations) handling should be separated from a deductive processes.
As a result, the sequent approach was selected as basic for the construction of logical engines in the framework of the evidential paradigm. This permitted to satisfy (1) in a good enough form. Besides:
{ for satisfying (2), a technique for the optimization of quanti er handling was proposed on the basis of an original notion of an admissible substitution, { for satisfying (3), proof search was proposed in the form \driving" the process of an auxiliary goal generation by taking a formula (goal) under consideration into account,
{ for satisfying (4), special methods for equality processing and equation solving were developed (allowing the use of algebra systems and problem solvers if necessary).
Investigations in this direction began in 1963, when the problem of automated
theorem proving in group theory was formulated by V. Glushkov. As a result, the
procedure admitted its interpretation as a speci c, sound and complete, sequent
calculus later called the AGS (Auxiliary Goals Search) calculus was proposed in
[
Attempts to overcome this disadvantage of AGS led to the construction of
an original sequent calculus [
Since then, these investigations were stopped until 1998, when the paper's
authors started participating in the Intas project 96-0760 \Rewriting Techniques
and E cient Theorem Proving" (1998-2000). This project gave an impulse for
modifying the calculus from [
Note that the (new) notion of admissibility is not enough for the construction
of sound calculi in the intuitionistic case. This situation can be corrected by
using the notion of compatibility rstly used in [
Interactive modes can serve for interfacing a computer assistant (in our case { the SAD system) with both a user and computer mathematical services existent in the external information environment. They can be designed and implemented only after xing the form of internal and proof environments. 4
The earlier-mentioned English SAD system satis es well enough the
requirements of the evidential paradigm and now it can be considered as its three-level
implementation that is intended for theorem proving and text veri cation [
At the rst level, its parser module analyzes an input mathematical text, its structure, and its logical content, encoded in the ForTheL statements. After this, the translation of the text into its internal presentation is made.
The result of translation gives a list of goal statements to be deduced from their predecessors. Note that there exists a module for processing rst-order formulas presenting in a \dialect" of ForTheL, which can also be used if convenient.
At the second level, the goal statements are generated one-by-one and subsequently processed by the so-called foreground reasoner of SAD for reducing them to a number of subtasks for a prover splitting a goal under consideration to several simpler subgoals or generating an alternative subgoal. The module becomes redundant when SAD solves a problem for automated theorem proving.
Proof search tasks are resolved by a background prover at the third level. The SAD native prover is based on a special goal-driven sequent calculus for the classical rst-order logic with equality. Note that it exploits the above-mentioned The above-given material shows that the evidential paradigm is well in line with the modern trends in the processing of formalized (not obligatory mathematical) texts and that the SAD system looks fruitful from the point of view of implementing the existing principles of the construction of computer mathematical services being de ned as information systems that are able to carry out numerical calculations and/or symbolic transformation and/or deductive constructions. The paper's authors hope that the ideas presented in the paper and used in the SAD system, will attract the attention of researchers in the eld of arti cial intelligence and will be useful in developing computer services intended for formal knowledge presentation and processing.