Computer Science – Artificial Intelligence
Scientific paper
2011-05-27
Journal Of Artificial Intelligence Research, Volume 10, pages 169-198, 1999
Computer Science
Artificial Intelligence
Scientific paper
10.1613/jair.573
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 top-down prover generates subgoal clauses, they are then processed by a bottom-up prover. The second technique deals with the use of bottom-up generated lemmas in a top-down prover. 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.
Fuchs Dmitry
Fuchs Madeleine
No associations
LandOfFree
Cooperation between Top-Down and Bottom-Up Theorem Provers does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Cooperation between Top-Down and Bottom-Up Theorem Provers, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Cooperation between Top-Down and Bottom-Up Theorem Provers will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-664469