Problem Solving of Elementary Algebra by Hierarchical Abstraction

1. INTRODUCTION

The abstraction of a problem and a relation which retains only their key characteristics will be in­ dispensable for global solving of complicated problems. Many researches of mechanical problem solving using this concept have been actively done, but a lot of problems to be solved seem to remain for practical use.[l],[2]. This paper de­ velops the method of EAPS(Elamentary algebraic Problem Solver) of the previous paper[3] by add­ ing (i)a tree-like address table of theorems and global relations for the efficient access to them and (ii)a mixed abstract notation of problems for flexible representation.

2. ABSTRACT EXPRESSIONS

In mechanical problem solving, it is considered indispensable to introduce an abstraction or an abbreviation method of expressions at least in complicated quantitative relations. Along this idea, we introduce an abstract form for quantita­ tive terms and relations as follows;

idname-k(C-name:value,· · · ,C-name:value), (1) where 'idname' takes a term 't', a literal 'rq' or a set of literals ·~. k is the identifica­ tion number though it is omitted in Table 1 for simplicity. The C-names('C-' is the abbreviation of the word 'characteristic' in this paper) are a variable 'var', a function class. 'fc'," form of a literal 'form' and a sign of terms 'sgn'. The value of 'var' is a set of variables in an ex­ pression. The values of 'sgn' are {p,z,n} and the combinations of them. The item 'form' takes the values 0,1,2 and 3 for a solution form q(x, t(var:~)), a semi-solution form q(y,t(var:{x})), a transposed form q(t(var:fx}),O) and the general f orm q(t(var:(xl ),t(var:txl)) respectively. An abstract form eq.(l) is obtained by parsing an objective expression by the aid of the rewriting rules shown in Table 1.

t(var:.,) : := const t(var : {x) ,fc: (x: {fs\)) : := fs(x) t(var: {x,y} ,fc: (x: (fsl,fs3\ )(y: lfs2 ,fs3))) :: = fs3(t(var: lxl ,fc: (x: (fsll)) ,t(var: (yl ,fc: (y:(fs2}))) t(num:2,var : {x,y),fc:(x: lfsl\ )(y: lfs2\ )) : := t(var: tx) ,fc:(x: \fsl} )),t(var:ly) ,fc:(y: \fs2})) q : : = =I >I< rq(var: lx,y) ,fc:(x: (fsll )(y: {fs2l )) : := q(t(var: txl ,fc: (x: lfsll)) ,t(var: IY} ,fc: ( y:\fs2}))) rq(num:2,var:{x,y\) .. - rq(var:(x\),rq(var:jy}) L ::=AIVIAV

Table 1. A part of rewriting rules.

In Table 1, fsl, fs2 and fs3 are function symbols, f and rq denote sets of terms and literals re­ spectively and num is the number of the elements of a set. The values of function classes about variables are polynomial 'poly', fractional 'fract' and so on. L is the abstraction of a compound logical operator.

The quantitative expressions in a given problem are reduced to three abstract forms; q(term,term ), rq(C-name :value,···,C-name:value) and L(rq(C­ name:value,···,C-name:value)). They are called the objective-based literal expression OBL, the characteristic-based literal expression CBL and the abstract compound-literals expression ACL. These three forms are cons1:ructed at the general identification and are permitted to appear in an expression as a mixed form .

In addition to the general identificaiton, sev­ ral special identification routines are imple­ mented which identifies the C-value if the trans­ f ormation rule to be applied contains a special kind of C-name such as the degree of a polynomial.

Problem descriptions take the following forms. Problems such as a proof-problem (Qx)(P(x)~R(x)) are expressed as ((Qx)P(x)l (Qx)R(x)) based on the state space representation, where Qx is a se­ quence of quantifiers and both P(x) and R(x) are predicates and called the precondition and the goal respectively. Value-finding problems are also expressed in a similar format to proof prob­ lems as follows;

( (3?x)P(x)ll (9?x)Obj (L(x=t(var:¢')))), where 'II' stands for an equivalence relation, and the goal part denotes to require an objective form corresponding to the ACL expression L(x=t( var:<P>).

3. THEOREMS .Mm TRANSFORMATION .Em

Mathematical theorems are classified into sever­ al subsets by their characteristics and can be accessed by means of a tree-like address table shown in Fig.l.

Tree 1 concerns primitive functions pf's such as addition, while Tree 2 concerns function classes fc's such as polynomials and also non-primitive functions npf's such as the absolute function. The C-item d means the domain where a theorem holds. p is the item that indicates an equality or inequallty relation. p indicates the kind of quantifiers and I is the number of literals in­ cluded in a premise of a theorem.

In addition to theorems, some relations called t transformation rules 'TR's are introduced in or­ der to find a global solving policy. There are two kinds of TRs, one of them is C-TRs and the other is P-TRs(i.e. problem-IRs). The form of a C-TR takes an implication form (Qx)(r(x)~(x)) (OP:S), where r(x) and s(x) are conjunctive nor­ mal forms of some abstract expressions of liter­ als. The symbols 'l:s' and '1.' represent probable relations. The OP part indicates location areas of supporting theorems, TRs or procedures of the TR. Some of the TRs are shown in Table 2.

Table 2. Transformation rules.

The universal quantifier of TRs are omitted for simplicity. The logical connective symbol L, the predicate symbol q and the variable symbols x and y in the TRs are variables for which any corresponding instance or variable can be sub­ stituted. The predicate symbol q denotes equal­ ity or inequality. TR d) means that a polynomial relation will be reducible to a combined logical form which consists of several linear or quadrat­ ic relations. TR al suggests that a polynomial term will be factorized into several linear or quadratic terms by a procedure. TR ® shows an absolute inequality which contains quadratic terms about a variable can be transformed to a sum of definite sign terms such as definite pos­ itive terms 1 where TH (j) and TH ~ are

a%0+a*x**~+b*x+c=a*(x+b/(2*a))**2+c-b**2/(4*a) and

a>0Ac-b**2/(4*a)~O

~(V x )a*( x+b/ ( 2*a) )*·~2+c-b**2/( 4*a )?;;0 respectively. In P-TRs, the symbols Q,Q1 and Q2 are variables for which any logical formula can be substituted. The symbol T denotes a tautology such as t(sgn:p )>0.

The access to TRs is performed by the aid of a tree-like address table a part of which is shown in Fig.2.

In the address table, the items d,R and fc have the same meanings as in Fig.l. The value C de­ notes the complex number domain, while R denotes the real number domain. fO,fl and f2 mean I=O, J=l andll2 respectively. A TR with J=o is a no­ premise relation. The value g of the item fc de­ notes the general-function class. 'A' indicates the abstraction levels of premises of TRs. If a TR involves several literal expressions of dif­ ferent abstraction levels, its address is rec­ orded at the respective abstraction levels .

The following describes the main part of appli­ cation procedures of TRs to the conjunctive normal form of the precondition of a problem. At the first step of application procedures, if the abstraction level of a TR is lower than that of a problem, the abstraction level of the TR is rai s ed to that of the problem by the identifica­ tion of the TR, otherwise the usual unification algorithM is adopted. Let P,'A · · ·AP,.' ···(a) and !1.11\· · ·AP&,.-.Q· ··(b) be a precondition of a problem and a TR respectively, where P' means an instan­ tiation of P and {il,· · · ,im) is a subset of {1,· · · · ,n], then the result of the application of (b) to (a) is P,'A · · ·J\P,.'AQ'. If the implication sym­ bol is replaced by the equivalence symbol in eq. (b), 111 ,···,ij~ are removed from the result.

4. SOLVING PROCEDURES

The solving procedures of EAPS are divided into three phases;(i)the identification of the current problem at the three abstract levels, ACL, CBL and OBL,(ii)the breadth-first search of a rele­ vant global solving policies by the aid of the tree-like address table and (iii)the depth-first solving in a concrete form a~cording to the sug­ gestion of the obtained global solving policies. A part of a solving tree generated by EAPS is shown in Fig.3, where the forms of PB, PBi and PBf are (PIG), (PIQ) and (QIG) respectively.

The global solving pol­ icies are placed in the ascending order of the difference between the precondition and the goal of PBt which is eval­ uated based on the assigned values to the fundamental C-items.

Fig.3 A part of a solving tree.

If no global solving policy is found, EAPS search­ es applicable theorems by the aid of the tree-like address table of theorems. If EAPS fails to find applicable theorems, it applies P-TRs to the cur­ rent problem then retries to solve the problem.

[Example] 'Prove that if k is a real number, the equation x*~2-2~k~x+2~k-2=0 of x has real roots'. The expression of the problem is

Since there is no applicable TR or TH to the pre­ condition of eq.(l), the problem transformation is tried. The application of P-TR 0) to eq. ( 1) yields

( (~k) (3 x) (-vk~Rvroot ( var: x ,rel: x'"'2-2*k·~x-2*k2=0)C:R~T). (2)

After finding no applicable TRs, one candidate of applicable theorems

(3x) (root ( var: x ,rel: a*x*~2+b~x+c=O )CR) it blh'·2-4*a''cl0

is found from the address area fc:poly-d : real-p:

nq-q:V-J:l involved in the address table of THs. The application of the above theorem to the pre­ condition of eq.(2) results in

( (\fk )--.kERVk·h~2-2>'·k+2'10h~o) .

( 3)

The CBL form of eq.(3) is

( (Vk) ... kERVrq-3·2(var: lkl,fc :poly)\\

The numbers 3·2 and 3·3 in eq.(4) denote the sec­ ond and the third literals of eq.(3) respective­ ly. The candidates of applicable TRs are (D and ®. The application of TR Q;l fails in the adop­ tion of TR Q) which is suggested by TR@. The ap­ plication of TR 0} to the OBL form of eq. ( 3) re­ sults in

((Vk)~keRV~(~(t(sgn:pz,var:lkl)),O)

ll~(t(sgn:pz),O)).

The application of the theorem TH Q) suggested by TR@ to eq.(3) leads to the result;

«Vk) ... keRV(k-1)*·~2+noDno). (5) The highest level of abstraction of applicable TRs to the precondition of eq.(5) is OBL, that is;

((Vk)~k,RVq-5·2(~(t(var:lkl,fc:poly,sgn:pz)), 0 )I\ ~ ( t ( sgn: pz), 0)) . ( 6)

The number 5·2 denotes the second literal of the precondition of eq.(5). The application of TR~ to the precondition of eq.(6) yields

( (Vk )-~RV~( t( sgn: pz) ,0 )II~( t( sgn: pz) ,0)) which leads to the completion of the proof.

6. CONCLUSION

The first version of EAPS[3] imple~ented on a mini-computer in an assembly language solved problems such as those which involve a simultane­ ous linear equation symbolically in about ten seconds. The new EAPS with additional facili­ ties presented in this paper is under develop­ ment on a computer with a 768 kB memory in LISP 1. 5.

ACKNOWLEDGMENTS

The authors wish to thank Mr. K.Imori for his help in the implementation of EAPS.