International Workshop on
First-Order Theorem Proving

Universidad Politécnica de Valencia,
Valencia, Spain
June 12-14, 2003



FTP'2003 is 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 workshop welcomes original contributions on theorem proving in first-order classical, many-valued, modal and description logics, including nonexclusively: 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.



Papers accepted for presentation are published in Technical Report DSIC-II/10/03, Universidad Politécnica de Valencia, 2003.
Papers accepted for publication are published in the ENTCS series (Electronic Notes in Theoretical Computer Science, volume 86 n.1).

JAR special issue:

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'2003, or new papers devoted to First-Order Theorem Proving. All these papers will go through a new review process.
The journal that will publish this special issue if the Journal of Automated Reasoning (JAR).
For more information, please visit the following web page: http://rewriting.loria.fr/FTP-2003/jar/

Workshop Organization

Program Co-Chairs:

Ingo Dahn, Universität Koblenz-Landau, Germany
dahn @ uni-koblenz.de

Laurent Vigneron, LORIA - Université Nancy 2, France
vigneron @ loria.fr

Program Committee:

Maria Paola Bonacina (Univ. Verona, Italy)
Ricardo Caferra (LEIBNIZ-IMAG, Grenoble, France)
Bernhard Gramlich (TU Wien, Vienna, Austria)
Paliath Narendran (SUNY at Albany, USA)
David Plaisted (UNC at Chapel Hill, USA)
Christophe Ringeissen (LORIA-INRIA Lorraine, Nancy, France)
Albert Rubio (UPC, Barcelona, Spain)
John Slaney (ANU, Canberra, Australia)
Tomàs Uribe (SRI Int., Menlo Park, USA)
Luca Viganò (ETHZ, Zürich, Switzerland)
Christoph Weidenbach (Opel / MPI Saarbrücken, Germany)
Hantao Zhang (Univ. of Iowa, Iowa City, USA)

Local Organization Chair:

Salvador Lucas
Universidad Politécnica de Valencia, Spain
slucas @ dsic.upv.es

FTP Steering Committee:

Alessandro Armando (Univ. di Genova, Italy)
Peter Baumgartner (Univ. Koblenz, Germany)
Maria Paola Bonacina, Chair (Univ. of Verona, Italy)
Ricardo Caferra (LEIBNIZ-IMAG, Grenoble, France)
Domenico Cantone (Univ. di Catania, Italy)
David Crocker (Escher Technologies Ltd., UK)
Ingo Dahn (Univ. Koblenz-Landau, Germany)
Bernhard Gramlich (Technische Univ. Wien, Austria)
Reiner Hähnle (Chalmers Univ. of Technology, Göteborg, Sweden)
Alexander Leitsch (Technische Univ. Wien, Austria)
Paliath Narendran (Univ. at Albany - SUNY, Albany, NY, USA)
Christoph Weidenbach (MPI Saarbrücken & Opel AG, Germany)

Invited Talks

Enrico Giunchiglia (DIST, Genova, Italy)
SAT and Beyond SAT
Thomas Hillenbrand (MPI, Saarbrücken, Germany)
Citius altius fortius: Lessons learned from the Theorem Prover WALDMEISTER
Dieter Hutter (DFKI, Saarbrücken, Germany)
Deduction as an Engineering Science

Related links

Laurent Vigneron
Last modified: 24-Mar-2005