The efficiency of theorem proving strategies

En savoir plus sur le livre

This second and slightly revised edition addresses previous errors and incorporates additional references based on reader feedback from the first edition. The focus is on analyzing the search efficiency of various refutational theorem proving strategies applied to propositional and near-propositional problems. The evaluation centers on the total number of proofs and partial proofs generated, rather than their sizes. Findings indicate that most common strategies result in exponential search spaces, even with simple clause sets, or lack sensitivity to the goal. In contrast, clause linking, which reduces problems to propositional calculus, demonstrates more favorable characteristics, akin to methods that cache subgoals. The A-ordering strategy, relevant for term-rewriting based theorem proving, is examined in detail, revealing advantages that may clarify its practical efficiency, alongside some combinatorial inefficiencies regarding goal sensitivity and irrelevant clauses. Additionally, SLD-resolution, significant for Prolog implementations, exhibits combinatorial inefficiencies, suggesting a potential shift to alternative theorem proving strategies. Techniques for analyzing the asymptotic complexity of first-order theorem provers are also developed, enabling a comparative analysis of the worst-case performances of different theorem proving methods.