No label defined (Q4345253)

Motivation: Before summarizing the main results of the book, we give a brief introduction to (automated) theorem proving and relevant problems. In this field, various specialized algorithmic methods implemented as theorem provers have been investigated for verifying the truth of logical statements often specified in first-order predicate logic. For applications of such provers, efficiency plays a major role. The efficiency of a theorem prover is not only measured in terms of the size of the final proof, it is better defined by the total number of inferences performed to find a proof. There exist various tests (for example, based on the TPTP benchmark library for automated theorem proving systems) for determining the experimental efficiency. But analytical results can hardly be found, although a theoretical study would `make general statements and be machine-independent whereas experiments tends to deal in specifics and to be machine-dependent'. Brief overview on the contents: The main contribution of the book is a list of asymptotic bounds on the sizes of the search spaces generated by various theorem proving strategies. Plaisted and Zhu considered the sizes of the search spaces (in contrary to the length of proofs as done by most logicians) produced by clause form refutational theorem proving strategies for first-order logic. The first part of the book concerns the propositional complexity of various strategies including hyper-resolution, resolution with A-ordering, all-negative resolution with and without ordering, SLD-resolution, model elimination with and without lemmas and caching, and clause linking. The main results in this area are the following ones: Most of the strategies perform very badly on simple set theory problems, logic puzzles, and even propositional calculus problems. Further, backward chaining strategies need to use caching. Forward chaining strategies generally seem to do well on Horn sets, but badly on non-Horn sets. In the second part of the book, the first-order complexity of diverse strategies are studied. Because of just semi-decidability it appears impossible to do any meaningful complexity analysis. Thus, several different kinds of asymptotic complexity measures are used instead. The most natural measures seem to be subterm size and duplication. Among others, the following strategies are analyzed wrt. these measures: Resolution, model elimination, clause linking, and the matings method. One of the consequences of the complexity analyses is that for hard problems, the lengths of the proofs and the duplication complexity will likely be large, i.e. that even a method that is single exponential wrt. the duplication complexity will probably be too slow. On the other side, the matings method is exponential wrt. the duplication complexity, but has found some fairly interesting proofs. All in all, as the authors conclude, `especially ordered semantic hyper-linking have the most long-term promise for a generally useful theorem prover'. Related Work: In an unpublished paper by Kleine Buening and Lettman from 1993, the search space sizes of monotone refinements of resolution (where deletion operations are not allowed) are considered. It has been shown that these kinds of calculi do not increase a certain measure of search space size by more than a factor of four. But general results are not proven. Judgement: One can see that much can be said about the complexities of various theorem proving strategies on various kinds of input clauses. As already mentioned above, some practical benefit can be expected from the theoretical results. The book addresses both theorists and practicians since it is written in a formal (and at the same time amusing) style as well as with motivating remarks for applying the results in practice. What is lacking is the analysis of strategies with special semantics and equality handling. The authors also fail to take into account the (non-trivial) differences in implementing steps that are often considered elementary in describing theorem proving procedures. Further, the (coarse) complexity classification could be refined in order to give additional insights. Although not everybody agrees with the authors' estimation of the hyper-linking method, the work of Plaisted and Zhu is really worth reading.