Theoretical Basis for a Knowledge Representation System

1. INTRODUCTION

A system named the SBDS (Structure Based Deduction System) including a formalism for representing knowledge and an inference algorithm is presented. It is a subsystem of a total knowledge system named the KAU (Knowledge Acquisition and Utilization) system that is designed as an intelligent interactive system intended to support man's intelligent activities such as engineering design, decision making, scientific research and so forth. Thus the motivation for the research resides in what is called the intelligent agent view point by

E. Feigenbaum [6].

SBDS adopts, as its basic framework for representation of knowledge, an extended form of the first order predicate logic, because it is, we think, suitable for converting to and/or being converted from any of three major forms of information used in computers today, i.e., (1) languages, (2) databases and (3) programs. In this paper, relations of (1) and (2) to SBDS are discussed. That of (3) to the first order logic has been discussed in [5] and [10].

As a matter of course, a knowledge system is required to have high expressive power in repr ~sentation of knowl~dge. Though there have been some approaches adopting the first order logic in AI problems [5], [7], [10] and also in the mor e prac tical problem of databases [3],[9], the first order logic shows a shortage of expressive power for many real applications. The adoption of the higher order logic in its general form [8] as the main framework instead of the first order logic, however, is not good solution because it is too a general form for the practical purpose and therefore the inference is inefficient to be used in a real environment.

We therefore adopt a simpler form that is obtained by defining, first, a formalism to define the predicate and a deductive inference algorithm and, then, extending the first order logic towards higher order within the framework until the extended form can accommodate .most of the language expressions that are almost sufficient to represent knowledge in many applications. The formalism for defining the predicate is combined with the hierarchical structure of entities defined in the universe. A fast deductive algorithm has been developed so as to use effectively the property of the

structure.

On the other hand, for users working in the real applications, the use of databases is becoming inevitable. So far a number of databases and their management systems have been developed [4). These DBMS's, however, are very inconvenient to be used for such the intelligent works as mentioned above . For an engineering designer, for example, the objective is to reach a final model through the repetitive processes of a model construction and its evaluation. He will require the data structure to be dynamically managed. But the conventional DBMSs can hardly do so because in these systems the structures of data are almost fixedly defined. Therefore it is desirable that the knowledge system takes over the dynamic restructuring of information and can accesses to databases only when the values of data are necessary. SBDS possesses such the capability. Thus the KAU of which the SBDS occupies the central part is intended to serve as an intelligent interface between users and DBMS's [12], [13].

A number of different approaches have been made and have also been developing for the problew of knowledge representation [1], [15]. The approach ~reposed in this paper is still different from them as seen from the system's point of view though it implies some concepts common to the others in part. Theoretical basis of our approach is on the first order predicate and the resolution principle [2],[14]. However as the SBDS also contains the concept of network, there are also some ideas in common between our method of deductive inference and methods developed for performing deductive inference on the knowledge represented in the network [15].

In this paper, we describe the SBDS with its mathematical foundation. A universe is defined as the collection of all concepts that can be referred through the language. Over this universe, the first order.logic is defined and then extended toward higher order to the limited extent. A classical predicate logic is used rather than the resolution logic not only because it is intuitively understood by many people but, rather, because it is convenient to extend the first order logic and also to convert the predicates to the database operations.

An inference algorithm has been developed in which the information contained in user's query is effectively used for searching information and for deduction. The algorithm is also applicable to the extended form by slightly modifying its control mechanism.

2. INTERFACE TO LANGUAGE FOR EXPRESSING KNOWLEDGE

A problem world is described in many cases by means of language, and, therefore, we consider only the world that is describable by the language.

In reality, a vocabulary allowed to be used in the knowledge system is finite in which some words, -nouns- designate sets of entities or individual entities while the order words -verbs, adjectives, propositions, some nouns, etc.- represent the attributes of entities or the relations amongst entities. We call the former the entity words and the latter the relational words.

The syntax of the language defines sentences. There are a set of basic patterns of sentences or basic sentences in short such that all sentences can be analysed to the combination of some of them. If a system can understand the meaning of each basic sentence and also is given a parsing algorithm for analysing the compound/ complex sentence to the logically connected set of basic sentences, then the system can understand the language. Here, by the term "understand" we mean that the system can process the information given in the form of language based on its meaning so that it responds correctly to users requests.

The set of basic patterns of sentences is finite in ordinary languages. In this paper, twenty-five patterns as shown in Table 1 are considered almost enough in case of English for expressing knowledge used in most of applica­ tions.

The vocaburaly, on the other hand, is different in every application. Though some common words can be defined independent of applications, some jargons are to be added in each applica­ tion. Therefore the dictionary in the system must be an open set.

3. DATABASE

A relational model is considered exclusively in this paper [3],[4] though the system is not restricted to it. In this model a relation is defined as a set of n-tuple records, (t1, t 2 , ···, tn), where ti is an occurence value in the domain Ti. A relation is represented in the form of a flat table with n colums and a relation name is given to it.

4. FIRST ORDER PREDICATE LOGIC IN ~ CLASSICAL FORM

In the classical predicate logic, an atomic formula or atom in short, is defined as F(t1, t 2 , ···, tn) where F is ann-place predicate symbol and t 1, ···, tn- 1 and tn are terms. Then a well formed formula, or a formula in short is defined recursively as follows [2]

• a . An atom is a formula.

b. If F and G are formula, then -F, FUG, F n G, F + G and F#G are formulas where .-, U, n, =t and ~ are read as "negation", "disjunction",

"conjunction", "imply" and "equivalent" respectively.

c. If F is a formula and x is a free variable in F1 then (Vx)F and (3x)F are formulas.

1. Formulas are generated only by a finite number of applications of a through c.

A formula can be written in the prenex normal form. In the following, it is written in a vector form as :

(~x)(S{Fi(Xi)}J. -(1) whe re ( ~x) = (Q1x1)(Q2x2) · ·· (Qnxn) with each Q· being either V or 3, S{ } stands for a l~gical structure composed of atoms, Fi,(i=~ .. ··m), by means of logical connectives shown 1n the above definition of the formula, and (xi) = (xi · · · Xini) ·

In the resolution logic [21,[41, the formula is standardized by being converted to the conjunc­ tive normal form and Skolemized. In this paper, instead of the standardization, the formula is modified in another way.

Firstly, no function symbol appears in the formula. In general, n-place function is a mapping from on to D where D denotes a domain of a variable. It is represented in the SBDS by an n+l-place atom *Ff(z;x1 ··· Xn) that is defined true iff f(x1 ···xn)=z holds. Since to each of this kind of atoms corresponds a proce­ dure that evaluates it procedurely, these atoms are called the procedural type atoms. The pro­ cedural type atom is identified by a symbol * on the left shoulder in the paper. An example is, *(ADD 5;2 3):"2 plus 3 is 5".

Secondly, in the resolution logic, Herbrand universe is defined as a set of which the ele­ ments are generated successively by means of the constants and function symbols appearing in the formula(s) while, in the SBDS, the universe v is first defined as the set of all objects that can be referred by the language.

Thirdly, the concept of sets is explicitly included in a formula. In the following, a variable free formula is called a ground formu­ la. Any subset I of the set of all ground atoms, F(t 1, ... , tn), of which t 1, ... , tn are in the universe determines an interpretation where the meaning of an n-place predicate symbol F is a n-ary relation over the universe : {(t1, ... , tm):F(t 1 , ... , tn)EI}. I is said to be a model of the formula if the truthhood of the formula is determined by the rules : F is true iff F f I and ..... F is true iff F, I. When I is a model, the set of the tuple {(tl, ···, tn)jF(t 1 , ... , tn)fl} is denoted Dr. ThenF(x 10 .. . , xn) is true iff (x 1 , .. ·, xn) f Dr. This fact is written as

(Vli!)[(Dr3x)~F(~r)1 where x=(xp ···,xn)--(2)

In many cases, Dr is a Cartesian product of Xi, (i=l, 2, ... , n), i.e., Dr=X1x ... KXn where each X· denotes a domain of the variable Xi· 1 . In this case, the formula (2) is rewr1tten as (Vx 1 ) · · · (Vxn) [ (X1 3 x1 )() · · ·() (Xn 3 xn) =}F(x,, · · · , Xn) 1 - - - (3)

or, equivalently,

(Vx1 ) ··· (Vxn)[X 1 *(x 1 )()···(\Xn*(xn)~F(x 1 ,

... ,xn)1

---(4)

where Xi *(xi) is a predicate meaning "Xi 3 Xi" · On the other hand, a fact that F(xl, ·· ·, xn) is true for some value (t,, · · ·, tn) in Dr is written as

(3x}[ (DO x) n F(x) 1.

- - - (5)

If Dr is a product set, then

(3x1) · · · · (3xn) [X1 *(x1 )n· · · n Xn*Cxn)n F(x 1 ,

.. · , Xn) 1.

(6)

If both V and 3 appear in a formula, then a recursive relation is obtained: (Q, x, ) · · · (Qnxn) [ (X1 *(x,) ~ (X2*Cx2) 2< · · · ~-f'Cxn·t)

fi-, (Xn*Cxn);F(x 1 , .. ·,xn)) .. ·)1 --- (7) where r represents either~ or n depending on Qi being V or 3. For example, if Dr=X" Y " Z, Qx=V , Qy=3 and Qz=V , then (V x) (3 y) (V z) [X*(x} ~ (Y*(y) () (Z*(z)

::? F(x,y,z)))1

- (8)

In these representation of formulas, each vari­ able is defined over V of which Xi,(i=l,··· ,n), is a subset. Then the formula can also be written in an abbreviated form as (Q 1x/X 1 )···(Qnxn/Xn)F(~ ,···,xn) - (9) meaning that the formula is true for assignment to each variable Xi of all or some values of Xi depending on the quantifier Qi being V or 3 , but otherwise it is not true. It is further simplified by abbreviating the variable symbols and moving F into the parenthesis as (Q1 X1 )·"(QnXn)(F,~, ... ,Xn) -- -(10)

With this formalism, (2) and (5) are written as (VDr)(F Dr) and (3Dr)(F Dr) respectively. A ground atom (F, t 1 , · · ·, tn) is a reduced form of (9) in which every domain has only one element. It shoud be noted that the formula (10) can be transformed easily to a set-of-clauses form of the resolution logic. Example:

(V X)(3 Y)(V Z)(F X,Y,Z}=(V x)(3 y)(V z)[( -X*(x) U (Y* (y)(l (-Z* (z) U F(x ,y, z)))) 1 = (""X*(x)U Y*(f(x}) n (~X*(x) lJ-Z*(z) VF(x,f(x) ,z)= { Ct,C2} Ct=-K*(x),Y*(f(x)), C2=~X*(x),~Z*(z), F~x,f(x),z) -- -(11) where f(x) is the Skolem function.

The general form of the formula, then, is (() X) [S I { (Fi X)} l - (12)

5. THE UNIVERSE AS AXIOMATICALLY DEFINED SET

A predicate symbol of a formula corresponds to a relational word in a vocabulary set. Let the simple collection of all predicate symbols be R. Then since the vocabulary is a finite set, R is also finite. Each Fi in R acts on U to define a basic pattern of atomic formula of which the predicate symbol is F1. In other words, to each Fi, an ordered set {t1 ,···,tni} is specified where each ti is in U such that the ground atom (Fi t 1 ,···,tn~ is in a model I.

The universe U is not so simple as R. Many dif­ ferent types of elemenumust be included in U. Consider, for example, two atomic formulas; (FATHER t1,t2):t1 is father of t2" and (CARD-NO t3,t4):"cardinal number of t3 is t4". Both t 1 and t2 are of the same type in a sence that they can be the elements of a set, say, PERSON. On the other hand, t3 is a set while t 4 must be an integer. In this case t) is said being of the different type and is one level higher than t4. Each ti in an atom can be of the different level as was seen in the case of CARD-NO.

These examples shows that any set of the ele­ ments in U must be an element of U too. Each predicate symbol specifies the level of each term to be an argument of the ground atom. Such a .term is called a ground term for the atom and a symbol # is attached in the following.

On the other hand, in the atomic formula (10) defined as the collection of all ground atoms, Xi is a set of ti's, and · therefore is an element of V that is one level higher than ti's. Thus an atom and its ground atom are defined over two levels of elements in U for each argument.

This definitions of formula requires the uni­ verse U being of multi-layersstructure. For example, the concept of the power set is neces­ sary to represent a formula such as : (VT 3 )(3 INTEGER)(CARD-NO T 3 INTEGER)?:"For every set is there an integer which is the car­ dinal number?", where T 3 is a set of all sets. Fortunately such the set has been studied as an axiomatic set theory. We can use the Zermelo/ Frankel axioms of set theory [11] as the uni­ verse though we don't touch on them here. We only point out that the set thus defined satis­ fies all conditions mentioned above U and, still further, such the set contains n-tuples, (t 1, ·· ··tn) too, as it elements.

Based on this structure of the universe, a simple formalism for defining formula is obtained. That is, a formula is a pair (Fi Dr) attached by the information for quantification, ~ where Fi€R and D 1 is a mapping of Fi into U.

6. INFERENCE ALGORITHM

Inference algorithm is defined to the formula in the form of (12). This algorithm is logi­ cally equivalent to the resolution principle [2] but is designed to have high physical per­ formance. It consists of the selection rule (SR), the test for implicative condition (TIC) and the replacement rule (RR). TIC corresponds to the unification algorithm and RR the resolu­ tion in the resolution logic respectively.

Suppose a formula P of the form P : (flpX) [ (BI, X1 )n · · · n(Bk, X k) ~(A, XJ J- - (13) exists in the knowledge base where (QpX) = (Qp 1 X1) · · · (QpmXm), X;!.= {Xi 1, · · ·, Xi a!} and X= {X1, · · ·, Xm} = i~ 1 X'i, and a query Q of the form Q: (QqY)[(C1, Y 1 )() ··· n(c1 , Y1)J -- -(14) is pre sen ted where (Qp'f) = (Qq 1 Y 1) · · · (Qqn Yn), Yj={Yj~o ···, Yj8j} andY={YI,···,Yn}= jt\].

Then a non-procedural type literal Cj is se­ lected from Q by SR and the relation (~'p X 0 )(A, X0 ) ~ (Q'q Yj) (C~ Yj) - - -(15) is tested by TIC where (Q p 1 0 ) and (()'q \' j) are the partial sequences of (Qp X) and (()q \') com­ prising only the variables included in Xo and Yj respectively. Implicative condition (15) is tested by the following two steps:

• (A) For each pair of corresponding variables, say Xpi and Yqi, of left hand term and right hand term of (15), either of the set theoreti­ cal relations shown in Table 2 should hold de­ pending on the combination of quantifiers of variables. This rule applies to all variables in the atoms of (15).
• (B) There should not be such indices pair (i,j) that, in (fl'p X 0 ) (A, X0 ), i-th variable is uni­ versally quantified and is preceding to j-th existentially quantified variable while, in (Q'qYj)(Cj, Yj), corresponding i-th universally quantified variable is preceded by j-th exis­ tentially quantified variable.

If the implicative relation (15) is certified by TIC, then a new formula R of the form R: (flrZ)[(C1, Zl)n···()(Cj-1, Zj-J}()(B1, W1)n·· · ·f'\(Bk, Wk)()(Cj+l, Zj+l)()· · ·n(Cl, Zl)]- -(16) is ~enerated ~y ~R ~~~re ~Q~ Z) = <Q_qZ1) ·::. (Qn Zn), Zj-{Z1, , ZJ~J}, 1Wi-tWil·k , Wiai}, and Z={Z1, ···, ZvJ=(.V Zi)V( .VWi)· Each Zi and its quantifier Qi l~jdecided 1 b~ its corresponding variables, Xi and Yi, in P and Q

respectively, and their quantifiers as shown in Table 3.

It is not difficult to show that above rules of TIC are equivalent to the condition for the unification algorithm to terminate successfully in the resolution logic.

The set theoretical relations appearing in Table 2 can be represented in the logical form as

(X:>Y)=(Vx)[Y*(x) -tX*(x)]

-- -(17)

(X,\Ytlcp) =<:!!z) [X*(z)"Y*(z)]

- - - (18)

The relation (15) is proved by showing that

the negation of the relation, i.e.,

..... [(~'pX~~(A Xo) "(~'QYj)(Cj Yj)]:: (Q'pXo)(A,X0 )

A(QqY)""(C·, YJ -- -(19) does not hold w~ere ~q is obtained by exchang­ ing V and a of each Qqi in ~'q· (20) is trans­ formed to the set-of-clauses form. Let it be denoted S. S is different to each assignment of quantifiers to variables. To avoid the no­ tation becoming too complicated, let's pay an attention for a particular pair of variables (Xi, Yi). The quantifiers of (Xi, Yi) is de­ noted (Qpi· Qqi). Then four different forms of S are derived according to the different specification for (Qpi. Qqi). Then the validity of conditions listed in Table 2 is tested by ap­ plying a refutation process to these conditions combined with S. Here, only a case, (Qpi· Qqi) =('v',a), is shown.

In this case, S={ .. ·, -X*i (xi), .. ·, A( .. · Xi · . .. )}, { ... y*iUyi(*))···}, {""Cj("·fyi(*)···)·· .. } where··· represent terms concerning to variables other then Xi and Yi· f(*) ·is a Skolem function where * represents a set of universally quantified variables preceding to Yi in the prefix ~q Yj).

These set of clauses are put together with (17) in the standard form, {~Y*(x), X*(x)}. Xi can be substituted by fyi(*) because by the second law of TIC it is ensured that * does not in­ clude xi. Then A(··· Xi···) and C(··· fyi(*) ···) is unifiable if A and Cis the same. Thus it is easy to show that the empty clause is deduced from the set of these clauses. The other cases are also proved by the similar pro­ cedures.

Example :

[ P: (VX)(VY)(VZ)[(BROTHER X Y)n(PARENT Y Z) ~ (UNCLE X Z)] "For every x, y, z, x who is brother of z's parent y is z's uncle" Q: (aU)[(UNCLE U IITom)n(ILL U)]? "Is there any uncle u of Tom, who is ill?" where X, Y, Z and U represent the set PERSON and xEX, yGY, z~Z and utU.

At the deduction SR selects (aU)(UNCLE U IITom) from Q and TIC tests for (VX)(VZ)(UNCLE X Z) ~(aU)(UNCLE U /ITom) - -(20) It holds because XAU~~. Z~{IITom}. Then RR

generate,

R: (aU)(aY)[(BROTHER U Y)~(PARENT Y IITom) I"'(ILL U)] -(21)

R is regarded as a new query.

The deductive procedure is repeated until ei­ ther the formula of which the Boolean value can be obtained or the formula consisting only of the procedural type literals is reached. Fur­ ther consideration is necessary to make the algorithm logically complete though it is ab­ breviated here. Refer [13] for the detail .

7. STRATEGY FOR SEARCHING THE CANDIDATE FORMULA - -

There may be a number of formulas stored in a knowledge system and, at a time only part of which participate to deducing the query . Therefore, quick selection of the relevant for­ mula is very important.

The universe is represented by a hierarchical structure in which each node represents a set of objects. In the following a set is denoted by the upper case letter. A node is connected to another node by either of two types of arcs representing the set--theoretical inclusion and disjointness. The former is called the !-type arc and the latter the D-type arc. For in­ stance, the set LIVING-THING(LIVTH in short), MAMMALIA, FISHES, BIRDS, MANKIND, DOGS,CATS etc are in the set-theoretical relations such as LIVTH~MAMMALIA, FISH, BIRD, INSECT,··· MAMMAIL :>MANKIND, DOG, · · · and so on. We say "X is upper to Y" or "X is larger than Y" when X:::>Y and Y is connected to X by the !-type arc. On the other hand, the set MAN and WOMAN are dis­ joint to each other and are connected by the D­ type arc. By applying the processes of linking by means of these arcs successively, a hierar­ chical structure of universe, called the seman­ tic skeleton structure, or the skeleton in short, is formed. Some node is connected to more than two other upper nodes by the !-type arcs. Such a node represeuts a set defined as an intersection of the other sets. For in­ stance, a set BOY is represented as the inter­ section of MAN and CHILD.

A formula that includes a set Xi as an argument is linked to the node Xi in the skeleton and is accessible from this node. Accordingly the formula (10) can be accessed from any of nodes X I' X2, . · ·, Xn ·

Suppose a query (14) includes a constant or a variable, say Yj, that is universally quanti­ fied. It is orainary the case because a query of which every argument is existentially quan­ tified variable is nothing else but a damp com­ mand. Then the formula P that satisfies the relation (15) to this query, if any, must be linked to some node Xj that is over Yj in the skeleton from the rule (A) of TIC. Therefore, it is reachable by following the !-type arcs upward starting from Yj. Since the skeleton expands downward, it reduces the search space considerably and formulas of which the predi­ cate symbols are the same with the query but the variables are out of above condition are disregarded.

The formula thus found is called the candidate which satisfies the condition of TIC only with respect to the variable Yj. It must be tested for the condition (Table 2) for the other vari­ ables too . The skeleton is used again. Since, this time, both left and right hand formulas of (15) are in hand and, therefore, both domains ( sets) of corresponding arguments can be speci­ fied in the skeleton, the tests for the set theoretical relations of Table 2 are achieved by the test for the positional relations be­ tween nodes in the skeleton. Since its algo­ rithm is very simple it can be implemented by the special but simple wired logic and there­ fore the test can be performed very fast. The SR selects a literal among all literals in the query that contains most constants I universally quantified variables.

The system further reduces the possibility of fruitless test being achieved. In case of con­ ventional first order logic, the set of formu­

las such as

B1 ~A, B2 '+A, · · ·, Be '+A - - -(22) often arises in the definition of the meaning of words. For instance, the relations between sets mentioned above are represented as (Vx) [MAMMALIA*(x) ~LIVTH*(x) 1}

(Vx) [BIRD* (x) ~ LIVTH* (x) 1

(Vx) [FISH*(x) ·HIVTH*(x) 1

- - -(23)

Suppose A ~Q is satisfied to a query Q. Then the resolution logic will make an exhaustive test looking for a path leading to the empty clause. It is exhaustive because the refuta­ tion process proceeds in the direction from A to Bi in each formula (22) in a sense that A is unified with the query and Bi is remained for

the next test.

In the SBDS every formula of the type(23) is represented by an arc in the skeleton. Search­ ing the formula by following the !-type arcs upward in the skeleton corresponds to searching the refutation path proceeding in the reverse order of the resolution logic. Thus, as far as such the formulas as (23) are concerned, the

exhaustive test is avoided.

8. ACCESS TO DATABASES ----

The formula (2) means that if a tuple x=(x1, ·. ··, xm) is included in D, a relation F holds among X!, ···, Xm· Suppose then that a set of n-tuples, D, is given as a data file in a table form. Then, the condition (D~&) for some n­ tuple, t=(tJ, ···, tm), is tested by a special procedure that searches t in the file. That i~ the premise of (2) is represented by a kind of procedural type atom. Let it be denoted as *(FGET, D:x1, ···, xn) and be called the file type atom where D indicate the file name. Then the formula (2) is written as

(VX1) · · · (VXn) [*(FGET D : X1, · · ·, Xn) ~F(X1, · · · , Xn) 1 - - - (24)

This formula gives a definition/description of a table type file D. A user input the system a set of data in the table form accompanied with a formula (24). After then, any user can use this file without any knowledge on it. The system determines itself how and when to access the file through the deductive operation and converts the formula to the relational algebra (4]. Only the outline of the conversion is shown without proof.

Suppose, a formula consisting only of the file type atoms.

(Q X) [S{*(FGET Di: Xi)}] -(25) is obtained as the result of deductive opera­ tionkwhere Xi=(Xi 1 , ···, Xini) and X=(X1, ···, Xn)=i¥JXi. Suppose each file Di is the set of mi-tuples and each domain Xi is a finite set. Let Xi*=X-Xi. Then (25) is equivalent to (Q X)[S{*(FGET Di·Xi*: X)}]=(Q X)[*(FGET, S{(Di xXi*)}, X)] -- -(26)

where Di·Xi* means a cylinder set in the n-di­ mensional space, X1 lt · · · x Xn, S is a structure of the set theoretical operations that is ob­ tained from S by replacing every A and U in S by A (intersection) and V (union) respectively, and S{(Di~Xi*)} means that the structure of the set operations S are applied to (DiXXi*). Since all the (Di~Xi*l's, (i=l, 2, ···, k), are the set of n-tuples, S{(Di(Xi*)} is reduced to a set of n-tuples. Let it be denoted P*. Then the formula (26) results in

(~ X)[*(FGET D* :X)]

-(27)

Here the following two file operations are introduced.

DIV(D*, X~)={x=(xJ, ···,Xi-!' Xi+I· ···, Xn)l

lCXXiCD*}

- - - (28)

PRJ(P*, Xi)={x=(xJ, · · ·, Xi- I, Xi+J, · · ·, xn) I

(XJ, ····Xi-1, Xi, Xi+!, ... , Xn)cD*}- -(29) These operations correspond to division and projection operations respectively of the rela­ tional algebra in the relational data base. Then the following relations between logical view and set-theoretical view hold. (QJXJ) · ·· (Qn-JXn-J)(VXn)[*(FGET D*: X~o

···, Xn)J=(QJXJ) · · · (Qn-JXn-!)[*(FGET

DIV(D*, Xn):X!, ... , Xn-d]

(30)

(Q1X1) ··· (Qn-JXn-J)(3Xn)[*(FGET D*: X1,

· · ·, Xn)J=(QJXJ) · · · (Qn-JXn-d [*(FGET

PRJ(D*, Xn):X!, ···, Xn-d] These relations and operations are repeatedly applied to the formula (27) until finally *(FGET T : ~) is obtained where T is either 1 or 0 depending on if the operations can be con­ tinued to the end or these operations result in an empty file. If T=l, the original query for­ mula proved true.

In practice, user must be able to designate some data to be output. Such the data must be saved during the above processes. When the other procedural type atoms besides the file type are included in a formula, a further con­ sideration is necessary. For the details refer [13].

9. EXTENTION OF THE SYSTEM

9.1 Predicate Symbol as Variable

A hierarchical structure can be introduced in the set of predicate symbols. Consider, for example, two atoms, (BROTHER X Y) and (SIBLING X Y). When the same terms are substituted into the corresponding variables, then (Brother, t1, t2)*(Sibling, t1, t2). In this case "Sibling" is said larger than "Brother". On the other hand, (Natural, X )()(Artificial, X ) shows an inconsistancy. The predicate symbols being in such relations are said disjoint to each other. Based on these relations, the skeleton is formed for the predicate symbols and the predicate symbol can be dealt with as if it were a variable because it can be pro­ cessed by the same algorithm as the other vari­ ables at the deduction. Then the atom can be rewritten as

(QX)(X), X=(Xo,X!,: .· ,Xn) ---(31) where the predicate symbol is denoted Xo. With this modification, the system can accept the query which asks the value in X0 , i.e., the predicate symbol. For example, a query Q: ( 3 RELATION) (RELATION {/Tom #Mary)?: "What is the relation holding between Tom and Mary?" can be answered by using P:(FATHER 1/Tom #Mary) if the relation FATHER=RELATION is given in ad­ vance as is the case of the other variables.

9.2 Recursive Form

Let the atom of the form (31) be called the n­ atom when it comprises n terms including X0 · In ordinary predicate, n is larger than or equal to two. Suppose it can be extended to the case n=l. There are only two 1-atoms of the form, (V X)(X) and (3 X)(X) with meanings "for all xEX, xfX" and "there is some x in X such that xEX", respectively. Thus (X) shows the logical aspect of the set X. The applica­ tions of TIC rules to the 1-atoms reveala the rule (A) of TIC being just the implicative con­ dition itself for two 1-atoms.

The SBDS has been described as including the concepts both of sets and of logic. It is for the purpose of taking advantage of the strength of each at the implementation. We can obtain the logical description of it by replacing X by (X) and the rule (A) of TIC by the implicative relation between 1-atoms. Then the universe is regarded as a collection of 1-atom'formulas and the formula (31) is rewritten as the relation among n 1-atom formulas to which the rule(A) of TIC, rephrased as the followings, is applied: (A') To each pair of corresponding inner 1atom formulas, the implicative condition should hold.

These concepts are extended. Assume that the universe can include not only !-atoms but gen­ eral formulas, by adding all possible formulas definable by Rand U to U resulting in U1, then by adding all possible formulas definable by R and U, to u, resulting in U2 and so on. For many applications the extended universe Uk with finite K may be enough. The mechanism for de­ fining the atom (ref. Sec.5) is unchanged. Then the SBDS has atoms in recursive form as ((FML)*o,(FML), ... (FML)n) -- -(34) where (FML)~ denotes a 1-atom corresponding to the predicate symbol and (FML)i,(i=l, ... , n), is a formula. The rule (A') is extended to : (A") For each pair of corresponding inner for­ mulas, the implicative condition should hold. The rule (A") is applied recursively to the formulas in form of (34) at the deduction.

As the result of this extention the SBDS ac­ quires a large power of expression. But the extension is based on the assumption that any 1-atom formula can be replaced by a general formula. Further study on its validity is nec­ essary. ·

Example: (VX)(VU)[(INTEND X (DO X U))O(CAN X(DO

• X U)) ~(DO X U)] :"Every one does thing if he intends to and can do it." where X;PERSON, U;UNIVERSE,

(CAN X (DO X U)) : X can do U, (INTEND X (DO XU)) : X intends to do U.

10. CONCLUSION

An outline for the SBDS, a central part of a knowledge system (KAU) designed as an intelli­ gent support system, has been presented. Math­ ematical foundation for the formalism for re­ presenting knowledge, the deductive algorithm and the interface with databases has been main­ ly described. The major emphases on the SBDS design are : (1) high processing efficiency, (2) high power of expression so that user can represent any knowledge he wishes and (3) easy access to databases. The core of SBDS has been implemented and is being tested for its useful­ ness.