The Q* Algorithm - A Search Strategy for a Deductive Question-Answering System

1. Introduction

The purpose of this paper is to describe an approach for bringing semantic, as well as syntactic, information to bear on the problem of theorem-proving search. The approach is embodied in a search algorithm, the Q* search algorithm, developed to con­ trol the search in an experimental theorem-proving­ baserl question-answering system. This system, termed the Maryland Refutation Proof Procedure System (MRPPS), llcOrpJrates both the Q* algorithm which performs the search required to answer a query, and an inferential component which performs the logical manipulations necessary to deduce a clause from one or two other clauses.

The inferential component of MRPPS provides a yariety of resolution-based inference rules. For a given query, a user may select one, or a combination of the following inference systems : unrestricted binary resolution with factoring, set-of-support, input re­ solution, Pl-deduction, A-ordering, paramodulation, linear and SL resolution. A MRPPS user may also select certain search options that are available in the sys­ tem.

The clauses from the negation of a given input query and trose in the MRPPS data base together with the selected inference system define a search space

THE (2* .1\UDRITHM - A SEI\.RCH STRATEX:;Y FOR A

DIDU:::TIVE QUESTION-ANSl·JERING SYSTEH

by

Jack Minker Daniel H. Fishman James R. '1cSkimin

The University of Maryland Computer Science Center college Park, Maryland 20742

which is a directed graph wl'nse nodes (states) are (labeled by) clauses. The initial states are nodes labeled by clauses from the negation of the query, and a goal state is a node labeled by the null clause, D ·

The Q* algorithm generates nodes in the search space, applying semantic and syntactic inforrration to direct and limit the search. This paper is restricted to a discussion of the Q* algorithm: . For a detailed description of the algorithm and of the entire MRPPS system, see Hinker , et al. [1972). 1 An overview of MRPPS and of its inferEftial component may be found in Minker, et al. [1973).

The Q* algorithm has been developed for eventual use in a question-answering system of practical scale. Such a system w::>uld have a "large" number of axioms stored in its data base. A substantial majority of these axioms w::>uld be fully instantiated unit clauses, termed "data axioms ." The remaining axioms, called "general axioms," define the predicates used and their interrelationships. One w::>uld want such a system to be very restrict.ive in permitting axioms to enter the search, in order to limit the number of I/O accesses to the data base as well as to avoid clause inter­ action and merrorv clutter. In addition, one w::>uld want to be able to answer simple questions simply. An effective theorem-proving search algorithm for a question-answering system should generate the search space by: (1) selecting only those axioms from the data base that are relevant to the query, such that the "more promising" ones enter the search first; and (2) deducing clauses from clauses already generated in as optimal an order as possible.

Both of these problems are handled in the Q* algorithm. The algorithm is subdivided into two dis­ tinct but cooperating subalgorithms: the base clause selection algorithm which handles the first problem, and the deduction algorithm which handles the second problem. The base clause algorithm uses primarily semantic inforrration, while the deduction algorithm uses primarily syntactic inforrration.

Before discussing the algorithm, we review some of the background which precedes the present w::>rk and uron which this w::>rk has been based.

2. Background

There has been a great deal of research in mech­ anical theorem-proving since the r3solution principle was introduced by Robinson [1965). M:Jst of the re­ search has been centered on developing refinerrents of resolution which reduce the size of the· search space. However, relatively little w::>rk has been reported in

developing improved search st(ategies or using seman~ tics for theorem-proving s~stems. (We have recently learned that Reiter [1972) is attempting to inconx:>rate semantics with a theorem prover by the use of rrodels.) Resolution theorem-proving programs tyPically use the unit preference search strategy, developed by W::ls, et al. [1964)~ in which the merit of a clause in the search is based on its length. While this is a useful strategy for proving simple theorems, it is not nearly powerful enough to successfully guide a search for even rroderately deep !113.thematical proofs. Furtherrrore, it is not adequate for use in question-answering applications -which consist largely of unit clauses, since it gives preference to all unit clauses without regard to their relevance to the query.

Green [1969)~ in considering the application of theorem-proving in question-answering systems, parti­ tioned clauses into two sets, active and passive, Ac­ tive clauses are inferred clauses and axioms selected fran the data base, whereas passive clauses are axioms which have not yet been selected. Only active clauses !113.Y be used in inferences. A passive clause is !113.de active only if it resolves with an existing active clause; preference is given to passive unit clauses. Green incorporated this search approach with the unit preference strategy in the QA3 system which employs, essentially, set~f-support as its inference system.

Kowalski [1970a, 1970b)~'~eparates the notions of an inference system and a search- strategy and describes their respective roles in the theorem-proving search problem. In addition, he defines a class of "uowards diagonal" search strategies which !113.Y be applied to arbitrary problem do!113.ins. These strategies simul­ taneously extend and refine the class of search stra­ tegies, which includes the A* algorithm described by Hart, Nilsson and Raphael [1968)9 Kowalski also pre­ sents a particular u~ds diagonal search algorithm, which he calls the I algorithm. In the I* algorithm, the passive/active clause concept is employed. In addition, the algorithm employs a clause merit evalua­ tion function in which beth the length and level of a clause are considered. Up.vards diagonal search stra­ tegies could also be defined using heuristics other than length and level (see Minker, et al. [1972)) ~

* In the I algorithm, the merit f(C) of clause C is a tuple, (i,j) , in which i = length(C) , and j = level (C) · Kowalski defines an ordering on this merit function which he tenns "up.-rcrrds diagonal merit," denoted by the symbcl ,;;du . Given clauses CJ of merit (i 1 ,j 1 ) and c 2 of merit (i 2 ,j 2 ) , tnen c~ ,;;du c 2 (1.e., c 1 is of better or ecrual upwards d1agonal merit than c 2 ) if

Thus, if the length and level of two clauses sum to the same value, it is better to oenerate the shorter clause, since the goal of the search strategy is to generate a clause of length zero. It is thus advan­ tageous to discriminate between clauses in this manner rather than sblel y on the basis of the sum of the merit components, as is done in earlier search al­ gorithms such as the A* algorithm (Hart, et al. [1968))9.

Based on this merit function, Kowalski partitions the search space into merit sets, called A-sets, into which clauses of equal merit are generated. The I* algorithm generates clauses into these merit sets in increasing upwards diagonal order. It first tries to generate a clause into A(O,O) which would be possible only if the null clause were in the starting set of base clauses. It then successively attempts to gen­ erate (by selecting a clause from the base set, or by inference) clauses into the sets A(O,l) , A(l,O) , A(0,2) , A(l,l) , A(2,0) , A(0,3) , etc. Any time a clause is generated, an attempt is made to recursively generate all of its successors and successors of its successors which are of better merit than the current merit to which the algorithm has sequenced.

* While the above description of the I algorithm is necessarily terse , the reader is referred to Kowalski [1970a, 1970b) ,7,8and to Minker, et al. [1972, 1973]1·2for more detailed discussions.

3. A View of Resolution Theorem-Proving Search as Problem-Reduction Search

Before describing the operation of the Q* al­ gorithm, it will be useful to describe how resolution theorem-proving search may be interpreted as problem­ reduction search. In a problem-reduction search, an operator is applied to a problem P to reduce it to a set of subproblems such that solution of all the successor subproblems implies a solution to P . Equivalently, the conjunction of these subproblems !113.Y be considered a new problem which must be solved for the given problem to be solved. This reduction pro­ cess is recursively applied to each generated subprob­ lem until the original problem has been reduced to a set of primitive subproblems which are trivial to solve.

~bre precisely, a problem-reduction consists of three sets:

1. a set of starting problems;
2. a set of operators that reduce a problem to a set of subproblems; and,
3. a set of final problems which are, by definition, solved.

In the context of resolution theorem-proving, a clause corresponds to a problem and a literal corres­ ponds to a subproblem. Thus, a clause is a conj unc­ tion of subproblems since all subproblems must be solved for the problem to be solved (i.e., all lit­ erals must be eliminated) .

The starting set of problems corresponds to a starting set of i:ase clauses. The actual members of this set will depend upon the inference system being used. For instance, if the inference system is set­ of-suooort, or if it includes set~f-support, th~ starting set of problems corresponds to the clauses in the negation of the query. For other inference sys­ tems, it consists of the entire set of base clauses, i.e., all of the axioms together with the query clauses.

Clauses may also be regarded as operators which are applied to problems by means of inference rules. However, the set of operators that may be applied will vary depending on the inference rule used, e.g., fac­ toring, paramodulation, and various refinements of re­ solution. For a resolution operation, two clauses are involved. In general, the choice of which clause is the problem and which is the operator is somewhat arbitrary. However, for certain inference systems, it seems natural to make a clearer distinction between the two. For instance, if input resolution is used, each clause of a linear chain may be regarded as a problem and all base clauses may be regarded as oper­ ators. For linear and SL resolution, ancestors of a problem may also be considered as operators, in addition to all the base clauses.

A clause may also be a final problem. In parti­ cular, the null clause is the only' such clause when one is attempting to refute a conjecture. Thus , when a null clause is generated, we know that a starting problem has been solved. Determining when a subprob­ l em is solved is nore difficult . This may be seen by oonsidering the process involved in solving a subprob­ lem. A subprobl em P (which =rresr:onds to a literal in a clause) , may be solved in either of tl.;o ways : l) it may be solved in a single step by aoplving an operator that refutes it (a unit clause) ; 2) alter­ nately, an operator may be applied to P that spawns a set of subproblems such that P is solved if and only if all of the subproblems are solved. In prac­ tice, the determination of when a given subproblem has been solved may be quite difficult . Depending on the inference system used, subproblems are attacked in arbitrary order . Consecmentl y , the bookkeeping re­ quired to keep track of which literals of a given clause have been spawned by 1vhich subproblems may be quite involved.

However , one inference system, SL resolution (Kowalski and Kuehner [1971)), lQ starrls out as being particularly well suited for this task. In the first place, SL resolution requires that only one subproblem be attempted at a given level. Secondly, the required bookkeeping is built into the clause representation used in SL resolution. In this representation, a clause is referred to as a chain. In SL resolution , a subproblem to which a solution is sought is actually carried al ong (and duly tagged) in each of the success­ or chains. Such literals are called "A literals" in the successor clauses. As new literals (called "B lit­ erals") are introduced in the attempt to solve a sub­ problem, they are placed to the right of the A literal. When all such B literals have been resolved away (re­ solution is only performed on rightnost B literals) and an A literal is exJX>Sed on the right , then that con­ stitutes a solution to the subproblem from which that A literal descended . At this time , SL resolution re­ quires that the exposed A literal be renoved from the clause - an operation which is called truncation. Only at this time, (and not before as with other re­ finenents of resolution) may a new subproblem from the original problem be selected for solution .

4. The Q* Algorithm

. * The Q* algorithm is based upon the L algorithm of Kowalski together with the idea of Green to allow only certain base clauses to enter the active clause space. Both of these approaches have been extended in the current algorithm. The Q* algorithm is subdivided into 1:w:l major comp::ments :

1. the deduction algorithm which uses primarily syntactic information; and ,
2. the base clause selection algorithm which uses primarily semantic information.

The deduction algorithm generates ne.; problems by the application of operators to problems already in the search space . Any operator that is applied must itself have been previously generated either by infer­ ence or by the selection of a base clause.

Probl ems and operators are generated by ti.JO major subalgorithms , FILL and REx::UR.SE , which are adaptations of analogous subalgorithms of the L* algorithm. As a clause is generated , it is placed into an A- set corres­ JX>n::l.ing to its merit . The algorithm uses a generalized up.vards diagonal merit function to calculate the merit of a clause , and generates clauses in approximately up.vards diagonal order . (Further details on this function as well as on the deduction algorithm are contained in Minker, et al. [1972 , l973J1 ,2.)

In using this merit function , it is hoped that clauses of better merit will be nore useful to answer­ ing the rruerv than those of \.JOrse merit. However, in practice, it is extremely difficult to develop oom­ oonents of the merit function that adequately reflect the relevance of clauses with respect to the query. ~1ost comrxments used to date have been syntactic in nature, rather than semantic, and have led to very in­ efficient search strategies. (See Slagle and Farrell [l971} 1 land Hinker , et al. [l972) 1 for examples .) Con­ secmently, theorem- provers using such a search stra­ tegy are often deluged with irrelevant clauses and

thus are inadequate for nost applications.

There are tl.;o ways to allevi ate this problem. First , after a problem is generated by an inference steP, various deletion rules may be applied so that the problem mav be eliminated in case it is redundant or semantically meaningless . Thus , tautologies , alphabetic variants and subsumed clauses may be eliminated. Furthernore, subproblems as well as prob­ lems mav be eliminated by predicate evaluation. This may be done by referencing stored semantic information about the problem domain . For instance, let C v F(Mary, x) be a generated problem, where C is the remainder of the clause . If it is known that the first argument of the father predicate must be male, and we know that Harv is female , then the literal F(t1arv, xl will never have a solution (i.e., no unit clause , F(Mary, a) , can be true , for any person a). l·Te can thus evaluate the literal F(Mary, x) as being true relative to the interoretation given to the prob­ lem domain and may eliminate the entire problem from the search space since it is unsolvable . With most inference systems completeness should not be violated bv deleting the clause . On the other hand, if a lit­ eral of a clause is evaluated as false, that literal alone, mav be renoved , since it corresoonds to a sub­ Problem that is solved.

Although predicate evaluation using semantic in­ formation about the problem domain will be useful in theorem- proving , it does not pPevent irrelevant clauses from being generated and entered in the search space. l'le thus feel that a more effective method by which to cut down the size of the search space is to avoid genePating irrelevant clauses in the first place . In particular , this can be accomplished by carefully selecting those opePators that are nost re­ levant to the search in progress and by inhibiting those which are irrelevant. This is the function of the base clause selection algorithm.

Depending on the inference system, the algorithm treats one or all of the literals of a generated clause as a specification with which to select axioms . Thus , each literal is termed a "spec literal." (This may be viel"ed as the selection of operators to apply to a subproblem. ) In order to select axioms relevant to the query, the Q* algorithm initially generates clauses from the negation of the query . Each spec literal is used to locate those axioms which either resolve with the generated clause on that literal, or, in some cases , which possess a literal which will unify with the soec literal. The axioms that have been located for a particular spec literal may be re­ duced in number by filtering out those which are found to be semantically inappropriate (e.g., because of in­ compatible argument types) . The remaining operators for a given subproblem then become candidates for generation and must be order ed so that "more promis­ ing" operators are tried first . The list of candi­ dates for a soec literal is placed on a list called the SPEX:LIST, which is itself ordered by using various heuristic criteria. Thus 1 the ordering of the SPEX:LIST reflects the judgment of the base clause algorithm as to which subproblems from among all subproblems in all generated clauses should be attacked first. That is, from among all literals in all generated clauses that are eligible for resolving, the base clause selection strategy picks the best one.

As a result of tiE control maintained over the base clauses by the base clause selection algorithm, the FILL operation of the deduction algorithm will not, in general, acquire all base clauses of a given FILL merit. It obtains only those base clauses made avail­ able to it by the base clause selection algorithm. As a result, the base clauses that are selected will not necessarily be generated in merit order. Consenuently, and in contrast to the /_* algorithm, the Q* algorithm is not admissible. However, as the examples in Section 5 derronstrate, the loss of admissibility may be of only theoretical importance since it would seem to be more important in practical QA applications to find any solution quickly rather than to find a simplest solu­ tion at great expense, at the risk of finding no solu­ tion at all because of space and time considerations.

The following sections describe the manner in which axioms are located, the way certain of these are filtered out, and the way those that remain are order­ ed. Section 4. 4 presents a discussion of a olanned extension of the search strategy in which the base clause algorithm may prune the search space and delete certain candidates from tiE SPEX:LIST upon the recogni­ tion of certain events in the search process.

4.1 Locating Candidate Axioms

As already indicated, the literals of generated clauses are used to locate axioms which may become candidates for generation. The inference system that is being used by the deduction algorithm will deter­ mine which generated clauses should be used for this purp:>se, and what criterion should be applied to select the axioms. If the inference system in use is set-of-support, or if it incorporates set-of-support as does SL resolution, then only the literals of supported clauses will be used. Furthermore, the axioms which become candidates will be those which could r>esoZve with the generated clause. On the other hand, if the inference system does not include set-of­ support then all generatErl clauses, including generat­ ed axioms, will be used to locate axioms. In addition, the resolution criterion must be weakened, so that an axiom will potentially become a candidate if it con­ tains a literal which unifies with a literal of a gen­ erated clause. The weakening of the resolution criterion is necessary in order to assure the refuta­ tion completeness of the algorithm, e.g., in cases where the only refutations for a given query involves the use of a lemna, and the query is not used until the lemna has been established.

Not only doe~ the inference system dictate which clauses are to be used in locating axioms, it also dictates which literals should be used. Thus, in "single literal" inference systems such as SL resolu­ tion or A-ordering, only one designated literal of each generated c lause is used, while for other infer­ ence systems, all of the litera.ls will be used for this purpose.

The approach to locating axioms which may enter into the search, may, for a given query, preclude the generation of certain axioms. That is, there may be axioms which are completely unrelated to the query in that they concern a different problem domain. But since these are completely irrelevant to the query, the search strategy will not be hindered from finding a refutation if one is attainable.

4.2 Semantic Filtering of Candidate Axioms

Once the potential candidates for a qiven spec literal are found, these may be subjected ~ to semantic filtering, and only those which are semantically con­ sistent with the spec literal and its host clause may become candidates. This filtering may be done on the basis of the class membership, or type , of a variable or constant in the spec literal. For example, suppose the generated clause literal is "'PARENT (Dan, Brett) and it is known that Dan is a male, or the literal is "'PARENT(x, Brett) and, from context, it is known that x corresponds to a male. Suppose further that the two potential base clause .candidates:

1. 'VFATHER(u,v) V PARENT(u,v) , and
2. "'~(u,v) v PARENT(u,v)

were found in the data base. Applying the filter, axiom (2) would be found semantically inconsistent with the spec literal since the variable u in the PARENT literal is found to be of type female from con­ text, (i.e., from its use in l'Dl'HER literal), and what is necessary is a PARENT literal whose first argument is of type male. Thus, only (1) Ynlld be­ come a candidate.

A further type of filtering may also be perfo:rm­ ed. l'lhen all of the solutions to a subproblem are ex­ plicit in the data base, it becomes unnecessary to generate any general axioms which might be used to de­ duce a solution to the subproblem. For example, let o.MJI'HER(x, Emily) be a generated clause literal. Also assume that it is known that every individual has exactly one mother. If the axiom l'Dl'HER(Roz, Emily) were found in the data base, then, since this com­ pletely solves the subproblem at harrl, it would be­ come the only carrlidate. No other axioms that oould resolve with o.MJI'HER(x, Emily) would be entered to satisfy this subproblem.

The filtering we have described can be seen to reduce the number of axians which are generated into the search space. As a result, fewer clauses will be available to. interact logically and so the total n~ ber of clauses which may be generated is thereby re­ duced. Clearly, the clauses of the implicit search space which have become ungeneratable as a result of this filtering could not ~ve contributed to a refu­ tation so that although the search algorithm fails to be aompZete (in the sense of exhaustive), it remains :r>efutation complete.

4. 3 Ordering of Carrlidate Axioms and Subproblems

Once the candidate axioms have been located arrl subjected to semantic filtering, they must be ordered so that the "more promising" ones will be generated first. As already noted, there is a two-level order­ ing that is performed: the candidates associated with a particular spec literal must be ordered (this corresponds to the ordering of operators to be applied to a subproblem) , and the lists of candidates for the various spec literals are ordered with respect to one another (this corresporrls to the ordering of subprob­ lems).

In ordering the candidates for a particular spec literal, two different approaches may be employed. In one approach, they may be ordered aocording to a :r>eaommendati on by the user. This is analogous to the recomnendation lists in PLANNER (Hewitt, [1971])12. Another approach is to order candidates aocording to the merit ordering, f , used by the deduction strategy, making sure that data axioms (i.e. 1 fully instantiated unit clauses) precede any general axioms.

With respect to ordering the subproblems, a heuristic guideline is applied when one or rrore con­ stants oc= in literals of the query clauses. In this event, the candidates located bv using constant­ carrying literals of generated clauses will precede in the ordering toose candidate axioms located by the use of general literals. The reasoning behind this heuris­ tic is that (1) constant-carrying literals will gen­ erally resolve (or unify) with fewer base clauses than will general literals, and (2) if a query is about a pnticular individual (constant), then the search mechanism will make more informed decisions about the relevanae of candidate axioms if it concentrates on this individual, and to others which are found to be related to it, rather than qoing off blindly on the basis of some general literal. In many cases, the general literal may actual! y unify with a large subset of the axioms in the data base while only a few of these may be relevant. Furtherrrore, by pursuing this p:>licy, literals which are uninstantiated at one level of the search may becorre instantiated at a subsequent level. Thus, in this approach, it will often be the case that clues (in the form of constants) to direct the search will be passed from one subprobl611 to aoother as the search progresses.

Figure 1 illustrates a proof that was derived giving preference to those literals that contain con­ stants. In Figure 1, clause (!)_yields two literals for the SPEX:Lisr. The literal M(y, Sally) would be given preference on this list since it contains a con­ stant. The axioms that can interact with the literal M(y, Sally) are entered into the search before other axioms that may apply to that clause. Similarly, in clause (3), the constant in H(v, Rita) gives this literal preference. AltOOugh proofs can be found Without using this heuristic, such proofs will tend to generate many unneeded clauses.

It is reasonable to assume that in question­ answering applications a large percentage of the queries will contain constants. Even if constants appear in a given literal, it may be reasonable to give preference to a literal containing only variables based upon a lower estimate of rotential candidates satisfying each of these literals. However, we would expect this to happen infrequent! y in question­ answering systems.

There may be several subprobl611S (spec literals) containing constants which must be ordered with re­ spect to one another on the SPECLisr. In this case, the ordering of candidate lists by their spec literals is accomplished by using a prediation of the merit, f , of a resolvent between the spec literal's oost clause arrl the first axiom in the ordered list of candidates from that literal. One consequence of this ordering is that if a generated unit clause is contradicted by a unit axiom, then this axiom surely will have become a carrlidate, and it will be placed first in the order­ ing so that it will be the very next axiom to be gen­ erated. Each time an axiom is rerroved from the list of can:lidates, the next candidate in the list is used for a new prediction, and the corresponding SPECLisr enti:v is reinserted into an appropriate rosition of the list- -- it may remain on top of the list, or some other subproblem may 6Tlerge as "rrost promising. "

In some data bases, there may be certain constants which oc= in a large number of 'the data axioms. Generally, these would be non-specific, class specify­ ing types of constants such as MALE and SINGLE as used in the data axiom.

PffiSON(JOHN, SMITH, ID475, MALE , FRT>W.E) .

Since such constants do not desianate particular in­ dividuals, arrl since they do occUr througoout the data base, thev will be of little value in directing the search . Thus, for the purpose of ordering the SPECLisr, spec literals. containing these types of con­ stants alone are treated as general literals.

4.4 Semantic Actions Durinq the Search

It was noted in Section 4. 2 that some subproblems mav be comnletely solved by data axioms stored in the data base . ~bre- generally~ some subprobl611s have an exact number of solutions while others have an in­ definite number of solutions . I f the number of solu­ tions to a given subproblem is known, then, during the course of the search, the progress of the search rela­ tive to finding these solutions can be rronitored. l'ihen all of the solutions have been found , that ror­ tion of the search graph which has been unnecessarily generated in the attempt to find these solutions can be pruned . In addition, the candidate axioms located through the use of literals in the pruned clauses or in clauses along the solution path will have their candidate status rerroved. The effect of this pruning is to reduce the number of irrelevant clauses in the search space. Of even greater significance is that the rotential successors of these clauses are effec­ tively prevented from being generated.

The bookkeeping required to apply these s6Tlantic actions would be quite complex when arbitrary infer­ ence systems are employed , · since, for a given clause (problem), atte:npts to solve a11 of the subprobl€!15 are carried out simultaneously. Ho.vever, SL resolution is particularly well suited for this aporoach, since only one subproblem is attacked at a time and because the bookkeeping required to detect the solution of a subprobl6Tl is built into the SL clause representation, as noted in Section 3. Seman­ tic actions are taken when truncation oc=s, since truncation only occurs when a subproblem has been solved . The semantic action taken is to increment a count and test it against the number of solutions sought . If this number is met , then pruning can be performed.

The above approach does not require that all solutions to a given subproblem be obtained before progressing to another subproblem. It would seem to be desirable, in some cases, to continue the search for additional solutions to the subproblem, while at the same time advancing to the next subproblem.

5. Example Runs With MRPPS

The !~PS system incorrorates a preliminary ver­ sion of the Q* algorithm plus an option for selecting the r algorithm. The current implementation of Q* does not yet include the semantic filtering of candi­ dates, and no mechanism has been included to take semantic actions. The current version inchrles the deduction strategy as outlined, together with a base clause selection strategy which locates and orders axioms essentially as described. All details concern­ ing the current imnlementation are described in Hinker , et al. [1972] 1 · The implementation of the 't algorithm uses the same deduction strategy as Q* , but the base clause selection strategy merely locates · axioms in merit order, that is to say , by length, witOOut regard to other clauses generated by the search.

We present comr.arative statistics for two differ­ ent queries, in which set-of-support and SL resolution were the chosen inference systems, and the merit com­ ponents were clause length and l evel . Clause length and level bounds were both set at eleven, and an f value bound (= length + level) was set at eleven. The data base used contains 295 data axioms which expli­ citly state the (1) mother, (2) father , (3) birth date, and (4) birthplace of individuals in terms of their identification (i.d.) numbers, and (5) which relate the first and last name of each individual to their identification number. The data base also includes 88 general axioms which define the various predicates in terms of other predicates .

Question l. "l<lhat is the name of Brett Fishman's moth­ er?"

The significant aspects of this simple question is that its negation in clause form is a unit clause con­ taining constants. With the data base used, it re­ quires four axioms and four levels of search to achieve a refutation.

* Both the I and Q* algorithms successfully completed the search, however as the statistics in Table 2 demonstrate, with considerably different levels of v.urk arrl resources required. Whereas the Q* algorithm fortuitously ~enerated the minimal number of base clauses, the L* algorithm has to generate all axioms of length one (i.e., all the data axioms), two, and three and some axioms of length four before the re­ quired general axiom (of length four) was obtained. Once this general axiom was resolved against the query clause, the resolvent, having support, could be resolv­ ed against many of the axioms already in A-sets, and similarly for the resolvents obtained. As a con­ sequence, many more resolvents were generated . Furthermore, the presence of a large number of clauses in A-sets required the use of a considerable amount of free space to keep track of the clauses as well as a significant increase in the search time required.

Question 2. "Is there a person who is the grandfather on the father's side of individual 67 and the grand­ father on the mother ' s side of individual 7?"

The negation of the question in clause form is:

where FF is the predicate "grandfather on the father's side", and FM is the predicate "grandfather on the mother 's side." This question, which requires six levels of search requires the following six axioms from the set of 295 data axioms and 88 general axioms:

F(x, y) v M(y, z) v FH(x, z)

F(x, y) v F(y, z) v FF(x, z)

M(4 , 7), F(6, 4), F(6, 63), and F(63, 67) .

Proofs were found using set-of-support and SL resolution as the inference mechanism. The statistics for set-of-support indicate that the Q* algorithm was quite selective as compared to I* both with respect to the number of resolvents and axioms generated. How­ ever, Q* did obtain considerably more general axioms than actually needed.

The same question was tested using SL resolution as the inference mechanism. The table shows statistics for the Q* algorithm as generated by the computer. It also shows statistics, generated by hand, for the Q* algorithm when the semantic rule of counting the number of possible solutions to a subproblem is used. The Q* and I* algorithms without U1e use of semantics gener­ ated the same number of inferences . However, I* brought in 381 axioms, only 6 of which were needed. Q* when not using semantics brought in 16 axioms, only 6 of which were actual! y needed. Q* without semantics performed better when using SL resolution than when using set-of- support as the inference mechanism. The use of semantics for Q* shows its general utility. The number of axioms entered were 7, while only 6 were needed for the proof. Although there is a significant decrease in the number of axioms generated using semantics, the one example should not be considered tc be the type of improvement that one will always achieve using semantic considerations to restrict the search. However, it is indicative of the use of semantics. The trace of clauses generated by SL re­ solution and the proof are shown in Figure 2.

6. Summary

l'lle have described a search strategy for theorem­ orovinq which uses both svntactic and semantic infor­ mation. to direct the search in a Question-Answering System. Host theorem-proving systems have used primarily syntactic information such as clause level and clause length to direct the search. Others have attempted to use only refinements of resolution with a breadth-first search or an ad hoc use of heuristic rules. Experience with such systems may have led some to speculate that means other than theorem-proving must be developed to perform deduction in question­ answering, or in other problems (e . g ., Anderson and Hayes [19721)+3 The reason for this skepticism of theorem-proving may stem from the inadequacy of search strategies to limit the search to a "reasonable" num­ ber of nodes in finding proofs. We agree that the use of only logical rules and syntactic heuristics will not be sufficient for most svstems. However, it is our hope that thP. introduction of seniantic information to aid in directing the seardl will be useful.

We have tried to shaw where semmtic information may be used in a theorem prover, and haw it may coor­ dinate with the syntactic heuristics and logical de­ duction. 'Ihere are several places where Sffilantics enter into the search process :

1. at the tirre a clause is generated, to deter­ mine whether it is Sffilantically neaningful;
2. in selecting a literal of a clause to ex­ pand;
3. in the filtering out of irrelevant oper­ ators; and
4. in taking actions when a literal is solved.

There is, hawever, a tradeoff as to when seinantics should be awlied. It may result that the attempt to determine whether or not a clause is solvable could take more time than the solving of the problem. Hence, sttrlies must be performed in this area to determine the various costs involved.

With an arbitrary inference system it is not always easy to determine when a literal from sene clause has been solved. The bookkeeping that might be involved could becare unmanageable. Hawever, as de­ scribed previously, SL resolution minimizes the book­ keeping problem. SL resolution has the additional advantage of providing the opportunity to select which subproblem to attack next.

Sene of the semantic information we use is gen­ eral, e.g., the count of the number of solutions to a subproblem; if such information is supplied by the user it =uld be used to advantage for any problem danain. A general frarna.vark for representing and applying semantic infonnation is needed. In addition, our semantic considerations have been directed primarily at the meaning of constants, and not at the rreaning of functions and Skolem functions that may frequently occur in clauses. These must also be =n­ sidered.

We have presented a first version of the Q* al­ gorithm that carnbines syntactic and semantic consider­ ations. Improvements must be made in the algorithm to handle parallel seari~ing su:.::h as in CONNIVER (Sussman and M:::Denrott[l972)) , and to :i.rrplement sane of the features that were described, but not in=rporated .in­ to the first version. Ha-~ever, based on l:irnited ex­ perience with the =ent version of Q*, it has been d::>served that the search does restrict the generation of clauses.

'Ihe area of semantics and theoren-proving re­ quires considerably rrore research and experlirentation. This paper has described a first step in exploring this area.