International Workshops on First-Order Theorem Proving (FTP)

Mission

The series of FTP workshops is intended to focus effort on First-Order Theorem Proving as a core theme of Automated Deduction, and to provide a forum for presentation of very recent work and discussion of research in progress. The workshops welcome original contributions on theorem proving in first-order classical, many-valued, and modal logics, including resolution, equational reasoning, term rewriting, model construction, constraint reasoning, unification, propositional logic, specialized decision procedures; strategies and complexity of theorem proving procedures; and applications of first-order theorem provers to problems in verification, artificial intelligence, and mathematics.

Past workshops

• FTP'97, Schloss Hagenberg, Austria, October 27-28, 1997

  • Special Issue of the Journal of Symbolic Computation on Advances in First-order Theorem Proving, Maria Paola Bonacina and Ulrich Furbach, editors, Vol. 29, Issue 2, Pages 117-392 (February 2000), Elsevier, 2000 (selected full papers from an open cfp launched after FTP'97)

• FTP'98, Schloss Wilhelminenberg, Vienna, Austria, November 23-25, 1998

  • Automated Deduction in Classical and Non-Classical Logics - Selected Papers, Ricardo Caferra and Gernot Salzer, editors, Lecture Notes in Artificial Intelligence, Vol. 1761, Springer, 2000 (invited papers and selected full papers from an open cfp launched after FTP'98)

• FTP'00, University of St Andrews, Scotland, July 3-5, 2000

  • Special Issue of the Journal of Symbolic Computation on First-Order Theorem Proving, Peter Baumgartner and Hantao Zhang, editors, Vol. 36, Issues 1-2, Pages 1-285 (July - August 2003), Elsevier, 2003 (selected full papers from an open cfp launched after FTP'00)

• IJCAR'01 (= CADE + FTP + TABLEAUX), Siena, Italy, June 18-23, 2001

  • Automated Reasoning, First International Joint Conference, IJCAR 2001 Siena, Italy, June 18-23, 2001, Proceedings, Rajeev Goré, Alexander Leitsch and Tobias Nipkow, editors, Lecture Notes in Computer Science 2083, Springer, 2001

• FTP'03 (see also here), Valencia, Spain, June 12-14, 2003 (collocated with RTA'03 and TLCA'03, part of RDP'03)

  • Special Issue of the Journal of Automated Reasoning on First-Order Theorem Proving (Volume 33, numbers 3-4, see here)

• IJCAR'04 (= CADE + CALCULEMUS + FroCoS + FTP + TABLEAUX), Cork, Ireland, July 4-9, 2004

  • Automated Reasoning, Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, David A. Basin and Michael Rusinowitch, eds., Lecture Notes in Computer Science 3097, Springer, 2004

• FTP'05, Koblenz, September 14-17, 2005 (collocated with TABLEAUX 2005, back-to-back with KI 2005)

• IJCAR'06 (= CADE + FroCoS + FTP + TABLEAUX + TPHOLs), Seattle, USA, August 16 - 21, 2006

  • Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, Ulrich Furbach and Natarajan Shankar, eds., Lecture Notes in Computer Science 4130, Springer, 2006

• FTP'07, Liverpool, United Kingdom, September 12-13, 2007 (collocated with FroCoS 2007)

  • Special Issue of the Annals of Mathematics and Artificial Intelligence on First-Order Theorem Proving, Silvio Ranise and Ullrich Hustadt, editors,
    (for additional information see the Call for Papers)

• FTP 2009, Oslo, Norway, July 6-7, 2009 (collocated with Tableaux 2009)

  • Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09), Oslo, Norway, July 6-7, 2009, Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, CEUR Workshop Proceedings 556 CEUR-WS.org, January 2010.
    Appeared in printed version as Research Report 386, University of Oslo, Department of Informatics, 2009, ISBN 82-7368-347-8, ISSN 0806-3036.

  • Special Issue of the Journal of Symbolic Computation on First-Order Theorem Proving, Nicolas Peltier and Viorica Sofronie-Stokkermans, editors,
    (for additional information see the Call for Papers)

• FTP 2011, Bern, Switzerland, July 4, 2011 (collocated with Tableaux 2011)

  • TABLEAUX 2011 Workshops, Tutorials, and Short Papers, Martin Giese and Roman Kuznets (editors), Technical Report, Institut für Informatik und angewandte Mathematik, Universität Bern, 2011.

Future workshops

• To be announced

Steering Committee

The Steering Committee is responsible for choosing location, local arrangement and program chairs for each workshop, as well as for making general decisions concerning the future of the workshop series. The committee consists of twelve persons, each serving for three terms (=three successive workshops). Around the time of each workshop four members of the committee step down, and the vacant positions are filled by holding elections among the FTP community. The FTP community consists of all people having participated in any FTP workshop, of all current and former members of the steering committee, and of all members of the current or former program committees.

President:
Ullrich Hustadt, University of Liverpool, UK (elected June 2006)

Members:
Alessandro Armando, Università di Genova, Italy (elected Oct.2001)
Ingo Dahn, Universität Koblenz-Landau, Germany (elected Oct.2001)
Ullrich Hustadt, University of Liverpool, UK (elected Nov.2005)
Paliath Narendran, University at Albany - SUNY, Albany, New York, USA (elected Oct.2001)
Nicolas Peltier, CNRS, France (elected Nov.2003)
Silvio Ranise, Fondazione Bruno Kessler, Italy (elected Nov.2005)
Stephan Schulz, RISC-Linz, Austria (elected Nov.2003)
Gernot Stenz, Technische Universität München, Germany (elected Nov.2005)
Cesare Tinelli, University of Iowa, USA (elected Nov.2003)
Luca Viganò, Università di Verona, Italy (elected Nov.2003)
Laurent Vigneron, LORIA - University Nancy 2, France (elected Nov.2003)

Former Members:
Peter Baumgartner, NICTA, Canberra, Australia (Oct.2000-Nov.2005, president 2003-2005)
Maria Paola Bonacina, University of Verona (FTP 1997-Nov.2003, president 1999-2003)
Ricardo Caferra, LEIBNIZ-IMAG, Grenoble, France (Jan.1999-Nov.2003)
Domenico Cantone, Universitá di Catania, Italy (Jan.1999-Nov.2003)
David Crocker, Escher Technologies Ltd., UK (Oct.2000-Nov.2005)
Ulrich Furbach, Universität Koblenz, Germany (FTP 1997-Oct.2000)
Bernhard Gramlich, Technische Universität Wien, Austria (Oct.2000-Nov.2005)
Reiner Hähnle, Chalmers University of Technology, Göteborg, Sweden (Oct.2000-Nov.2005)
Jieh Hsiang, National Taiwan University, Taipei, Taiwan (FTP 1997-Jan.1999)
Alexander Leitsch, Technische Universität Wien, Austria (Jan.1999-Nov.2003)
Christopher Lynch, Clarkson University, USA (FTP 1997-Oct.2001)
William McCune, University of New Mexico, USA (elected Nov.2005)
Xumin Nie, Oracle, USA (FTP 1997-Oct.2001)
David Plaisted, UNC at Chapel Hill, USA (FTP 1997-Oct.2000, president 1997-1999)
Michael Rusinowitch, LORIA, Nancy, France (FTP 1997-Oct.2001)
Gernot Salzer, Technische Universität Wien, Austria (FTP 1997-Oct.2000)
Camilla Schwind, Université Aix-Marseille II, France (FTP 1997-Oct.2000)
Klaus Trümper, University of Texas at Dallas, USA (FTP 1997-Jan.1999)
Christoph Weidenbach, MPI Saarbrücken, Germany (Jan.1999-Nov.2003)
Hantao Zhang, University of Iowa, USA (FTP 1997-Jan.1999)