First-order theorem proving (FTP) is among the most traditional disciplines in Artificial Intelligence. Its roots date back to the 1960s, which brought us milestones like the Davis-Putnam-Logemann-Loveland procedure for propositional logic and the resolution calculus for the first order logic. Since then, FTP has been an area of steady and active research. This is witnessed best by the existence of international conferences (CADE-the "Conference on Automated Deduction" being the most well-known) that have FTP as a core topic.
In the 1990s, the idea of a "Workshop on First-order Theorem Proving" was born as a (successful!) attempt to complement the international conferences by providing an informal forum for presentation of recent work and discussion of research in progress on FTP as a core theme of automated deduction. The call for papers mentions interest in first-order classical, many-valued and modal logics, resolution, equational reasoning, term-rewriting, model construction, constraint reasoning, unification, propositional logic, specialized decision procedures, strategies and complexity of theorem proving procedures, and applications of first-order theorem provers to problems in verification, artificial intelligence, and mathematics. (More information about the FTP workshop series is available from the web page http://www.logic.at/FTP/.) FTP 2000, the third workshop in the series, was held in the autumn of 2000 in St Andrews, Scotland, in conjunction with Tableaux 2000, the major international conference for automated reasoning with analytic tableaux and related methods. Following the tradition established by the First Workshop on FTP, this special issue of the Journal of Symbolic Computation has been edited to commemorate the success of FTP 2000.
There is no reason to limit submissions to the special issue to those papers that had been presented at FTP 2000. From a wider call for submissions we received 16 submissions, each of which was thoroughly reviewed. For most papers we asked two or three experts from the submissions' subject areas for reviews. One submission received was very controversial, and we eventually arrived at five reviews. As the result of the reviewing process 11 submissions were accepted.
The papers of this special issue match very well the scope of FTP cited above. More concretely:
Resolution theorem proving. The four papers dedicated to resolution based theorem proving propose different ways for improvements: the two papers by Nicolas Peltier, Model building with ordered resolution: extracting models from saturated clause sets and A calculus combining resolution and enumeration for building finite models deal