FTP'2005
International Workshop on
First-Order Theorem Proving Koblenz, Germany
September 14-17, 2005 Co-located with TABLEAUX
2005
Back-to-back with KI 2005
|
FTP'2005 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 nonexclusively: resolution, tableau methods, 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.
Papers accepted for presentation
are published in a Technical Report of the University of Koblenz and
will be available at the workshop.
As for the previous editions of
FTP, a special issue of a journal is prepared after the workshop. The
papers published in this journal will be either long versions of papers
presented at FTP'2005, or new papers devoted to First-Order Theorem
Proving. All these papers will go through a new review process.
Program Chair:
Reinhold Letz (Munich U. of Technology, Germany)
Program Committee:
Alessandro Armando (Univ. of Genova, Italy)
Bernhard Beckert (Univ. Koblenz-Landau, Germany)
Christian Fermüller (Vienna U. of Technology, Austria)
Bernhard Gramlich (Vienna U. of Technology, Austria)
Bernd Löchner (Univ. Kaiserslautern, Germany)
Chris Lynch (Clarkson Univ., USA)
Paliath Narendran (SUNY at Albany, USA)
Nicolas Peltier (IMAG, Grenoble, France)
Michael Rusinowitch (LORIA, Nancy, France)
Renate Schmidt (Univ. of Manchester, UK)
Miroslav Velev (Carnegie Mellon, USA)
Luca Viganò (ETHZ, Zürich, Switzerland)
Local Organization:
Bernhard Beckert
Gerd Beuster
Vladimir Klebanov
Thomas Kleemann
Jan Murray
Oliver Obst
Alex Sinner
Christoph Wernhard
FTP Steering Committee:
Alessandro Armando, Università di Genova, Italy (elected Oct.2001)
Peter Baumgartner, MPI Saarbrücken & Universität Koblenz-Landau, Germany (elected Oct.2000, president since 2003)
David Crocker, Escher Technologies Ltd., UK (elected Oct.2000)
Ingo Dahn, Universität Koblenz-Landau, Germany (elected Oct.2001)
Bernhard Gramlich, Technische Universität Wien, Austria (elected Oct.2000)
Reiner Hähnle, Chalmers University of Technology, Göteborg, Sweden (elected Oct.2000)
Paliath Narendran, University at Albany - SUNY, Albany, New York, USA (elected Oct.2001)
Nicolas Peltier, CNRS, France (elected Nov.2003)
Stephan Schulz, RISC-Linz, Austria (elected Nov.2003)
Cesare Tinelli, University of Iowa, USA (elected Nov.2003)
Luca Viganò, ETH Zürich, Switzerland (elected Nov.2003)
Laurent Vigneron, LORIA - University Nancy 2, France (elected Nov.2003)
The workshop will be held in conjunction with TABLEAUX 2005. TABLEAUX is the major international conference for automated reasoning with analytic tableaux and related methods. General information for the TABLEAUX conference series: http://i12www.ira.uka.de/TABLEAUX/.
| June 5, 2005 | Deadline for paper submissions |
| July 29, 2005 | Notification of acceptance |
| August 12, 2005 | Final versions due for proceedings |
| September 14-17, 2005 | FTP'2005 |
The conference will include research papers, system descriptions, position papers and invited lectures. Submissions are invited in three categories:
| A | Research papers (up to 12 pages) reporting original theoretical and/or experimental research |
| B | System descriptions (3-5 pages) describing new systems or significant upgrades of existing ones, especially including experiments; systems will have to be freely available online |
| C | Position papers (2 pages) describing the authors' research interests in the field, work in progress, or future directions of research |
All papers will be refereed by the program committee, and will be evaluated on their significance, technical merit, and relevance to the workshop. Papers accepted for presentation (except position papers) are published in a Technical Report of the University of Koblenz and will be available at the workshop. As for the previous editions of FTP, a special issue of a journal is planned after the workshop. The submission will be open to papers on First-Order Theorem Proving.
Authors of accepted papers are expected to present their work at the conference. For Category B submissions, a working implementation must exist.