It seems to me (at least according to books and papers on the subject I read) that the field of automated theorem proving is some sort of art or experimental empirical engineering of combining various approaches, but not a science which tries to explain WHY its methods work in various situations and to find classes of situations for which they work. Or may be I am not aware of some results or the problem is too hard.


Has it been clarified in a rigorous way why, for example, Robinson's resolution works better than Gilmore's saturation? 
(intuitive reason of course is that most general unifier already contains all information about infinitely many terms from Herbrand's universe, but it is only intuition, not a concrete reason, as well as the fact that you can not know when to stop searching for a proof of a formula A in the case A and not(A) are both unprovable is not a rigorous explanation of undecidability of first order logic). 


I even saw a paper shows that there are cases in which London museum algorithm (brute force search, essentially) performs better than resolution! 


Maybe somebody have found some large classes of formulas on which resolution works well?  

Maybe some probabilistic analysis of proving methods?


Thanks in advance.



Reasons for success in automated theorem proving
You may be interested in the wonderful little book ``The Efficiency of Theorem Proving Strategies: A Comparative and Asymptotic Analysis'' by David A. Plaisted and Yunshan Zhu. I have the 2nd edition which is paperback and was quite cheap. I'll paste the (accurate) blurb:


``This book is unique in that it gives asymptotic bounds on the sizes of the search spaces generated by many common theorem-proving strategies. Thus it permits one to gain a theoretical understanding of the efficiencies of many different theorem-proving methods. This is a fundamental new tool in the comparative study of theorem proving strategies.''


Now, from a critical perspective: There is no doubt that sophisticated asymptotic analyses such as these are very important (and to me, the ideas underlying them are beautiful and profound). But, from the perspective of the practitioner actually *using* automated theorem provers, these analyses are often too coarse to be of practical use. A related phenomenon occurs with decision procedures for real closed fields. Since Davenport-Heinz, it's been known that general quantifier elimination over real closed fields is inherently doubly-exponential w.r.t. the number of variables in an input Tarski formula. One full RCF quantifier-elimination method having this doubly-exponential complexity is CAD of Collins. But, many (Renegar, Grigor'ev/Vorobjov, Canny, ...) have given singly exponential procedures for the purely existential fragment. Hoon Hong has performed an interesting analysis of this situation. The asymptotic complexities of three decision procedures considered by Hong in ``Comparison of Several Decision Algorithms for the Existential Theory of the Reals'' are as follows:


(Let $n$ be the number of variables, $m$ the number of polynomials, $d$ their total degree, and $L$ the bit-width of the coefficients)


CAD: $L^3(md)^{2^{O(n)}}$


Grigor'ev/Vorobjov: $L(md)^{n^2}$


Renegar: $L(log L)(log log L)(md)^{O(n)}$


Thus, for purely existential formulae, one would expect the G/V and R algorithms to vastly out-perform CAD. But, in practice, this is not so. In the paper cited, Hong presents reasons why, with the main point being that the asymptotic analyses ignore huge lurking constant factors which make the singly-exponential algorithms non-applicable in practice. In the examples he gives ($n=m=d=L=2$), CAD would decide an input sentence in a fraction of a second, whereas the singly-exponential procedures would take more than a million years. The moral seems to be a reminder of the fact that a complexity-theoretic speed-up w.r.t. *sufficiently large* input problems should not be confused with a speed-up w.r.t. *practical* input problems.


In any case, I think the situation with asymptotic analyses in automated theorem proving is similar. Such analyses are important theoretical advances, but often are too coarse to influence the day-to-day practitioner who is using automated theorem proving tools in practice.


(\* One should mention Galen Huntington's beautiful 2008 PhD thesis at Berkeley under Branden Fitelson in which he shows that Canny's singly-exponential procedure can be made to work on the small examples considered by Hong in the above paper. This is significant progress. It still does not compare in practice to the doubly-exponential CAD, though.)


