UNSEARCHMO: Eliminating Redundant Search Space on Backtracking for Forward Chaining Theorem Proving
Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence. Pages 618-622.
Abstract
This paper introduces how to eliminate redundant search space for forward chaining theorem proving as much as possible. We consider how to keep on minimal useful consequent atom sets for necessary branches in a proof tree. In the most cases, an unnecessary non-Horn clause used for forward chaining will be split only once. The increase of the search space by invoking unnecessary forward chaining clauses will be nearly linear, not exponential anymore. In a certain sense, we “unsearch” more than necessary. We explain the principle of our method, and provide an example to show that our approach is powerful for forward chaining theorem proving.
@inproceedings{ijcai2001p86,
title = {UNSEARCHMO: Eliminating Redundant Search Space on Backtracking for Forward Chaining Theorem Proving},
author = {He, Lifeng},
booktitle = {Proceedings of the Seventeenth International Joint Conference on
Artificial Intelligence, {IJCAI-01}},
publisher = {International Joint Conferences on Artificial Intelligence},
pages = {618--622},
year = {2001},
url = {https://ijcai.org/proceedings/2001/86},
}
TY - CPAPER TI - UNSEARCHMO: Eliminating Redundant Search Space on Backtracking for Forward Chaining Theorem Proving AU - He, Lifeng T2 - Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI-01 PB - International Joint Conferences on Artificial Intelligence PY - 2001 SP - 618 EP - 622 UR - https://ijcai.org/proceedings/2001/86 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
