Preface

               Nicolas Peltier1 and Viorica Sofronie-Stokkermans2
                        1
                         LIG, Grenoble INP/CNRS, France
           2
               Max-Planck-Institut für Informatik, Saarbrücken, Germany

    This volume contains the papers presented at the International Workshop
on First-Order Theorem Proving (FTP 2009) held in Oslo, Norway, on July
6–7, 2009. First-order theorem proving is widely recognized as a core theme of
automated deduction and has achieved considerable successes in the last decades.
FTP 2009 is the seventh in a series of workshops intended to focus effort on
first-order theorem proving by providing a forum for presentation of recent work
and discussion of research in progress. The FTP workshop is held since 1997;
its aim is to bring together researchers interested in all aspects of first-order
theorem proving. It welcomes original contributions on theorem proving in first-
order classical, many-valued, modal and description logics. Previous editions of
FTP took place in Schloss Hagenberg, Austria (1997); Vienna, Austria (1998);
St Andrews, Scotland (2000); Valencia, Spain (2003); Koblenz, Germany (2005)
and Liverpool, UK (2007).
    FTP 2009 was held together with the 18th International Conference on Au-
tomated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX
2009, web page: tableaux09.ifi.uio.no). On July 7, 2009 there was a joint session
with TABLEAUX 2009 with Peter Jeavons as (joint) invited speaker.
    The technical program of FTP 2009 consists of two invited talks on by Sil-
vio Ghilardi on “Model-Checking of Array-Based Systems: from Foundations to
Implementation” and one by Peter Jeavons on “Presenting Constraints” (joint
with Tableaux 2009), eight regular papers and two position papers. The topics
of these papers match very well those of the workshop, ranging from the theo-
retical foundations of first-order theorem proving to practical applications, e.g.
in verification and web technology.
    Many people contributed to make this workshop possible and we sincerely
thank all of them. First of all, we would like to thank all the scientists who
submitted interesting papers and abstracts to FTP 2009 and the invited speakers
for agreeing to speak at the workshop. Many thanks also to all the attendees
for contributing to the intensive exchange of ideas in the workshop. We also
thank all the members of the Program Committee and the additional reviewers
for their excellent job and for their thorough and quick reviews. We are very
grateful to the local organisers (in particular Roger Antonsen, Martin Giese and
Arild Waaler) for their numerous advices, constant support and for taking care
of practical matters. We thank the Norwegian Research Council and the Dept.
of Informatics at the University of Oslo for their generous financial support. We
also would like to thank the steering committee, in particular Ullrich Hustadt
for their strong support to the FTP workshop series.