Special JSC issue on First Order Theorem Proving

[Viorica Sofronie-Stokkermans]

[We apologize if you receive multiple copies of this announcement]

----------------------------------------------------------------
                    CALL FOR PAPERS

            Journal of Symbolic Computation
       Special Issue on First Order Theorem Proving
   http://www.mpi-inf.mpg.de/~sofronie/ftp-special-issue.html
----------------------------------------------------------------
                 Deadline for submissions
                 **** May 1st, 2010 ****
-----------------------------------------------------------------

This special issue is dedicated to the topics of FTP 2009, namely all
aspects of First-Order Theorem Proving as a core theme of Automated
Deduction. We welcome original contributions on various aspects of
first-order theorem proving, including (but not restricted to):
  * theorem proving in first-order classical, many-valued, and
    modal logics, including:
      - satisfiability in propositional logic,
      - satisfiability modulo theories,
      - specialized decision procedures,
      - constraint reasoning,
      - equational reasoning,
      - term rewriting,
      - resolution,
      - paramodulation/superposition;
  * strategies and complexity of theorem proving procedures;
  * implementation techniques;
  * applications of first-order theorem provers to:
      - program verification,
      - model checking,
      - artificial intelligence,
      - mathematics,
      - computational linguistics.

Guest editors:
==============
  Nicolas Peltier (CNRS - LIG, France)
  Viorica Sofronie-Stokkermans (MPI,Saarbruecken, Germany)

Deadline
========
The deadline for submissions is
               **** May 1st, 2010 ****
If you would like to submit a paper and need a deadline
extension please send an e-mail to Viorica Sofronie-Stokkermans
(e-mail: sofronie at mpi-inf.mpg.de) before May 1st, 2010.

Submission procedure
====================

Submission to this special issue is completely open.

We expect original articles (typically 15-30 pages; submission of larger
papers will be evaluated depending on editorial constraints) that present
high-quality contributions that have not been previously published in a
journal and that must not be simultaneously submitted for publication
elsewhere (extended and/or improved versions of conference papers are
acceptable).

* The introduction of the paper MUST explicitly address the following
  questions in succinct and informal manner:
     - What is the problem?
     - Why is the problem important?
     - What has so far been done on the problem?
     - What is the contribution of the paper on the problem?
     - Is the contribution original?     Explain why.
     - Is the contribution non-trivial?  Explain why.

* All the main definitions, theorems and algorithms must be
     illustrated by simple but meaningful examples.

Without these, the paper will not be considered.

Submission to this special issue is via the EasyChair submission system
http://www.easychair.org/conferences/?conf=ftpjsc2010.

Submissions must comply with JSC's author guidelines.
They must be written in English and should be prepared in LaTeX.
The article should preferably be written using Elsevier's document
class "elsarticle". The Elsevier LaTeX style file package (including
detailed instructions for LaTeX preparation) can be obtained from
  http://www.elsevier.com/latex.
It consists of the file: elsarticle.cls, complete user
documentation for the class file, bibliographic style files
in various styles, and template files for a quick start.

An older version of the "Elsevier Article Class (elsart.cls)" with
"JSC add-on style (yjsco.sty)" and "Harvard style references
(elsart-harv.bst)" can be obtained as the package "JSC LaTex"
(that contains all the necessary style files and a template) from
    http://www4.ncsu.edu/~hong/jsc/JSC_LaTex_2007_Mar_12.zip

Contact
=======
For further informations please send an e-mail to
Viorica Sofronie-Stokkermans (e-mail: sofronie at mpi-inf.mpg.de)