The Eighth International Workshop on First-Order Theorem Proving will take place in Bern, Switzerland on July 4, 2011, co-locating with Tableaux 2011, The 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods on July 4-8, 2011.

Call for Papers

Scope

The series of FTP workshops focusses on all aspects of theorem proving in first-order logic. It aims to be a forum for the presentation of original work, and for the discussion of work in progress.

Relevant topics for the workshop include (but are not limited to)

• theorem proving in first-order classical, many-valued, and modal logics, including:
  • satisfiability in propositional logic,
  • satisfiability modulo theories,
  • decision procedures,
  • constraint reasoning,
  • equational reasoning,
  • term rewriting,
  • resolution,
  • paramodulation/superposition;
• strategies and complexity of theorem proving procedures;
• applications of first-order theorem proving 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), Liverpool, UK (2007), and Oslo, Norway (2009). For more information about FTP, its scope and previous workshops, please, see the FTP Workshop Series web page.

Paper Submissions

Authors are invited to submit papers in the following categories:

• Extended abstracts of up to 15 pages describing original results, 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:

https://www.easychair.org/conferences/?conf=ftp2011

Submissions will be reviewed by at least two referees, possibly more, and will be evaluated on their significance, technical merit, and relevance to the workshop.

Publication

Accepted submissions will be published as CEUR Workshop Proceedings and will be distribted at the workshop.

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.

Important Dates

Invited Speakers (NEW!)

Programme Committee