Automated Hypothesis Generation Using Extended Inductive Resolution

Abstract

We report on a method of automated hypothe6i& gen~~ation, called !-resolution, which is derived from deductiv~:: resolution technio·tes. The method is inductive in characttr, in th~ sense thAt given input statement E, it generates hypotheses H, such that E is a deductive conse­ quence ot H. The meth(Jd is extended by s gener­ alized unlfi cation algorithm which introduces appropriate identity assumptions needed to unify a J,iair or literals. The !-resolution technique is shown to embody a version or Oclc.'lllll! 1 s razor as a prur · .Lng heuristic. Some promisin{; experi­

·nental results are also presented.

In [5J we discussed a general method for transforming deductive consequence generators into htductive consequence generators. In this paper we wish to report on a general mechanized inductive ~:~ethod, to be called !-resolution, which Wa!5 derived from normal resolution proc­ dures. The r-reeolution procodure was not designed as a special purpose routine only applicable to certain problems (lilce the routine de~cribed in [2)), but rather it is applicable to any problem in any context suitably describ­ able in the syntax or first-order predicate cal­ culus with identity. The potential range of applicability of the method is thus extremely broad. Our routine appears to deal with A D)re general class of hypotheses than previo'.lsly reported efforts in thie area; in particular, see [1], r9l, [10], [111, and [121.

~e assume familiarity with the usual termi­ nology and theory of resolution. For any expres­ sion E, we represent the set or clauses obtained from the clause form of E by C(E). For a set C of clauses, we represent the set of all pairwise resolvents of members ot C by R(C). We then define R<l(c) = c and RJ1+1(c)- R(Rfl(C)) IJ RI'(C).

For ~ur purposes, we will consider resolu­ tion as a consequence generator. As such, reso­ lution ir not complete. That is, for any expres­ sion E, th~re are expressions E' euch that E entails ~ 1 but for no n ia it the case that C(E') ~ rtn(c(E) ). For just one type of example, consider the case in which E' contains predicates which do not occur in E, and note th~t r~solution introduces no new predicates.

The basic !-resolution principlE: is very similar to the basic resolution principle. The prin~iplc appears to be, in ese~ntial respects, the same as the basic inverse method of f31, appa~ntly developed by Maalov as early as 1964. However, our development was independent of Haslov 1 6 worJc, and our routine is used induc­ tively rather than dedl:ctively. As with the deductive case, before the prlnciple can he

Charles G. Morgan Department ot Philosophy Universit1 ot Alberta Edmonton, Alberta

Canada applied to a given exoression, the exoreesion must first be transforLJed into a certain nonm.l form. For !-resolution, input exnressions are first transformed into prenex dis.1unctive norii'.al form, using the standard equivalences:

(Q1) ··· (Qn)(E1 V ··· v Ell) where the Qi are quentif,ers, each over a differ­ ent variable, and each Ei is a conjunction of literals. We must now remove the quantifier! to obtain the quantifier-tree disjunctive normal form. To avoid introduction of rore complex Skolem function::: than necessary, we next em!'loy the stand~rd quantifier distrihl:tion rules to obtain an equivalent e~>ression such that the scope of each quantifier contains as few cf the Ei as possible. We then remove all universal quantifiers by replaci~g them with appropriate ~olem functions. (That is, if a universal quantifier does not occur within the scope of any existential quantifier, we renl&ce the variable or the universal quantifier, wherever it occurs in the Ei, by a new constant (0-place function). It a universal quantifier occurs within the scope of exiotential nuantifiers over variables x1, ··· , xp, then we replace the vari­ able or the universal quantifier Wherever it occurs in the Ei by f(x1, ··· , xp), where r is some new p-pl&ce function.) 'tie tl-ten drop all quantifiers. The resulting expression is called the f-clauae form; a conjunction of literals is called an !-clause. If E is any exprePsion, then we represent the set of f-clausee obtained from E by fC(E). Note that in the !-clause form, free variables represent existential qlmntifi­ cation. Note aloo that it the input is to be several expressions, A1, ··· , Aq, then we must obtain the !-clauses from their conjunction, A1 & ··· & Aq.

We assume familiarity with the star.dard terminology regarding substitutions and with the unification aleorithm. A, usual, if C is a set of expresaions and ~ is a set of substitutions, by ex we mean the set of expressions oht~ined hy performing every substitution in ~ on every member or c.

The basic !-resolution Principle ellows the inference or one f-clauae from a given pair or f-clauses. Cur first step is to renane the v~riables in one or the !-clauses 80 that the pair has no varinbles in common. Let E1 &nd E2 be th~ two resulting !-clauses. Let C1 and C2 be the aets of literals occ\lrring in E1 and E2, respectively. Further, ~uppose there are subsets

C1' nnd C2 1 of C1 and C2:

such that C1 ' ! 1 {E2l' ··· , E2wa 1 is unif:!~t.He by a most general unit er X. Then an !-resolvent of E1 and E2 is the !-clause which results from conjoining the literals in the set:

where of course 11 - 11 is set theoretic subtrac­ tion. Note that we tr.ust include the empty clause, designated by EHP, as a possible f-retolvent. For our purr;osos, EMP is taken to he !n!!!, in Bftl"J inter}:retation.

For any expression E, there are only a finite number of f-resolvents ot pairs in tc(E). We designate the set of f-resolvents ot pairs ot t-claueee in eet C b;y fR( C). We then define mO(c) · c and tRJ1+1 (c) · tR(fan(c)) u ran(c). A detailed proof of the following usef'ul theorem 'I1IA1 be found in r 6 J.

Theorem 1 r Let E be any closed first­ order expression. Then E is valid it and only it tor 801118 n, EMP E fftD(tc(E)).

For any t'IIIO expressions, E1 and E2, if E2 is false in every interpretation which fsleifiee E1 1 then we write E1 If-F E2; it E2 is true in every interpretation which satieties E1, we write .81 I~ 12. Clearly we have E1 lt-F E2 it and only it 12 U- E1 · So if an expression E2 is generated from expre·aion E1 b;y falsehood preserving rules, we know that E2 entails E1 in the usual sense. The important thing about !-resolution is that it 1a falsehood preserving. A detailed proof of the following theorem may be found in rs1.

Theol'OIII 2: Let E1 and E2 be any two closed first-order expressions. If for some n, tc(E2) ~ tftD(tc(E1)), then E2 It- E1 (i.e., '11 ,,_, E2).

Thus we can use !-resolution to generate h:JPOtheae~ from which our input may be deduced (aee [7) for a general discussion ot otjections to this approach). However, as an hypothesis aenerator, t-recolution is incomplete in the sense that for any exprestion E1, there are expreesiors E2 such that E1 I~F E2 but for no n is it the case that tC(62) c tRD(fC(E1)). Again simply note that !-resolution introduces no n6w predi­ cates. So !-resolution automatically incorporates some form or pruning.

It is useful to characterize the p~n:l.ng heuristic in more intuitive tems. We ma;y think ot a lit~ral as a statement or a basic (or atomic) fact about the subject matter under consideration. Note tint that when we substitute a term, 'Which occurs in or1e l:lteral, for a free variable in eome other literl<l, we are in Ill'\ intuit.! ve sense reducinc the number of unnamed entities which might possibly be required to satir.ty the liter­ ala; intuitively, the more existential quanti­ fiers in the prenex ronn or an expression, the more entities which might possiblr be required to aatisty the expression. Bl1t note secondly that the only substitutionA that are 118de are those wt':ich allow the elimination of a pair or Uterals. So the intuitive heuristic seems to be:

• (H.1 ) Reduce the nlJ'lber of unnamed entities where ouch a reduction

will allow a reduction in the number of basic tacte.

Thu~ ~~ can aee that basic r-rP.~olution incorpor­ ates a verPion of Ockham 1 ~ razor.

Let us ccnflider an extr.,rr.ely si""'le examPle r Either Smokey is a black ~r.imal or there is an animal that is not black. In symhob we haver

We obtain the followi~g f-clausesr

(a.2) As & Be

(a.J) Ay & .., By

By basic f-reeolution we obtain:

(a.4) As

And (a.4) simply says: Sa:lkey is an anillal. By Theorem 2, we kno~ that (a.4) entails (a.1). Note that we have reduced the number of unnamed entities as well as the number or basic ract.s in nrriving at the hypothesis ·

The heur:lstic (H.t). is actually a hit broader than thu performance or !-resolution. Suppose we receive the following report from a detective ~t the scene of the crime: Someone killed a perPon named John and someone killed a per11on named Rill. We might represent our information ~helically by:

From (b.t) we obtain C\nly one r-clause r

(b.2) Pj & Px & Kxj & Pb & Py & ~

Since we have only one !-clause, basic r­ resolution is not applicable. Dut heuristic (H.1) 'l«luld direct us to the tollowin~; hyt>Otheses, among others :

(b.J) Pj & Kjj & Pb & P,y & lt7b (John committed suicide and someone killed Bill.)

• (b.4) Pj & KjJ & Pb & Kbb

(John and Bill both cormdtted suicide.)

• (b.5) Pj & Pb & Kbj & Kjb (John and Bill killed eacl':. other.)

(lUll killed John and corrrnitted

• (b.6) Pj & Kbj & Pb & Kbb suicide.)

(The aa.me person killed hoth .rohn

• (b.?) Pj & Px & Kxj & Ph t. Kxh and Bill.)

Such examples and the state~nt of the heur1~tic suggest adcing another rule of inference; the rule will Le called linear contraction, or LC for short. The rule allows us to infer one !-clause from one other r-c~use. Let C bo the set of literals ht some given r-cl:u:se, and su\?pose there is a subset of C, say C 1 = (E1, ··· , En], such that there is a most general unifier ~or C 1 ; that is, E1 ~ "' ··· · En).. Then I.C allows us to infer the !-clause formed by conjoining the members or c~.

The rule LC ~uld allow the generation ot (b.J - 7) from (b.2), as well as 30me additional hypotheeee. But note that the example indicates the sensitivity of I.C to the amount of detail in the repre3entation. If the predicate for person­ hood were eliminated from (b.2) we ~uld have:

(b.a) ltxj & ~b

Since instantiating x for '1 (or '1 for x) would not allow us to reduce the number of basic facts, even LC would not allow any inference from (b.a). The faet that all the individuals in (b.!) are persons means that instantiation reduces the number ot persons. Con3equently, in any proposed applic3tion, we must be careful to include all information concerning the individual~; named or quantified.

It is VQry simple to establish that LC is falsehood preservin&· Since tree v~riables repre­ sent existential quantification, substitution of a te~, t, for a free variable simply involves one or three possibilities: (i) replacing a pair or existential quantifiers by a single existential quantifier, in case t is a variable; or (ii) replacing an existential quantifier by a universal quantifier, in case t is composed of Skolem functions; or (iii) replacing an existential quantifier by some intf'lrpreted constant, in case t is an interpreted constant. But then we just note that: (i) (!x)(E!(x) & E2(x)) entails (!x)E!(x) & (~)E2(y); (ii) (x)E(x) entails (!x)E(x); and (iii) E(a) entails {~)K(x). These consideration&, combined with the fact that E & E is equivalent to E, establish the desired result.

Both basic !-resolution and LC strive to reduce tl:e number of atomic facts. However, since neither deals explicitly with equality, both share the im~licit assumption that constants represent distinct entities. If we could some­ times assume that certain terms designate the same object, we might be able to further reduce the number of ato~c facts. For example, in (b.a) if we could assume j a b, then we could arrive at Kxj via LC. These consideration~ led us to develop a &lightly different version of the uni­ ficatior. algorithm, called equality assumption introduction (EAI), which introduces just those equalit) assumptions which will allow a reduction in the number of basic facts. We will give a brief statement of a version of the EAI algorithm suited to the unjfication of pairs of literals, E1 IUld U. ~le asswne E! and E2 are either both negated or both unnegated and that both employ the baffle predicate. In the following algorithm, k is just a counter, ~ will correspond to 8 most general unifier, and eq lliill be a set of required equality nst5utlptions. By (t/t 1 ), we mean the aubstitutlon of t for t 1; we use ~ o ~I to designate the usual composition of su~stjtution ~ete; we use ~ tor the empty set.

1. f~t k ~ O, E1o = E!, E20 = E2, ~O = ~~ and eQo"' ~.
2. It Elk= E~, then set ~ = lk and eq .. eqk and stop.
3. Find the (ordered) disagreement set (ttk, t2k) or E1k and E2k.
4. If t!k 13 a variable not in t'k' then go to step a.
5. 5o If t~ is a variable not jn ttk, then go to step 10.
6. If t!k is shorter than, or ot the same length as, t2k· then eet lk+! · ~k ~nd 8Citc+! - eqk(t1J!t2k) lJ (tlk = t2k, ~'ld go to step 11 ·
7. ~et ~~ · \k and eqk+! '"' eqk(t2J!ttk) U [t2k · t1k 1 and go to step 9.
8. a, Set ~k+ 1 · lk o ((t2k/t1k)} and eqk+1 = eqk(t2k/t1k).
9. Set ~~ · E2k(t2J!t1k) and E!k+l · E1k(t2~t1k) aY~d go to step 17..
10. Set ~ 1 = ~k o ((t1k/t2k)1 and 8Citc+! "" eqk(t1J!t2k).
11. f~t E1k+ 1 · E1k(t1tft2k) and ~1 - E2k(tt~!t2k).
12. Set k · k + 1 and go to step ~.

This moc;itied unification al~rithm 1.s j11st an extension of the usual one. If two clauses are unifiable, then our nlgorithtn returnt~ 8 most general unifier (in the usual sense) and an empty eq. Our algorithm differs from thl'l normal unification ~.l~rithm at those points where the normal algorithm termin~tes unsuccessfully. The normal algorithm ~~lts with no unifier if (i) the disagreement ~et contains no varj~ble, or if (ii) one term 1:; contained in the ott-er. In such car.es, EAI introduces (via the set eq) the exPlicit assumption that the two termA nre enual and ~\..jr·':.itutee the short.i"'1" for the lonp,er. '!'he reason for substitJ.;t l'lg tne s"o.l"t.er for the longer is to gunrantee t.hat t'1e suhet it. uti on process will terminate.

If we employ EAI, then basic f-resclution and LC must be sligh~ly altered so th&t the resultant f-cl.auses cpnt'lin the contents c.f eq. The f-l'esolvent is o'.Jtainec.l b;y C(\njoining the literals ln the followir.~ set (compare wit.h ( *) 1 above):

For :U::, the reeultant ::l.c.:!se !.& the conjunction of the mer.1bers of C>. U eq (inetead of just C~). In both ce ,;es, of cour.,e, t!.':l >. i!< the substitution set obtained from EAI.

&sic f-.,.esolution ar.d LC when extended b;y KAl still generate only 3 finite number of r­ clauaes from any given finite ~et. For a finite set C of !-clauses, we mean ~ efR(C) the set of all !-clauses which result from the application or busic !-resolution and LC, both extonded by Bll. As usual, we dei'inP. etRO(c) · C and etffr+1 (C) .. er~(C) U etR(etaD(C)). Pbr any set C ot !-clauses, b:y &!(C) we me:m the set or equ.Uity axioms of the language of c. It is then possible to prove the tollowingt

Theore111 3: Let El and E2 be any t\110 closed expressions in a first-order langua,se with iden­ titf· If for eome n, fC(E2) c ef~(fC(E1)), then {.i2J U ~(tc(E1)) I~ El. -

In other wni111 our methods, extanded by EAI, will aenerate from the !-clauses of an input expres:;ion E1 1 the £-clauses of expressions E2 such that ci?en the usual equality axioms, E1 is entailEd b;y E2.

The intuitions embodied in the EAI extension ai'e ali~tl.y 1110re complex than those embodied in hel.ll'ietic (H.1) in t-wo ways. Pir:rt., the extended method proposee a reduction in the number of J!1!!!!!! ent '!.ties, providing such a reduction will reduce the number of atomic fActa. And eecondl:y, the extended athod prt>poaes restrictione on certain functic-,lal values, again providing that such restrictions will raduce the number of atomic facta.

Two rather distinct circumstances for the application or r-reeolution may he identified. In the first case, no back3r0und assumptions arc presupposed. The input to our procedure is then just the set of !-clauses obtained from the · expression of the state of affairs for which we would like an hypothesis.

Let us consider an example. f:uppoae we wish to find an hYJ'Othesis to account fer the following expressions

From (c.1) we obtain the follo"ing f-clauseaz

(o.2) Ray&~Py

(c.3) ~ l!ab

(c.4) ~llbc

(c.5) Po

0\11' methoJ yields the following results:

To obtain the desired hypothesis, we must trar.a­ late hack into normal first-order notation. Rut the question is, which !-clauses sh(\uld he included? Py Theorem 3, we coul~ choose any single !-clause, or any non-empty subset. Various heuriAtica could be used to nake the selection, but we will mention only one here.

Suppose we are after h~~thesea which account for 3 disjunction, say P V Q, and suppose we know that S entails P and R entails o. Then we could use s, ~r we could use R, or we could use the disjunction f. v R. One ·reason for preferring the disjunctive hypothesis is that it is deduc­ tively weaker than the alternatives; it therefore places r-er refltrictiona on the range of possi­ bilities and is thus in some intuitive sense more likely to be true. To make this idea a little more precise, we introduce a definition. We will say that one !-clause A cover!! another f-c:lau!le B just tn case either (1) A is identical to B, or (ii) A results frorn applyint. extended LC to some !-clause c, Wlere C covers B, or (iii) A results from applying extended basic f-reeolu­ tion to f-clausu C and D, where 'A is covered hy at least onE; of C and D. \ie my then fornalize our heuristic by saying that !n the selection or !-clauses for hypotheses, - llhould include r­ clausea sufficient to cover every !-clause in the original input. Thus in 0\11' example, we ehould not use just (c.4), or just (c.6), or just (c.12). In fact, therP- is no single f-cl'luse which covers all of (c.2- 5). But we could use (c.11) and (c.12) to obtain:

Or we could use (c.J), (c.4), and (c.S) to ohtain:

Or we could use (c.3) and (c.12) to obtaint

Each of these hypotheses entails (c.1). There are various other pot;sibilitiea as well, but. the range of possibilities i11 auhstantiP.lly smaller than tr~t Wh!oh we would have to c(\naider if no heuristic were employed.

Thtt second circumstance in which we mipht wish to une r-resolution is the more usual one. F~~ently we wish to obtain an hypothesje to account for A, g:l.ven the presupposition fl. '!'hAt is, we want 110me C ouch that:

• (d.1) C & B I~ A

But (d.1) is equivalent to:

(d.2) C It· ..., B V A

And (d.2) is equivalent to:

1-'ron. this er.Blllple we can eee that the input to CJur f-reaolution procedure sh,uld be the r­ clauses in A al~ng with the f-claus~s in the negation of our pr~Jsuppo:;itlon. If we have more than one presuppositior;, then we must tske the negation of the conjunction of all our presup­ positions. Ou1· :input presuppositions can be any statements at, all, whether factual or logical. We could for example have the axioms for identit;r theory as our presuppo1dtions.

For simplicity, let us consider a standard syllogistic example. Suppose we would like an t:ypothes1s which would entail "All dogs are hairy", given the assumption that "All dogs are Dl&lllnals". Our assumptio"l na,y be formalized as:

The negation of (e.1) is just:

From (e.2) we obtain the !-clause:

The statement we want to be able to derive nay be formalized as:

And (e.4) gives us the following f-clauses:

• (e.5) -,Da

(e.6) Ha

From (e.J) and (e.5) we obtain:

(e.7) ..., Ma

tb other applications of our rules are possible. ~o we get the following hypotheses, IUIIOng others:

(Everything js hairy.)

(e.9) (x) ...., lobe from (e.7)

(There are no mammals.)

Note that (e.10) is the only hypothesis ohtalned in accord to;ith the coverinc heuri::;tic diflcusscd above.

We should sa:' a few rore w.::.rdR about the cover:i.np, heuristic when used wi+.h >Jntecf'!c'P-ntl:v given information. f.uppose we are assw.illg "1 and B2 aB antecedently given infl1rl"ation .)nrl we are secl<ir.g an hypothesis to accour1t for A. r"lur input would then ~·~ the f-clam;es rr-:>1:1 ~ F1 v ..., B2 VA. Suppose rt·d.Ler U.at. l.n ·lN·ivh·t· ·H!I' hypotheses, we l'IIB.ke no use of l'lr>:'f' r-cb;.;r.e !'rem ..., B1. Ther. the hyr:oH.es~!; p;hen ~.Y t.hf:' ~"ver ~ ry heur1 stic would be of the !'r.·rm ..., -:::1 V c. But. note that D1 & (...,81 V C) i~ equ~vdlent to D1 & c. So there would ~e nc- r.eed to include tt:e r-e~uses free ~ 81 in our hYfotl'.ene~; t:nrler these cir·cumstances. The sar.1e con~idcrations would apply tc conjur1ctive components of B1 Me B2 (i.e., to disjuractiv-. c0mponent~ of-. B1 and ..., B2). ConHequently, the covering heurhtic should only be applied to that portion or t.he ir.put which does not arise froM antecerler>tly given presurposit!Ons. In this simnle exa~le, the covering heuristic should be npplied only to A and n~t to -,81 nnd not to..., B2. In the syllogistic ~le above, t.he covering heuristic should be apPlied only to (e.5) l'lnd (e.6) and not to (e.3).

Experlmentally, we can reoort that for an:r syllogiSII' whose validity doe11 not aM~'e exb­ tential iaport, given the conclusion and one premise, our method with the ~overing heuristic will yield just the required adcitional premise. Further, for those ~yllogismR ljhich do require existential import, our ~thod generP.tes the hypothesis that there :Is !!Omethil"'g i.n the appropriate subject class fr0r.1 the inpct of the desired conclusion and the premises as 4Seump­

tions.

The most extensive experimental test or ~ur rr.ethods has heer. Jl'l&de !n the areA of non­ standard lcp:ics. In particular we have dealt in dehU with many system~'< of modal lopic snd many syste:n!. of relevance lopi.c. The charac­ teristic serr.a'!lt.ics for such 11ystems de~ends on the determination of certa~ restriction~ to be placed on given semar.tic relntions. !.:sing our methods we have heen ahle to p.f!nerate from a eernantic translation of the axioms and infer­ ence rules the knowr. semantic requirements for every case im·estig;q.ted--ahcut 30 systems have been examined at this time (see r41 and (81). Further, in these cases, we can employ A sli~tl;r modified version of the covering heuristic and prove that the hypotheses pererated by our methods will yield the cherscteristie semantics if !Dl first-order conditione will. Theee results a::.·e particularly pleasiT'g, as our methoc!s were designed from a general point of view, with no thought of this applicAtion.

We 'loiOuld like to see JI'IOre extensive testing of our methods i.n more l'ract. ical, lese formal areas. In any cal"e, i.t rhoulo ~e l-ome in nint! that the methoc! cannot he Ul'led to ~r.­ crate new predicates (i.e., new "ccncer.ts"). The hypotheses generated ~re alwAy~ in ter~e of t"tE. input predicates, with the rol"sirle exce"ti.on of equality.

\~e "'ould finally li!<e to point nnt. trat EAI could be t·scd to r.upplP.!"omt normal deductiv., resolution. The rest;lta:'lt clau~e would l·e forr.lPd tn the usual way l'llonF; with t.l1e rlit<jur.ction Of thP nesatione of the 8QU&lity aesumptione in eq. By employin£ simple leJdcal orderin£ principles in formulating equality statements, no special axioue tor equality would be required. (Such an application would be similar to the method described in ( 131. ) It seems intui t1 vel.y that W might sul',otantially speed up proofs involving equality by introducing just the appropriate eql:.&lity statem£nts needed for obtaining reeolvents. However, at this tinJe we have not conducted an experimental examination of BAI in the deductive context.