This volume contains the proceedings of FTP'2003, the fourth in a series of workshops intended to focus effort on First-Order Theorem Proving as a core theme of Automated Deduction, and to provide a forum for presentation of recent work and discussion of research in progress. The previous workshops of this series were held at Schloss Hagenberg, Austria (1997), Vienna, Austria (1998), St Andrews, Scotland (2000). In 2001, FTP was part of the IJ
CAR Conference, held in Siena, Italy.
FTP'2003 is one of the three main events of the Federated Conference on Rewriting, Deduction and Programming (RDP'03), together with RTA (the 14th International Conference on Rewriting Techniques and Applications), and TLCA (the 6th International Conference on Typed Lambda Calculi and Applications). FTP'2003 was hold on June 12-14,2003, in Valencia, Spain.
The articles included in this volume represent a selection among the 16 papers presented at the workshop FTP'2003. In addition, two papers correspond to invited talks. The topics of these papers match very well those of the workshop which cover theorem proving in first-order classical, many-valued, modal and description logics, including non-exclusively: resolution, equational reasoning, term-rewriting, model construction, constraint reasoning, unification, description logics, propositional logic, specialized decision procedures; strategies and complexity of theorem proving procedures; implementation techniques and applications of first-order theorem provers to verification, artificial intelligence, mathematics and education.
We sincerely thank everyone who contributed to make this workshop possible and who participated to the selection of the papers for these proceedings. First of all, we would like to thank all the authors who contributed the papers to FTP'2003. We thank the members of the Program Committee and the additional reviewers for their excellent job. We also thank the Steering Committee, and Maria Paola Bonacina in particular, for their advice throughout all phases of the workshop. Finally, we thank Salvador Lucas and his collaborators of the University of Valencia, who did a very good work at preparing the local arrangements, and publishing the preliminary version of the papers published in this volume as Technical Report DSIC-II/10/03 of the Universidad Politécnica de Valencia.
Program Committee Chairs
Program Committee
Additional Referees
Alessandro Armando, Jüurgen Avenhaus, David Déharbe, Didier Galmiche, Florent Jacquemard, Alexandre Miquel, Raúl Monroy, Robert Nieuwenhuis, Silvio Ranise, Sophie Tison, Femke van Raamsdonk, Lida Wang.
FTP Steering Committee
Local Organization
María Alpuente, Salvador Lucas (chair), Javier Oliver, María José Ramírez, Germán Vidal, and all the ELP group at the Universidad Politécnica de Valencia.
