S.L.Katretchko BETWEEN LOGIC AND HEURISTIC The aim of this article is constuction new tipe of logical calculi - logical-heuristic calculus (calculus of proof-search) which, in explicit form, contains means of reducing complete search. Such an explication "heuristic" component of calculus is reached with the help of meta-level means. Among them major mode for reducing search is structual information about contrary literals of formula. There are two major approaches to studying the process of reasoning (problem-solving). On one hand, it is necessary to discover and investigate correct modes of reasoning in which the property of "truth" is preserved. This task which can be formulated as the question "what is a correct reasoning (proof)?" is considered in Logic. In order to decide this problem, Logic is based upon the concept of "logical form". There is a special syntactical method to deal with this concept - the method of construction of a logical calculus. In this respect, the calculus in question is a "black box" which guarantees the "true" conclusion under the "true" premisses. Thus, Logic (logical syntax) gives the answer for the question about correct reasoning - "the correct reasoning is a proof". But logical syntax, as a "black box"-calculus, isn't interested in the real process of derivation building, in studying the question about methods of proof-search, in studying and construction a more manageable and efficient machinery of "truth" preserving. Availability of any method of exhaustive (complete) search, e.g. British museum algorithm, is quite enough for Logic (logical syntax). On the other hand, the process of problem-solving can be investigated in the light of the following question: "how is it possible to build a piece of correct reasoning?". This task is considered in Heuristic. Heuristic investigates general principles and methods of problem-solving. In my dissertation I define it as follows: Heuristic (heuristic method) is a system of rules (a rule) for essential reducing the complete search, i.e. heuristic methods are opposed to exhaustive search methods. The area of intersection of Logic and Heuristic is proof- seach theory (PST) which investigates possible methods of problem-solving ("how is it possible to build a proof?") in some calculus. PST deals with the heuristic component of proof systems. More precisely, the aim of proof-search theory can be defined as follows: "discovering, on the basis of a calculus and an entity in the calculus in question of the structure of a possible derivation of this entity, a derivation which is interesting in some respect" [1]. Thus, proof-search theory can be included into the logical pragmatic (fig. 2). My investigation is a sistematic heuristic (pragmatic) analysis of logical calculi. The main aim is following: what is a tool for answering the question "how is it possible to build a proof?". Is it possible to use the concept of logical form as such a tool? How is it possible to use the concept of logical form for a proof-search? Let me illustrate this problem with the help of the simple example of verifying validity of formula F : ((P1 & ... & Pn) implication Q) implication ((not q implication not (P1 & ... & Pn). First, its validity can be snown by means of a truth-table, i.e. we can verify all possible combinations of truth value of variables P1, ..., Pn, Q which occur in F. This is a non- heuristic method of complete search. Second, this complete method might be reduced with the help of using the sence of logical connective "implication". Suppose, that F is invalid. Then, using the sence of implication, we obtain that "P implication Q" must be true and "not q implication not P", false. If "not q implication not P" is false, then "not q" is true ("q" is false) and "not P" is false ("P" is true). But if "P" is true and "q" is false, then "P implication q" can't be true. Thus, it proves falsehood of our assumption, i.e. F is valid. In this case, we essentially reduced complete search. There are few methods of similar reducing - Beth's semantic tableaux, Smulluan's analitic tableaux etc. Notice, that in this case it suffices to analyse only "surface" structure of formula F, i.e. F: ((P implication q) implication (not q implication not P)), when P : P1 & ... & Pn. Third, it can be done with the help of knowledge of derived rule - law of contraposition, because the "surface" structure of F is following: ((A implication B) implication (not B implication not A)). (Notice, that the problem of using derived and adissible rules is an important part of PST). The second and third methods of establishing validity of F capitalize on structure (form) of F (only "surface" structure). But it might use possibilities of the stucture of logical form in a more essential way. It is possible to analyse stucture of formulae in order to expose relevant information for proof- search. It is the key appoach for my investigation. F can be easily transformed in an equivalent disjunctive normal form (d.n.f) F : P & notq v Q v notP (eqivalent in logical "sence", but not in heuristic "sence"). For establishing validity of F one can use not only information about composition of conjuctions of d.n.f F, but also information about composition and quantity of complementary pair literals of d.n.f. F. In this case, d.n.f. F may be P ---------notQ represented as diagram [2] in \ \ which verification of validity notP Q of d.n.f.F is trivial. This example allows me to give the following "positive" answer for the question: it is possible to use logical form for the building of derivations, because logical form contains useful information for the proof-search. A more precisely answer is given. It can be constucted, on the basis of logical calculi, special logical - heuristic calculus which, in explicit form, contains means of reducing complete search. Such an explication "heuristic" component of calculus is reached with the help of meta-level means. Among them two major modes are of point out: 1. method of "global processing of information". 2. method of metavariable (dummy variable). The systems which have means of proof-search I termed calculus of proof-search . They can be constructed like this. For any calculus B any proof-search method can be represented as a mode of construction over every entity S which is to be tested for its deducibility, a special calculus - proof-search calculus H - the deducibility in which of a special object a is equivalent to the deducibility of S in calculus B. It is possible to introduce a modification of Maslov's inverse method, which I termed calculus of numbers with index. I regard this calculus as universal proof-search calculus in which it is possible to simulate other poweful proof-search methods (for example, well-known methods of resolution and splitting). REFERENCES 1. S.Yu Maslov "The theory of deductive systems and its applications" (Russian), Moscow 1986. [Engl. transl. MIT Press 1987]. 2. G.V.Davydov "The synthesis of the resolution method and the inverse method" in Journal of Soviet Mathematics vol.1 N1. 3. S.L.Katretchko Maslov's inverse method //Logika i kompjuter:2, Moscow, Nauka, 1995 P.62-75 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ ! -------- ! ! ------------- ! ! LOGIC ! ! HEURISTIC ! ! -------- ! ! ------------- ! \ ! ---------------! / \ ! PROOF-SEARCH ! / \ ! ! / \ ! THEORY ! / ! ---------------! / \ / \ LOGICAL FORM \ \ METHOD OF "GLOBAL PROCESSING \ OF INFORMATION" \ METHOD OF METAVARIABLE \ / LOGICAL CALCULUS \ / !------------------------- ! ! CALCULUS OF SEARCH-PROOF! !--------------------------! fig.2