20th WCP: Between Logic and Heuristic

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 form) 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 form).

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». Computer Heuristic (computer 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 Computer 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 (look at Fig. 2 in the end of this article).

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 (proof-search theory)?

Let me illustrate this problem with the help of the simple example of verifying validity of formula F:

(1) ((P1 & ... & Pn) É Q) É ((Ø Q É Ø (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 É Q » must be true and « Ø Q É Ø (P1 & ... & Pn) », false. If « Ø Q É Ø (P1 & ... & Pn) » is false, then « Ø Q » is true (« Q» is false) and «Ø (P1 & ... & Pn) » is false (« P1 & ... & Pn » is true). But if « P1 & ... & Pn » is true and « Q » is false, then « (P1 & ... & Pn) É 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.

(2) ((p É Q) É (Ø Q É Ø 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 É B) É (Ø B É Ø 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:

(3) (p & Ø Q) Ú Q Ú Ø p

(equivalent 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 represented as «diagram» (Fig. 1), in which verification of validity of d.n.f. F is trivial.(2)

KatrFig1.jpg (11081 bytes)

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:

method of metavariable (dummy variable);
method of «global processing of information».

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 formula S which is to be tested for its deducibility, a special calculus— proof-search calculus H— the deducibility in which of a special object Å is equivalent to the deducibility of S in calculus B ( Fig. 2).

It is possible to introduce a modification of Maslov’s inverse method, which I termed calculus of numbers with index.(3) 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).

KatrFig2.jpg (21702 bytes)