Simplification and Reduction for Automated Theorem Proving

Abstract

The most severe obstacle on the way to the efficient automation of theorem proving is the size of the search space for drawing new inferences. There are two well known ways to overcome this difficulty. One solution comes under the term ”refutation strategies”, which denotes techniques to choose candidates for the next inference step. The other solution is termed ”reduction", which subsumes all techniques to remove those elements of the search space that do not contribute to the solution and thus are redundant. The second approach’s most critical part is the test on redundancy. Since each element of the search space has to be subjected to such a test, its efficiency is crucial for the value of the reduction approach. Subsumption, being one of the most important types of redundancy, is also a most problematic one. In this thesis, new and efficient tests for the variant and the subsumption property are developed, both based on the well known algorithms for detecting isomorphism of directed graphs. A most undesired aspect of redundancy is the derivation of subsumed clauses. Besides the problem with the subsumption test, the amount of computer time, which is spent for the derivation and normalization of such a clause, is purely wasted. In this thesis, the two approaches, strategy and reduction, are combined by a strategy to decrease the number of redundant information derived. This strategy is heavily based on a special treatment of logical equivalence. It turns out that this strategy represents a first step towards the answer of several open questions in automated theorem proving, like the problem with the derivation of redundant clauses, the choice of the appropriate representation and inference rule, the question for a theory to demodulate on the literal level, and finally the choice of clauses to apply a given inference rule. These problems are discussed in Wos’ (1988) 33 Basic Research Problems.