Cybernetics and Systems Analysis, Vol. 39, No. 5, 2003
EVIDENTIAL PARADIGM: THE LOGICAL ASPECT
A. V. Lyaletski
UDC 510.645:004.832.3
This paper is devoted to the description of a logical formalism, which is a part of the so-called evidential paradigm proposed by academician V. M. Glushkov in the form of a complex program of works called “Evidence Algorithm.” Basic sequential calculi, their distinctive features, and results on their soundness and completeness are given. These calculi were used as a result of implementation of a system of automated deduction (SAD). Keywords: automated theorem proving, deduction, first order logic, sequential calculus. INTRODUCTION V. M. Glushkov proposed the Evidence Algorithm (EA) at the end of the seventieth [1] in the form of a program of works on creation of systems for automated theorem proving. Basic aspects of implementation of the EA program are as follows: — construction of a formal language (languages) to write theorems and their proofs (if required) in different semantic domains of mathematics; this language should be maximally approximated to the language of natural mathematical publications; — formalization of the concept of machine evidence for every step of a proof in the constructed language as follows: each step of the proof should be justified with the help of constructed formal methods of inference search and also with the help of mathematical facts that are well known at the current moment; — construction and development (with the help of EA) of an information environment containing the description of mathematical concepts, their properties, and the corresponding statements and influencing the concept of machine evidence of a step of a proof; — construction of interactive methods of processing mathematical texts. The idea of construction of EA is in the tideway of modern trends in constructing and integrating computer mathematical services. In this connection, by the end of the ninetieth, the works on the implementation of the conceptions inherent in EA [2] were renewed. A distinctive feature of the investigations on EA that are pursued now is that the search for a statement and its proof (verification) should be performed in the environment of a self-contained mathematical text written in a language that agree closely with the natural mathematical language. (Such a self-contained mathematical text is understood to be a text containing all the data necessary for proving the statement being considered.) EVIDENCE ALGORITHM: THE CURRENT STATE The basic principles that characterize the EA program at the present stage of its development can be detailed in the form of the so-called evidential paradigm whose structure is described below. Languages. Languages should satisfy the following requirements: — they must have formal syntax and semantics; — they must provide the possibility of forming axioms of theories, required statements, lemmas, theorems, and proofs for obtaining self-contained texts;
Taras Shevchenko State University, Kiev, Ukraine,
[email protected]. Translated from Kibernetika i Sistemnyi Analiz, No. 5, pp. 37-47, September-October, 2003. Original article submitted October 1, 2003. 1060-0396/03/3905-0659$25.00
©
2003 Plenum Publishing Corporation
659
— their thesauri must be separated from expandable grammars; — they must maximally approximate to natural languages of mathematical publications; — they must make it possible to translate formal texts written in these languages into formulas of the first order language with a view to using well-developed methods of inference search. Deduction. According to the evidential paradigm (Evidence Algorithm (EA)), the kernel of any system of processing mathematical texts (knowledge) must be of the so-called “evidential” procedure used for establishing the soundness of the step being verified and validity of the entire statement, which is proved using some complete deductive technique. It is natural that, to this end, various methods of strengthening the evidential procedure should be provided, in particular, the search for auxiliary statements and other relevant information, use of analytical transformations (i.e., the use of existing capabilities of computer algebras), representation of machine steps of inference search that reflect expedients that are customary for man, etc. At the current stage, it is assumed that the deductive technique should provide the realization of the following functions: — to display the syntactic structure of the problem being solved; — to efficiently form deductive constructions in the signature of the initial theory; — to reduce the solution of a goal (problem) to the solution of a number of auxiliary subgoals (subproblems); — to use analytical transformations (to use the capabilities of systems of computer algebra) to separate the process of finding a concrete solution from deduction; — to choose methods of solution that adequately reflect distinctive features of object domains; — to use expedients that are customary for man in proofs; — to support the interactive mode of inference search. Information environment. The EA program provides for the construction and evolutionary development of its information environment (the base of mathematical knowledge) that accumulates knowledge obtained during the implementation of EA, contains the description of distinctive features of the object domain being considered and, eventually, affects the concept of machine evidence of a step of a proof. The information environment should use distinctive features of representation, extraction, and processing of computer mathematical knowledge. Interface. Interface means should provide the possibility of active participation of unskilled (as to EA) users in its process of searching for the solution of a formulated problem and facilitate the understanding of the search process and also of the used way of achievement of the goal formulated (for example, in the interactive mode). Moreover, they should provide the connection (for example, through Internet) of mathematical services that are most helpful in finding a possible solution of the problem being considered. At present, we can speak of the first software implementation of the evidential paradigm in the form of a system of automated deduction (SAD) (http://ea.unicyb.kiev.ua). Since the deductive component plays a very important role in the implementation of the EA program and has a number of essential distinctive features, which differentiate it from modern systems of inference search, a formal description of only this component is given below. QUANTIFIER RULES AND ALLOWABLE SUBSTITUTIONS As has already been noted, the evidential approach naturally leads to the necessity of construction of evolving reasoning techniques in different first order logics. These techniques should allow a system of automated processing of mathematical texts to prove statements within the framework of the signatures of the initial theories, which, naturally, implies attempts to abandon skolemization, which is realized, as a rule, only with a view to obtaining highly effective methods of processing of mathematical texts and practically means that man cannot understand the process of machine search for a proof when the interactive mode is used. Moreover, the use of skolemization for nonclassical logics frequently requires “sophisticated” methods of transformation of the initial text, which substantially changes the initial text and then leads to the impossibility of using human intuition to help computers in choosing optimal techniques of inference search. Investigations on machine reasoning techniques led to the creation of various methods of inference search in first order theories. In particular, attempts of improvement of Gentzen calculi themselves [3] and some their modifications were made. Among them, we should first mention the Kanger method [4] and a congenial method from [5], which is based on a heuristic search procedure used in group theory and proposed in [6]. We note that skolemization is already absent in these techniques and that some departure from the Gentzen concept of an allowable substitution of terms for variables is observed when definite quantifier rules are used. However, the technique proposed in these works was found to be inefficient from the practical viewpoint and is not widely used.
660
Usually, in implementing machine methods of inference search, preference was given (and is given) to systems of inference search that are based on ideas that date back to T. Skolem [7] and J. Herbrand [8]. They make it possible (owing to skolemization and subsequent combination of rather simple propositional rules with the algorithm of construction of the so-called most general unifier) to automatically realize inference search by some sufficiently efficient way. First of all, the well-known resolution method [9] and inverse method [10] should be mentioned. Later on, attempts to make use of ideas of the authors of these methods in other methods of automated inference search have led to the development of many various techniques of inference search, for example, the method of elimination of models, connection graph method, tabular methods, etc. In [11], one can found almost all the latest advances in creating efficient methods of automated reasoning in the first order logic, but all these methods require skolemization. A higher efficiency of the methods that use ideas of T. Skolem and J. Herbrand in comparison with machine methods based on usual Gentzen sequential calculi is mainly caused by the fact that the latter methods use an additional exhaustive search with respect to different orders of application of quantifier rules. (Note that the question of construction of a modification of the classical Gentzen calculus in which all the positive quantifier complexes were eliminated using preliminary skolemization was studied in [12].) When quantifier rules are used in standard Gentzen calculi instead of the variables of the quantifiers being eliminated, definite terms are substituted. In order to make an inference step sound, the substitution being chosen should satisfy definite restrictions. A substitution that satisfies these restrictions is called allowable. At present, two types of the concept of an allowable substitution for sequential calculi are mainly considered, namely, the Gentzen concept [3] and Kanger concept [4]. Hereafter, we will show how one can modify the concept of an allowable substitution that is introduced in [13] and, as a result, obtain some optimization of quantifier applications, which leads to a substantial growth in the efficiency of inference search in sequential calculi. The Gentzen concept of an allowable substitution. Usual (Gentzen) quantifier rules that substitute a term in an arbitrary structure for a variable of the quantifier being eliminated (during “top-down” application of this rule) are of the form (see, for example, the calculus LK in [3]) ∀ x F,Γ→ Θ
Γ → Θ, ∃ x F
| tx , Γ →
Γ → Θ , F | tx
F
Θ
;
here, the term t must be free for the variable x in the formula F . (Note that an expression of the form F |tx denotes the result of simultaneous substitution of t for x.) This restriction (introduced by G. Gentzen) on the substitution of a term for a variable leads to the standard concept of an allowable substitution, which completely meets all the requirements of the proof theory but becomes absolutely “useless” from the viewpoint of providing the efficiency of the process of inference search. The sequent considered below is a good illustration of this fact (see example 3a in Chapter 4 of [14]). Let there be a sequent P1 , P2 , P3 , P4 → G , where we have P1 is ∀ x1 ∃ b1 ∀ u1 (B (u1 , b1 ) ⊃ ∃ a B ( f (u1 , a), x1 )), P2 is ∀ x 2 ∃ b 2 ∀ u 2 ∀ y 2 (B ( f (u 2 , y 2 ), b 2 ) ⊃ B (u 2 , x 2 )), P3 is ∀ x 3 ∃ b 3 ∀ u 3 ∀ y 3 ∀ z 3 (B ( f ( f (u 3 , y 3 ), z 3 ), b 3 ) ⊃ ⊃ B ( f ( f ( y 3 , z 3 ), u 3 ), x 3 ), P4 is ∀ x 4 ∃ b 4 ∀ u 4 ∀ y 4 ∀ z 4 (B ( f ( f (u 4 , y 4 ), z 4 ), b 4 ) ⊃ ⊃ B ( f ( f (u 4 , z 4 ), y 4 ), x 4 )), G is ∀ a1 ∃ x ∀ a 2 ∀ a 3 (B ( f (a 2 , a 3 ), x ) ⊃ B ( f (a 3 , a 2 ), a1 )). The deducibility of this sequent in LK [3] will be established in the section “Example.” Here, we note that the quantifier rules must be applied to all the quantifiers that belong to P1 , P2 , P3 , P4 , and G. Hence, the standard concept of an allowable substitution generates 22 ! / ( 4 !* 4 !* 5 !* 5 !* 4 !) different orders of application of quantifier rules to the sequent P1 , P2 , P3 , P4 → G , and the Gentzen concept of an allowable substitution implies an exhaustive search for all possible orders of application of quantifier rules, whereas resolution methods make it possible to obviate such a search owing to skolemization. The Kanger concept of an allowable substitution. To optimize the procedure of application of quantifier rules, S. Kanger proposed in [4] his sequential calculus of the Gentzen type (which is denoted here by K). In the K calculus, a “pattern” of an inference tree is first constructed with the help of special variables called parameters and “dummy” variables (parameters and dummies according to S. Kanger). At definite moments of time, attempts are made to transform the “pattern”
661
into the inference tree of the initial sequent by substituting definite terms determined from the “pattern” for “dummy” variables. Failing such an attempt, the process of “unfolding of the pattern” runs up to the next attempt of obtaining an inference tree and so on. The basic distinction between LK and K consists of a special modification in the above-mentioned quantifier rules and in the partition of the process of construction of a “pattern” into definite stages (the description of this process is omitted here). Quantifier rules in K are of the form ∀ x F,Γ→ Θ F
| xd
,Γ→Θ
< t1 , . . . , t n / d > ,
Γ → Θ, ∃ x F Γ → Θ , F | xd
< t1 , . . . , t n / d >,
where d is a “dummy” variable, t1 , . . . , t n are terms that are free for the variable d and contain only functional symbols from the premises of the rules applied, and the expression t1 , . . . , t n / d shows that d should be replaced by only one term from t1 , . . . , t n in the case where an attempt is made to transform a “pattern” into some proof tree. The “dummy” variables are replaced by chosen terms at the end of each stage and, at each stage, the inference rules are applied in a definite order. This deduction scheme in K leads to the Kanger concept of an allowable substitution and, owing to this fact, the inference search process in K becomes more efficient than that in the standard Gentzen calculus. In particular, for the sequent from the above example, we can restrict ourselves to the consideration of only 6 ! / 2 ! ( = 360) different orders of possible applications of quantifier rules (however, as in the case of the LK calculus, it is impossible to prefer any of possible orders). With a view to increasing the efficiency of inference search, the Kanger concept of an allowable substitution can also be used to modify the intuitionistic calculus LJ [3]. Note that the Kanger approach still does not make it possible to achieve such an efficiency of the deduction process that is observed when preliminary skolemization is used. This is explained by the fact that, as well as in the case of standard admissibility, if any order of applications of quantifier rules does not lead to success, then a new order of preferences is chosen, and so on. A distinctive feature of the approach proposed. Despite the fact that the Kanger concept of an allowable substitution leads to the increase in the efficiency of search processes in comparison with the Gentzen concept, the calculi that use it do not make it possible to achieve the efficiency that is observed after skolemization. This is explained by the fact that, as well as in the case of Gentzen admissibility, the chosen order of application of quantifier rules influences the establishment of the deducibility of the initial sequent. If, for some reason or other, it does not provide a success, then it is necessary to try to use another order of application of rules, etc. In this article, in order to improve this situation, the author propose construct calculi of the sequential type in which the quantifier rules are necessary only for fixing the quantifier structure of formulas that forms the sequent being investigated. Based on the analysis of this quantifier structure and a chosen (based on some considerations) substitution that can transform the leaves of the sequential inference tree into axioms, it is possible to try to establish whether the initial sequent is deducible or not deducible using a special concept of an allowable substitution. THE EVIDENTIAL APPROACH TO INFERENCE SEARCH The sequential calculi (without skolemization) considered below are so constructed that a maximum of requirements on deduction in the evidential style are fulfilled. Note that the first of them, i.e., GD1 , can be considered as an extension of the “line” of calculi that are presented and investigated in [15–17] and the second one, i.e., GD2 , which can be considered as a simplified version of the rules from GD1 that are applied to the succedent, had eventually led to the calculus GD, which formed the basis of implementation of the logic apparatus of the SAD system [18, 19]. Preliminary information. We consider the classical first order logic without equality with the standard notation of logical connectives. To denote the empty formula, the symbol ◊ is used. The concepts of a variable, a term, the formula of a literal, and its complement are considered to be known. The expression F ¬ denotes the result of one-step insertion of negation into a formula F of the form (∀ x P) ¬ is ∃ x ¬P , (∃ x P) ¬ is ∀ x ¬ P, ( P ⊃ Q) ¬ is P ∧ ¬ Q, ( P ∨ Q) ¬ is ¬ P ∧ ¬ Q, ( P ∧ Q) ¬ is ¬ P ∨ ¬ Q, (¬ P) ¬ is P, and A ¬ is ¬A, where A is an atomic formula.
The positive ( P F + ) and negative ( P F − ) occurrences of a formula F in a formula P are defined as usual.
662
Hereafter, the letter W (possibly, with lower indices) denotes a set or a sequence of first order formulas each of which can contain indexed and unindexed variables. We assume that different quantifiers of formulas from W have different variables. The concept of the scope of a quantifier is also assumed to be known. For each variable υ from W, a countable set of new variables of the form k υ is introduced, where k = 0 , 1, 2 , . . . . These new variables are called indexed. Any expression being considered can contain ordinary variables and indexed ones. If k is an index and F is a formula, then the expression k F denotes the result of simultaneous assignment (at the upper left) the index k to all the bound variables of F (i.e., the old indices are replaced by the new index k). We assume that a variable υ is an unknown variable with respect to W if and only if there exists a formula P ∈ W such
that P (∃ υ F ) + formula P ∈ W
or P (∀ υ F ) . Accordingly, υ is called a fixed variable with respect to W if and only if there exists a such that P (∃ υ F ) − or P (∀ υ F ) + . −
If S is a sequent of the form W1 → W2 , then variables fixed with respect to W2 (unknown variables with respect to W1 ) are called fixed variables with respect to S. And vice versa, unknown variables with respect to S are called unknown variables with respect to W2 (fixed variables with respect to W1 ). The set W induces an antisymmetric relation p W on the set of bound variables of the formulas from W as follows: u p W if and only if, for some formula F from W, a quantifier with a variable w from F belongs to the scope of a quantifier with a variable u from F . Moreover, in this case, if k u and i w are indexed variables and enter into the same formula from W, then
k
u p W i w is also assumed to hold true (here,
k
u and
i
w denote the variables u and w after reindexing).
The concept of a substitution is treated as in [9]. Any substitution component is assumed to be of the form t / x , where x is called the variable (denominator) and t is called the term (numerator) of the substitution. It is also assumed that the concept of the most general (simultaneous) unifier of sets of expressions is known. Let σ be a substitution, and let t / u ∈ σ, where u is an unknown variable with respect to W and t is a term. If w is a fixed σ σ . variable with respect to W and w enters into t, then we write w
