Lemma generation for model elimination by combining top-down and bottom-up inference
M. Fuchs · International Joint Conference on Artificial Intelligence · 1999
A very promising approach for integrating top-down and bottom-up proof search is the use of bottom-up generated lemmas in top-down provers. When generating lemmas, however) the currently used lemma generation procedures suffer from the well-known problems of forward reasoning methods, e.g., the proof goal is ignored. In order to overcome these problems we propose two relevancy-based lemma generation methods for top-down provers. The first approach employs a bottom-up level saturation procedure controlled by top-down generated patterns which represent promising subgoals. The second approach uses evolutionary search and provides a self-adaptive control of lemma generation and goal decomposition.