UNSEARCHMO: eliminating redundant search space on backtracking for forward chaining theorem proving
Lifeng He · International Joint Conference on Artificial Intelligence · 2001
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.