Improving efficiency of a theorem prover by eliminating redundant unifications using network structures

S.-J. Lee and D. Plaisted (J. Automated Reasoning, vol.8, pp. 25-42, 1992) proposed a theorem proving method, called the hyper-linking strategy, in order to eliminate the duplication of instances of clauses during the process of inference. A theorem prover, which implements the strategy, was also constructed. In this implementation, many literal unifications and partial unifications are performed repetitively from round to round, resulting in a large overhead when many rounds of hyper-linking are needed for hard problems. We propose a technique which maintains information across rounds by constructing shared network structures, so that redundant work on calculating literal unifications and partial unifications, and on duplicate instance checking in each hyper-linking round is avoided. Experiments show that the overhead is reduced significantly when the required number of rounds is large