# Cooperation Between Top-Down And Bottom-Up Theorem Provers

Dirk Fuchs Fachbereich Informatik, Universitat Kaiserslautern 67663 Kaiserslautern, Germany D F U CH S @ I N F ORM AT IK  . U N I - KL  . D E
Marc Fuchs Fakultat für Informatik, TU München 80290 München, Germany FU CH SM QINF ORMATIK .TU-MUEN CHEN .D E

## Abstract

Top-down and bottom-up theorem proving approaches each have specific advantages and disadvantages.  Bottom-up provers profit from strong redundancy control but suffer from the lack of goal-orientation, whereas top-down provers are goal-oriented but often have weak calculi when their proof lengths are considered. In order to integrate both approaches, we try to achieve cooperation between a top-down and a bottom-up prover in two different ways: The first technique aims at supporting a bottom-up with a top-down prover. A topdown prover generates subgoal clauses, they are then processed by a bottom-up prover. The ss We apply our concept to the areas of model elimination and superposition. We discuss the ability of our techniques to shorten proofs as well as to reorder the search space in an appropriate manner. Furthermore, in order to identify subgoal clauses and lemmas which are actually relevant for the proof task, we develop methods for a relevancy-based filtering. Experiments with the provers SETHEO and SPASS performed in the problem library TPTP
reveal the high potential of our cooperation approaches.

## 1. Introduction

Automated deduction is —at its lowest level—a search problem that spans huge search spaces. In the past many different calculi have been developed in order to cope with problems from the area of automated theorem proving. Essentially, for first-order theorem proving two main paradigms for calculi are in use: Top-down calculi like model elimination (ME, Loveland, 1968, 1978) attempt to recursively break down and transform a goal into sssees that can finally be proven immediately with the axioms or with assumptions made during the proof. Bottom-up calculi like superposition (e.g., Bachmair & Ganzinger, 1994)
go the other way by producing logic consequences from the input set until an obvious inconsistency is derived.

When comparing results of vanous provers (e.g., Sutcliffe & Suttner, 1997) it is obvious that provers based on different paradigms often behave quite differently. There are problems w here bottom-up theorem provers perform considerably well, but top-down provers poorly, and vice versa. The main reason for this is that bottom-up provers often suffer from the lack of goal-orientation of their search, but profit from their strong redundancy control mechanisms. In contrast, top-down provers profit from their goal-orientation but suffer from insufficient redundancy control. This entails long proof lengths for many problems