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