In this paper, a comparison is made of several proof calculi in terms of
the lengths of shortest proofs for some given formula of first order
predicate logic with function symbols. In particular, we address the
question whether, given two calculi, any derivation in one of them can
be simulated in the other in polynomial time. The analogous question for
propositional logic has been intensively studied by various authors
because of its implications for complexity theory. And it seems there
has not been as much endeavour in this field in first order logic as
there has been in propositional logic. On the other hand, fOr most of
the practical applications of logic, a powerful tool such as the
language of first order logic is needed. The main interest of this
investigation lies in the calculi most frequently used in automated
theorem proving, the resolution calculus, and analytic calculi such as
the tableau calculus and the connection method. In automated theorem
proving there are two important aspects of complexity. In order to have
a good theorem proving system, we must first have some calculus in which
we can express our derivations in concise form. And second, there must
be an efficient search strategy. This book deals mainly with the first
aspect which is a necessary condition for the second since the length of
a shortest proof always also gives a lower bound to the complexity of
any strategy.