Cooperation between Top-Down and Bottom-Up Theorem Provers

摘要

Top-down and bottom-up theorem proving approaches each have specificadvantages and disadvantages. Bottom-up provers profit from strong redundancycontrol but suffer from the lack of goal-orientation, whereas top-down proversare goal-oriented but often have weak calculi when their proof lengths areconsidered. In order to integrate both approaches, we try to achievecooperation 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. Atop-down prover generates subgoal clauses, they are then processed by abottom-up prover. The second technique deals with the use of bottom-upgenerated lemmas in a top-down prover. We apply our concept to the areas ofmodel elimination and superposition. We discuss the ability of our techniquesto shorten proofs as well as to reorder the search space in an appropriatemanner. Furthermore, in order to identify subgoal clauses and lemmas which areactually relevant for the proof task, we develop methods for a relevancy-basedfiltering. Experiments with the provers SETHEO and SPASS performed in theproblem library TPTP reveal the high potential of our cooperation approaches.