Cooperation between Top-Down and Bottom-Up Theorem Provers

Bottom-up pro v ers prot from strong redundan y on trol but suer from the la k of goal-orien tation, whereas top-do wn pro v ers are goal-orien ted but often ha v ew eak al uli when their pro of lengths are onsidered. In order to in tegrate b oth approa hes, w e try to a hiev e o op eration b et w een a top-do wn and a b ottom-up pro v er in t w o dieren tw a ys: The rst te hnique aims at supp orting a b ottom-up with a top-do wn pro v er. A top-do wn pro v er generates subgoal lauses, they are then pro essed b y a b ottom-up pro v er. The se ond te hnique deals with the use of b ottom-up generated lemmas in a top-do wn pro v er.W e apply our on ept to the areas of mo del elimination and sup erp osition. W e dis uss the abilit y of our te hniques to shorten pro ofs as w ell as to reorder the sear h spa e in anappropriate manner. In tro du tion Automated dedu tion is at its lo w est lev el a sear h problem that spans h uge sear h spa es. In the past man y dieren t al uli ha v e b een dev elop ed in order to op e with problems from the area of automated theorem pro ving. Essen tially, for rst-order theorem pro ving t w o main paradigms for al uli are in use: T op-down al uli lik e mo del elimination (ME, Lo v eland, 1968, 1978) attempt to re ursiv ely break do wn and transform a goal in to subgoals that an nally b e pro v en immediately with the axioms or with assumptions madeduring the pro of. When omparing results of v arious pro v ers (e.g., Sut lie & Suttner, 1997) it is ob vious that pro v ers based on dieren t paradigms often b eha v e quite dieren tly . There are problems where b ottom-up theorem pro v ers p erform onsiderably w ell, but top-do wn pro v ers p o orly,and vi e v ersa. The main reason for this is that b ottom-up pro v ers often suer from the la k of goal-orien tation of their sear h, but prot from their strong redundan y on trol me hanisms. Therefore, a topi that has ome in to the fo us of resear h is the in tegration of b oth approa hes. It is also p ossible to mo dify al uli or pro v ers whi h w ork a ording to one paradigm so as to in tro du e asp e ts of the other paradigm in to it. This, ho w ev er, requires a lot of implemen tational eort to mo dify the pro v ers, whereas our approa h do es not require hanges of the pro v ers but only hanges of their input. Information that is w ell-suited for impro ving the p erforman e of top-do wn pro v ers are lemmas dedu ed b y b ottom-up pro v ers. These lemmas are added to the input of a top-do wn pro v er and an help to shorten the pro of length b y immediately solving subgoals. Normally, the emplo y ed pro of pro edures an signi an tly prot from the pro of length redu tion obtained. This means that an un b ounded use of b ottom-up generated lemmas without using te hniques for ho osing only r elevant lemmas (i.e.