The First-Order Complexity of First-Order Theorem Proving Strategies

Abstract

We would like to study the complexity of first-order theorem proving procedures. A first-order theorem prover typically takes as input a formula A of first-order logic and, if the formula is valid, eventually outputs a proof. Otherwise, the prover may run forever. Since first-order logic is only partially decidable, this is the best we can hope for. One can easily show that there can be no recursive bound on the length of the running time in terms of the length of the input, even for valid formulas. This makes it appear impossible to do any meaningful complexity analysis, since it is impossible to have a theorem prover with, say, exponential running time. However, we would like some kind of an asymptotic complexity analysis, because it would give valuable and machine-independent insight into theorem provers, insight that is difficult to obtain by running examples alone. A theoretical analysis, for example, can tell us something about the behavior of a prover on infinite classes of problems, which cannot be determined by running examples. Such an analysis would enable us to say in a rigorous way what it means for one theorem proving method to be better than another, at least on certain kinds of problems, and would enable us to pose interesting open questions about the existence of theorem provers of various complexities. It would also suggests new approaches to theorem proving, as we will show, approaches that might not have been considered otherwise. Of course, experimental studies of theorem provers provide additional information that should be combined with theoretical insights to obtain a complete picture.