FTP 2009 is the seventh 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 workshop welcomes original contributions on theorem proving in first-order classical, many-valued, modal and description logics, including (but not restricted to):

theorem proving in first-order classical, many-valued, and modal logics, including:

satisfiability in propositional logic,

satisfiability modulo theories,

specialized decision procedures,

constraint reasoning,

equational reasoning,

term rewriting,

resolution

paramodulation/superposition;

strategies and complexity of theorem proving procedures;

implementation techniques

applications of first-order theorem provers to:

program verification,

model checking,

artificial intelligence,

mathematics,

computational linguistics.

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). For more information about FTP, its scope and previous workshops, please see the FTP Workshop Series web page.

Invited speakers:

Silvio Ghilardi, Universita degli Studi di Milano, Italy

Peter Jeavons, Oxford University Computing Laboratory, UK (with Tableaux)

Paper Submissions

Authors are invited to submit papers in the following categories:

Extended abstracts of up to 15 pages describing original results.

Position papers of up to 10 pages describing work in progress, or future directions of research.

System descriptions of up to 10 pages, describing new systems or significant upgrades of existing ones, especially including experiments; sources and manuals of systems will have to be freely available online.

Presentation-only papers, describing work recently published or submitted (no page limit). These will not be included in the proceedings, but pre-prints or post-prints can be made available to participants. We see this as a way to provide additional access to important developments that FTP Workshop attendees may be unaware of.

Authors are encouraged to use LaTeX and the standard article class/style file (10pt or 11pt). The first page should contain the title, the authors' names, e-mail and postal addresses. Submissions should be made via Easychair at the following address: http://www.easychair.org/conferences/?conf=ftp2009

Publication

Accepted submissions will be published as a technical report of the University of Oslo and will be distributed at the workshop. They will also be available on the web. As for the previous editions of FTP, a journal special issue is planned after the workshop. The submission will be open to papers on First-Order Theorem Proving.

News (November 2009):

We plan a special issue dedicated to the topics of FTP 2009 in the Journal of Symbolic Computation.
The submission will be open, i.e. not restricted to papers accepted to FTP'2009. The call for papers will be posted soon.

Important dates (extended)

Full paper submission deadline:	4 May 2009 (24:00 GMT)
Notification of acceptance/rejection:	2 June 2009
Final version due:	11 June 2009
Workshop:	6-7 July 2009

Program Chairs

Nicolas Peltier and Viorica Sofronie-Stokkermans

Local organization

Roger Antonsen

Programme Committee

Alessandro Armando (DIST - University of Genova)

Franz Baader (TU Dresden)

Peter Baumgartner (National ICT Australia)

Bernhard Beckert (University of Koblenz)

Maria Paola Bonacina (Università degli Studi di Verona)

Ricardo Caferra (Grenoble INP - LIG)

Martin Giese (University of Oslo)

Ullrich Hustadt (University of Liverpool)

Alexander Leitsch (Vienna University of Technology)

Christopher Lynch (Clarkson University)

Nicola Olivetti (LSIS, Université Paul Cézanne, Marseille)

Nicolas Peltier (CNRS - LIG) (co-chair)

David Plaisted (University of North Carolina-Chapel Hill)

Silvio Ranise (Università degli Studi di Verona)

Michael Rusinowitch (LORIA - INRIA Lorraine)

Renate Schmidt (The University of Manchester)

Viorica Sofronie-Stokkermans (Max-Planck-Institut für Informatik, Saarbrücken) (co-chair)

Arild Waaler (University of Oslo)

Christoph Weidenbach (Max-Planck-Institut für Informatik, Saarbrücken)