Eliminating Redundant Search Space on Backtracking for Forward Chaining Theorem Proving

This paper introduces some improvements on the intelligentbacktracking strategy for forward chaining theorem proving.How to decide a minimal useful consequent atom set for arefutation derived at a node in a proof tree is discussed. In most cases, anunnecessary non-Horn clause used for forward chaining will be split onlyonce. The increase of the search space by invoking unnecessary forwardchaining clauses will be nearly linear, not exponential anymore. In thispaper, the principle of the proposed method and its correctness areintroduced. Moreover, some examples are provided to show that theproposed approach is powerful for forward chaining theorem proving.