5 added 200 characters in body

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.)

4 added 84 characters in body

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 the 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.

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.)

3 deleted 109 characters in body; added 8 characters in body

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 which is perhaps better known (due to real algebraic decision methods being a pillar of algorithmic algebra) 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. The asymptotic complexities of the three 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.

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.)