[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] FTP'07 Special Issue CFP


find enclosed the CFP for a special issue of the AMAI journal
after the FTP'07 workshop.

Apologies for multiple copies.

Best regards,

                            CALL FOR PAPERS

                         Special issue of the
                      FIRST-ORDER THEOREM PROVING                       


First-order theorem proving is one of the core themes of Automated
Deduction and one of its most mature subfields. First-order logic is
sufficiently expressive to allow the specification of a wide range of
problems in a natural way.  At the same time an extensive variety of
sound and complete calculi for first-order logic exists which have
been implemented in a number of high-quality, fully automated
reasoning systems.  These in turn make it not only possible to
effectively solve problems formulated in first-order logic, but also
make it attractive to consider closely related logics, for example,
many-valued, description and modal logics, from a first-order

This special issue is intended to present recent advances in the field
to an audience of applied logicians, automated deduction theorists and
applications specialists.


This special issue will focus on First-order Theorem Proving as a core
theme of Automated Deduction, including:
 *  theorem proving in first-order classical, many-valued,
    description, and modal logics, including:
    - constraint reasoning,
    - decision procedures,
    - equational reasoning,
    - model construction
    - paramodulation/superposition,
    - resolution,
    - satisfiability modulo theories,
    - tableaux,
    - term rewriting,
    - unification;
 * strategies and complexity of theorem proving procedures;
 * applications of first-order theorem proving to:
   - program verification,
   - model checking,
   - artificial intelligence,
   - mathematics,
   - computational linguistics.


This special issue welcomes original high-quality contributions that
have been neither published in nor submitted to any journals or
refereed conferences. 

Authors of papers presented at FTP 2007 are welcome to submit extended
and revised versions of their papers. However, contributions are not
limited to those based on papers presented at FTP 2007; other
submission are welcome as well. All submissions will be refereed to
usual journal standards. 

Submissions should be formatted according to the Instructions for AMAI
submissions <http://www.springeronline.com/journal/10472/submission/>
and authors are encouraged to use the AMAI LaTeX style files for
preparing their submission. Preferably, submissions should be between
20 and 40 pages long.  

Submissions should be made via Easychair at the following address:



Paper submission:            May 28, 2008
Notification of acceptance:  August 4, 2008
Final versions due:          September 4, 2008

* Silvio Ranise   (LORIA and INRIA-Lorraine, France)
* Ullrich Hustadt (University of Liverpool, UK)

The scope of Annals of Mathematics and Artificial Intelligence is
intended to represent a wide range of topics of concern to scholars
applying quantitative, combinatorial, logical, algebraic and
algorithmic methods to Artificial Intelligence areas as diverse as
decision support, automated deduction, reasoning, knowledge-based
systems, machine learning, computer vision, robotics and planning. 
It is hoped to influence the spawning of new areas of applied
mathematics and the strenghtening of the scientific underpinnings of
Artificial Intelligence.