zbMATH — the first resource for mathematics

Eliminating dublication with the hyper-linking strategy. (English) Zbl 0784.68077
Summary: The efficiency of almost all theorem proving methods suffers from a phenomenon called duplication of instances of clauses. We present a novel technique, called the hyper-linking strategy, to eliminate such duplication. This strategy is complete for the full first-order predicate calculus. We show the effectiveness of this strategy by comparing it with other proving methods. We give empirical evidence that both the Davis- Putnam procedure and the hyper-linking strategy are comparable to each other and better than other common theorem proving strategies on propositional calculus problems. The fact that the Davis-Putnam procedure is faster than resolution and other common methods on propositional problems seems not be appreciated by a large segment of the theorem proving community. Also, we give empirical evidence that the hyper- linking strategy is better than other common theorem proving methods on near-propositional problems like logic puzzles. We attempt to explain the superior behavior of the hyper-linking strategy and the Davis-Putnam procedure by examining the kinds of duplication that can occur during the search with the different methods. In addition, we show the completeness of the hyper-linking strategy combined with several support strategies.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI