The role of first-order theorem proving as a core theme of automated deduction has been recognized since the beginning of the field, at the dawn of artificial intelligence, more than 40 years ago. Although many other logics have been developed and used in AI, deduction systems based on first-order theorem proving have recently achieved considerable successes and even mention in the general press. It was a first-order theorem prover that first proved the Robbins algebra conjecture, and thus reached the New York Times Science section (NY Times, Dec. 10, 1996).
Not only in proving mathematical theorems, but also in various other disciplines of AI, first-order theorem proving has made substantial progress. In planning, for example, it turns out that propositional theorem provers are able to outperform special-purpose planning systems on some problems. This is remarkable, since it was considered folklore that planning required specialized algorithms. Similar developments can be observed in the field of model-based diagnosis. In knowledge representation, simple techniques from resolution or tableaux methods can be used to build kernel systems.
Over the years, the impact of first-order theorem proving has grown beyond artificial intelligence, connecting with both computational logic (e.g. logic and functional programming, deductive databases) and symbolic computation (e.g. constraint problem solving, rewriting techniques, computer algebra), while a continued major motivation for research in theorem proving has come from its applications to verification. In a nutshell, first-order theorem proving is the heart of automated deduction, at the intersection of symbolic computation, computational logic, and artificial intelligence.
An international workshop on first-order theorem proving, FTP'97, was organized by the guest editors in October 1997 at Schloss Hagenberg near Linz. Twenty-five extended abstracts were presented at the workshop and are available at http://www.logic.at/ ftp97/. The workshop was successful and became a starting point for a call for paper for this special issue. Eighteen papers were submitted to this special issue, and with the help of thirty peer reviewers, eight were selected for publication.
The selected papers reflect the diversity of research at the frontier of the field, including papers on core theorem proving topics (e.g. use of lemmas in tableaux, theory reasoning), integration of methodologies (e.g. theorem proving and model building), applications (e.g. in deductive databases), and logical foundations (e.g. proof theory and algebraic logic).
To emphasize the applications of theorem proving, the volume is opened by the paper of Chandrabose Aravindan and Peter Baumgartner, who show how theorem-proving techniques enable the reduction, from exponential to polynomial, of the space complexity of certain database updates. The second paper, by Matthias Baaz and Alexander Leitsch, brings the reader back to the foundations of theorem proving in proof theory, with an