Lemma Generation for Model Elimination by Combining Top-Down and Bottom-up Inference
Abstract
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.
Cite
Text
Fuchs. "Lemma Generation for Model Elimination by Combining Top-Down and Bottom-up Inference." International Joint Conference on Artificial Intelligence, 1999.Markdown
[Fuchs. "Lemma Generation for Model Elimination by Combining Top-Down and Bottom-up Inference." International Joint Conference on Artificial Intelligence, 1999.](https://mlanthology.org/ijcai/1999/fuchs1999ijcai-lemma/)BibTeX
@inproceedings{fuchs1999ijcai-lemma,
title = {{Lemma Generation for Model Elimination by Combining Top-Down and Bottom-up Inference}},
author = {Fuchs, Marc},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1999},
pages = {4-9},
url = {https://mlanthology.org/ijcai/1999/fuchs1999ijcai-lemma/}
}