Definition Theory as Basis for a Creative Problem Solver

Introduction

One of the main directions in research of artificial intelligence is developing problem solving systems namely, systems for automatic designing /SAD/. Their practical importance is invaluable. These systems are capable to solve constructive tasks. A task is constructive if the un­ known is some kind of an object of which characteristics are described in the con­ ditions of the task. 'rwo kinds of these are distin~ished:

1. 'I'he objects to be constructed are defin­
2. ed explicitly:
3. a/ well-defined task
4. b/ incompletely defined task - here the conditions provide an incomplete description of the object
5. The objects to be constructed are defin­ ed implicitly.

In these taks the objects are not named only certain expectations are given about them.

Designing t~ appearing on the expecta­ tions of a non-professional customer belonc to latter type. lt can't be expect­ ed from him to give an expliciG definition of a required program e.g. with the in­ put-output · relation. All he can do is to give some hints on his own expectations towards some "programlike" thing. 3imilar problems occur at decision making where information is implicitly connected with the question to be decided about.

A 3AD capable of solving the second type constructive task, must consist of the following two basic oomponents:

1. Hic:h-level problem defining unit which provides an explicit definition to the implicit object description
2. ::Jolvine unit which carries out the
3. exPlicitly defined task

;.:athematical logic and its model theory provides plenty of facilities in SAD reaear.ch. In our present study we intro­ duce the usefUlness of definition theory, an intensively developing filed of model­ theory, from the point of view of ::lAD.

Basic definitions

'Che following triple form a language: (syntax, the set of possible worlds, vali­ dity), or formally L =(F, M, !o').

• A type t is a pair of functions, i.e.
• t ·<'t'',-t'such that
• R'-t' & w' <Pl where W· {o, 4 1 2 1 ·· · J
• R9t·s w
• Oo-4:'() Doi"=¢ where ~ denotes the empty set.

Here Dot and ~t' are the domain and the range of t respectively. 0, t' is the set of relation symbols and Doi'is the set of function symbols.

In the followings we suppose that a t-type first-order langugage "L ··<,.F .. , M~, ,_)

is g~tven. Here HI: is the set of t-type structures. A t-type structure Of is a function for which

1. Olfo) ~A is the universe of the s;~c~uri;~C~J
2. vc. (R, ~ :4 for each relation symbol R ~ D<>t 1
3. aCF) : *"CF~_.A for each function symbol F G Dot and if 1: -rn -o then Cll CF)~A

Aboves are to be found in more details in (1]. I·:otations of common knowledge are also to be found there.

From now on when program is being dis­ cussed relation symbols will be used in describing the oamputer programs where such symbols may show what relation the input-output should have. This descrip­ tive method provides a far more natural handling of the programs than the des­ criptions of programs by functions, since this approach is more close to the intuition of the non-programer customers.

Intuitive d~scription of :3.'\.D based on the definition theory

Let r~,f* be a set of first-order formu­ las which provides the knowledee of a discripline within that r·esigning will occur. ~~.c,. r provides the semantics of a proeraminr.; language and the proper­ ties of different implemented proc,rams.

The customer r,ives his requeots with the hel;p of a set of formulas Z1 · 'l'his I implicitly defines one or more relation symbols and/or function symbols which do not occur in Dot 1 U Doi" · In the follovliilf:S without limitinr: rcncrality, we suppooe that Z' tivco the !lllplicit definition of only one relation symbol P. 'S.g. Z:: gives the implicit defini­ tion of such a program of which input and output are in relation P. Let X(P) denote the set of formulas defining the relation P implicitly.

I.et t pJ (t'CJ(P,,.},iJbe the extension of the t type t and AF P be the syntax of the first-order language extended by relation P. Thus Z! (P) ~ 1 F !p

T .. carry out the design of the required object we have to give its explicit description by a forrula of 1 Ft- · So as to have the required program ¥~itten in our programing language we have to find such a formula from ,Ft which defines P explicitly.

Let P,P 1 ~£M'ua,t' be two n-placed rel.J.tion symbols and Z!(P')~ ,F'-.,., · ',/e say that ,Z(p) defines P implicitly if

Z!(P}uX(p') ~V~'"'' (PCxO·?-..PCi'"')) where X 1 " 1 .g{X,r .~,.) and V,it"J.IIx, .. . ll.r,.. \ie note that Z!(P') is obtained from by replacing P everywhere by P'.

de give an equivalent definition to this: Let (U,T?)40lU(~P,R)) where 0/GH'- ,r<s:;~ Given any models[O.R) and(ti,f')forE(P) then f·~'. This means thatnJtJimplicitly defines P if for any model ~'t there is at most one n-placed relation R interpreting the relation symbol P such that f:l,~)trE(P).

:t Let tpf r . If it has n free variables then we use the notation CfC'X 1 "'J.

27[p) explicitly defines the relation P if there is a formula tfC "i 1 "'l€,rt for which

z:'rPJ F Vx(,, ( PCx("1JcH> c..pc i l"!J).

Replacing P by Y' in the set of formulas ~ everywhere we obtain Z'{lp) · For Z' (f) the following is true:

fi'J z:.r rreJ2Z{PJu { v xM fPrx("1J c4>CfL7{"!iJJ

where · is the symbol of semantical equivalence.

ii'hat is the taak of a high-level problem defining unit supposed to be at SAD? It has to find a definition GG,F .. on the base

of r knowledge to the re~uested expectation of the customer given by ~(P) so that r u { Vf'"'cPG frtJ )<H g Ci'"'J)} ~ Z! (P)

In other words using (#f) such formula l}[ic"'.J~,,t h~ to be found for which rt==2{B).

This task results in the following questions:

1. Does a formula 9 exixt to r so r t-Z" (9) · If such doesn't exist then r r l could be extended, let's say, to a {r'~,r*) so as to have the required formu­ la 9 existing such thu t r' t==- Z'Ce)

This procedure can be done with the help of a system consistinc of a theorem prover and of an inductive hypothenis generator. :·'irst it will examine the truth of r (J { ,"~ J 1- <fl\ 1 '{>

/here A 1! is obtained so that all the formulas of Z! are linked with the "and" connective A /. If tlis isn't true then we exami,ne whether r I u l11\Z} ,_'fit l'f is true. If this isn't so then we take · r" t another extens1on e c.

r, r" ;ie note that selecting 1 suppose an oriented inductivity.

The following problem belongs to here also. Is it true that all certain characteristic model Cll (C/2�I1~ of a set of formulas r becomes a model of 1!(9} too, i.e. is it true that

at=-2!ra>

Let us suppose that the existense of 0 ,;,F"t: is proved or that taldmg the risk of a possible negative answer we suppose the existence of 9 . In this case the following question appears.

2. I low can we obtain the sui table formula () from set of formulas r v2 CP) ? llere we show some of the possible ways of producing formula 9 · a/ ,.,uZ'CP)~ vxc"J (P(xcr.JJ~ecir"'J)

i.e. the definition of P is parametrically given by the set of formulas I'CP). Here (;l"'} c { lf 11 ·· · , cr,.,) 1 3 c;-c""'J -s:. "311i . .. '3 cr"" · c/ ru~(p) F= V Vi~) (P(i'"')~ 8,. CiCnJ] j.fl.l·,"

. i.e.rcP) defines P ex:9licitly up to disjunction. d/ rvL'{P),. V 3ic"''Vic"J(pr;c"~8,· C?'tf"'~ J.~·~t .

i.e. Z:CP) defines P explicitly up to parameters and disjunction.

It mi[~ht happen th:.l.t the set of formulas r has to be extended till r' as it is mentioned in j. so as to define e

In that case if set of formulas ..l'tP)is too weak then, sil!lilarly to the methods described in [2] we ~\Ve to find such a formula 9 for which

r v lv'r", cP a'" 1 J ..:-. e c i"c" 1 J)J ,_ 2! .

'i'he set of formulas r can be extended here too if found necessary.

In that case if answer to question 1. is positive the following statement is true. loemma: a/ if ru'1!(P},_'/'i(JJJ(p(X'"J)~>9[X'"!:/J then r t-=2 {B)

b/ if ruZCP)I'V y'-/" 1 (Pft,.J,k+~l: ?'~ '*'·k ·

then r!=Pl9J.J or rt=:Pt9~), ... , or r t=Z {9~c)

.le note here that we luve to try the {J / (t~l'6 k.) in b/ till the first formula where the statement stands for true.

If ·the answer to question 1. is negative ·t:-tcn the knowledge within the disciplines defined by f1 io not enoueh for the explicit description of the required ob­ ject.

On the basis of aboves a "hieh-level"

problem defining unit of SAD should operate the following way.

The basic knowledge of SAD is provided by set of formulas r . The customer gives his required object description by the help of set of formulas Z'(P) As a first step the unit has to find an exact answer for the existence of 9 , but since it is to complicated a task the following way is chosen. Pirst the system controls whether2(P) contradicts to knowledge r , i.e. it tries to deduce the identically false (cpll 1f) from r UI!. · If this doesn't 6uceed within a present time period then the system presupposes the existence of a formula and it will proceed onto the 2. task, i.e. produc­ ing 8 ·

Let us suppose that we succeeded in producinc such a formula. It is followed by tis tryine:

rJ-zceJ

If this is true then 9 really becomes the requirements of the customer if not, then it may be supposed that the knowledge r of the SAD is not satisfactory for defining e . rherefore r has to be extended till r' and aboves have to be I repeated now for set of formulas r . 'l'h c system will eo on with this either until it proves the impossibility of Z(P) on the basis of t fie extended set of formulas or, it succeeds to produce formula 9 · Of course the system goes on with tryine only for a fixed time. .. 'e note that the extension of set of formulas r need inductive logical means from the system.

:.ow we shall see that case when g (P) defines P only up to the disjunction, t :1:1 ·; is when

ru2CP)t= \1 Vx(rtJ(P(ic" 1 )~e,.['xc"'1) l· ·~1.: 'rhe so obt<.:. inecl formulas E); Cit"~ (t·L~ 1.::) have to be controlled one by one. So rt-.27 (9,) .or r t-2{f7L) 1 .. . 1 or r rZ' {9k)

This control goes 011 until the first (;),· for which rt-.zrcet) · If neither B.· satisfies above condition ·then it might be supposed that the knowledge r is not satisfactory. In this case the pro­ decure goes on similarly, i.e. r is

extended until r' , etc.

Useful theorems of definition theory

In this chapter we introduce those theo­ rems of definition theory without proof which provide the explicit definition of P on the basis of Z!fP} and r . 'fheir proofs can be found in L.: 1]. It is expected· to obtain different types of theorems depending on the strenght of Z!CP) · '.ie begin ~i th the theory contain­ ing the weakest conditions for ~(P).

If Z(P) , r and a model Ol is given then the conditions of the theorems contain either that how many relations R £ llA are there for which (Ol,Q ),.2 {P) '; or 'n. that how many such relations ~£ :'4 are there to such a relation f?~~ so as (Ol,R') ~ {Ol,R)

1. Theorem /Chang - iJakkai Theorem/. If for every model {a,R) /for which IAI>cv / of ...Z: u r':

IAI t{R' : ( 01, R ) ~ ( u, Q')} I < 2

then there are a finite number of para­ metric formulas 81. [ ic"l r::fl/lltf) J 1 G>.zCi(":J''"],..'I ~["l'(M:ii-'""'] of ,F~ such that

r vZ'(P) F v :Jir"" 1 Vil"'(Pti~~4-»~.[i1"'t;C-ij ·-~~k

The theorem intuitively states if ~(P} circumscribes the relation P in some measure then there exists a parameter­ -vector (u;, .. . 1 tr,..) and there are formulas Q i [ 'i (M) VC'"'1 J (t sc'$ II!) of 1 F't such that one of them gives the definition of P. In other words the set of formulas ~fP) defines P explicitly up to para­ meters and disjunction.

Theorem 2. If set of fornulas .z'(pj is such that to each model C-t~Ht it is

I{~ (Ol,R) ... 2. J I<:: 2IAI

then there exists a finite number of first-order parametric formulas ~i (~ ·i$lt.}ao that

ru2cP) 1= V .3ii'"'Vtr"l (par"~...,.. e, [ ir"' urn.~J) 'cl"d:

The intuitive meaning of the theorem is as it follows: if the number of relations satisfyine set of formulas .z'Cf>) is less than the number of all possible relations then up to disjunction 27CP) parametrically defines relation Po ·L'he condition of the theorems claims that not all the possible relations should carry the characteristics described by the set of formulas 2lP).

Above theorems /Theorems lo and 2o/ are true also for that case when the number of the suitable relations is less than not .2 1 /tl, butiAI+ioe. in this case there exists a finite number of first­ -order parametric formula and such a parametervec·tor that one of the formulas will give the definition of relation P by the suitable parametervectoro

Low let us see possible number ZCP) are finite those cases when the of relations satisfyine in the models.

'l'heorem 3. If for every model (a, R) (tl~

of .2(P)vZ it is true that

){R·! (Oi,tl} 9u,R')Jf < w

then there exists such a lc~c..> and there are such formulas ~ [ iJ' ... 'l , 91 [ ;<"' if ,..,,J ( '-" t'~ lc.) in 1 Ft that

r uZfP) 1=- :J(j-C'"'J (~ [iiC ... Jj)ll

-7 v v i(tl'( Pc"Kc"''J~eic;Pir;-tiiMlJ). 1 ~ ,." k

'I'heorem 4o If ;!!(P)uf' is such that in every model C.P£ H~ it is l{R:t:,.t,R}F '""'".ZJI<"" then the statement of the previous theorem is true.

Intuitively the above theorems /Theorems 3o and 4./ state the followinc: if ..z'{P) is such that its required characteristics are fulfilled in every model by at least finite number of relations then there 0 + ex1.sts such a formula 6' e ,F" for ca.lcula ting parameters cJir . 1 1}",.. and there exist formulas e., ... ,t'Jic.E-,F* out- of which one defines relation P by the parameters determined by CY ·

;:·rom the point of view of ~.lAD this means t lut a theorem prover extended by induct­ ive elements can prove, that

Zf'P)I)f' ,_ 3 u-c"'J tS"{crc""'].

On the basis of thic proof a zero-order termvector T Cnt} must be selected so that Z ;..~[r c"" 1 ] o!>fter t 1l is it has to be proved, that

2! f- V Vr("I(P(ic"'')...,. 8,· [ il"1-r. lns) J). l~l·~lc. ·rhen on the basis of knowledge r : we select the suitable defining formula ().- J:rl*IJ

i ow Wf! further restrict the requiremelits concernine set of formulas Z {P) o

·.~heorem 5o If for each model {O,R} of ZtP}vf' there exists such a finite k~ , so lf~' :p,R)£:(01, ri)JI ~ k

__, r- - (l·tl1 then there exist such formulas o ~· 1.. tr ~ {),i" CiC" 1 u-r"" 1 1 ( 1""'J ·~ r 1 1· I'~ k } in Ft Uw.t I L' (P Jur 1= v 3Trc"" 1 6'! r ifC'"lJ !\ V ;;t"' 1 6s-! rc:r"'!]..., ··~·~~..... { " -;. v \1 ~(10, r p r "ic .. , J ~e.~· cic" 1 u- c,.1)). '" ·":Jk

"l'hcorem 6 o (;~ueker rheorem/: If 2:" (P)IJ[ is such that for each model a £/1~ there exists a finite ~~/ , so

I l il :(a, rV 1= Zit I ~ k

then there exist such formulas

In these theorems similarly to 'l'heorems 3. and 4. the formulas tSt ~"' r} and the formula ~ serve to define the parametervector. 'rhe definition of relat­ ion ~ is done also on the basis of those described after Theorem 4. There is a difference only when definition is done on the basis of Theorem 5, because here we have. to try out the formulas not only acco:tdinc: to t' {4::n's k.) but also according to S ( ~ ~ ~ ~ 'f') ·

The conditions of Theorems 5. and 6. for ECP) are so much stronger than those of l'heorems 3. and 4. that now we claim the existence of such a finite k which is upper-bound of the number of suitable

relations in each model.

'.i'he .ZfP) is t :e strongest in that case if this conditions are satisfied in each model by at least one relation. Now we discuss those theorems which refer to

this.

Theorem 7. / Svenonius' Theorem/: If for each model {()1, R) of ..z!(p} I) f' :

ll ~· = (a,R}~(a,~')} I s 1 then there exists a finite m <Co) and there exist such formulas 9, C(lM~ Cr·~'d) in rt eo that,

2'CP)uP FV Vi'"'(P[il",cH> G>,· [if"'IJ). , ... ~'-'"

Intuitively it means that if we take two extensions {o?, R,) and {a,RJ of any mo­ del Cfl~ht so that these become models of r U.2 (P) and these are isomorphic then ~. :;s ~.~.

In this case the set of formulas ~cP) defines relation P up to disjunction.

Theorem 8. /Beth's Theorem/: If the set of formulas .L'CP)ur' is such that for each model a J:= f·ft :

cc-;;c·~ then there exists such a formula ~ A

1 -l ~ .. ca,~Jtt=-Z!fP) J I~ .l in 1 F-t that

Intuitively if 2CP) is so strong that every model Citi=Ht can be extended to a model of rur by at the most one relat­ ion then .ZCP) defines relation P explicitly.

Conclusion

As we could see from aboves the model theory provides mathematical bases suitab­ le for the development of different kinds of SAD important in the practice. This is expecially important because to construct implicitly described objects from psicho­ logical point of view is a task demanding creativity. The degree of creativity part­ ly depends on the circumscription of the required object and partly on the develop­ ment of the corresponding discipline. With the help of the theorems of different strength described in aboves we can obtain different SAD-s of different degree of creativity. So far we can see tru1t the research of artificial intelligence requires the application of deep mathe­ matical results of mathematical logic. To make SAD more effective we need the ~ following problem to be solved: if.Z:fP)sa,F and rs;,rt-are given then what conditions should ~(P) satisfy so as to have a formula .tJ ~. r.f existing for which r ,ztaJ.