Logic List Mailing Archive

First-Order Theorem Proving (FTP 07)

12-13 September 2007
Liverpool, U.K.

FTP'07 - Last call for papers


        International Workshop on First-Order Theorem Proving
        (September 12-13, 2007, Liverpool, United Kingdom)
                  http://www.csc.liv.ac.uk/~ftp07/

The Sixth International Workshop on First-Order Theorem Proving will take
place at the University of Liverpool, UK, on September 12-13, 2007,
co-locating with the Sixth International Symposium on Frontiers of Combining
Systems on September 10-12, 2007.

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); as part
of IJCAR in Siena, Italy (2001); Valencia, Spain (2003); as part of
IJCAR in Cork, Ireland (2004); and Koblenz, Germany (2005).  For more
information about FTP, its scope and previous workshops, please, see

                    http://www.csc.liv.ac.uk/FTP-WS/

Paper Submissions
------------------
   Authors are invited to submit papers in the following three
   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.

   * [NEW] 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/FTP07/

   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 a technical report of the
   University of Liverpool and will be distribted 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.

Important Dates
----------------
Paper submission deadline (all categories):  June  29, 2007
Notification of acceptance/rejection:        July  23, 2007
Final version due:                           August 3, 2007
Workshop:                             September 12-13, 2007

Invited Speakers
-----------------
Aspects of First-order Reasoning in the KeY system
Martin Giese                 (Linz, Austria)

Applying FTPs in Formal Software Safety Certification
Bernd Fischer                (Southampton, England, UK)

Hierarchical and modular reasoning in complex theories: the case of
local theory extensions
Viorica-Sofronie Stokkermans (Saarbruecken, Germany) [joint with FroCos]

Program Committee
------------------
Peter Baumgartner      (Canberra, Australia)
Bernhard Beckert       (Koblenz, Germany)
Reiner Haehnle         (Chalmers, Sweeden)
Ullrich Hustadt        (Liverpool, England, UK)
Alexander Leitsch      (Vienna, Austria)
William McCune         (Albuquerque, New Mexico, USA)
Hans de Nivelle        (Wroclaw, Poland)
Nicolas Peltier        (Grenoble, France)
David A. Plaisted      (Chapell Hill, USA)
Silvio Ranise          (Nancy, France) [Chair]
Christophe Ringeissen  (Nancy, France)
Albert Rubio           (Barcelona, Spain)
Luca Vigano            (Verona, Italy)
Jian Zhang             (Beijing, China)


Local Organization Chair
-------------------------
   U. Hustadt (Liverpool, England, UK)

Conference Venue
-----------------
   The workshop will take place in at the Universtiy of Liverpool on
   September 12 and 13, 2006.  It will be collocated with the 6th
   International Symposium on Frontiers of Combining Systems
   (FroCos'07) which will take place prior to FTP'07.

Further information
--------------------
   For regular updates about the workshop organization, please, visit
   the FTP'07 web page:

                 http://www.csc.liv.ac.uk/~ftp07/

   For contacting the PC chair, please, send an email to
   Silvio.Ranise[AT]loria.fr (substitute [AT] with "@").