The Coq mailing list

[geoff AT cs.miami.edu]

                  C A L L   F O R   P A P E R S

                  Journal of Automated Reasoning

                         Special Issue on 

            Empirically Successful Automated Reasoning


With improving technology, theorem proving and related methods are
successfully being applied to larger problems and used in more domains.
To further disseminate developments and results in this area, a special
issue of the Journal of Automated Reasoning dedicated to empirically
successful automated reasoning will be published.

We invite submission of articles describing work on the implementation
and deployment of working automated reasoning systems and applications.
Both participants of the successful ESCAR-workshop at CADE-20 (see
http://www.cs.miami.edu/~geoff/Conferences/ESCAR/) and other authors
are invited to submit contributions. Submissions should be mature
journal articles.  They may address any aspect of "really working"
systems and applications, and should not focus on theoretical ideas
that have not yet been translated into working software. 

Similar to the ESCAR-workshop, this special issue will have two tracks,
one for systems and one for applications. Suggested topics include, but 
are not limited to:

Systems 
 * Implementation techniques and comparisons 
 * Data structures and algorithms for the efficient representation of
   terms, formulae, search states, etc., e.g. new indexing techniques,
   efficient implemetation of simplification orderings, etc. 
 * Higher level data structures and formats for the representation of
   proof tasks and derivations, proof and lemma storage, etc. 
 * Implemented and evaluated heuristics 

Applications 
 * Descriptions of automated reasoning solutions in application domains 
 * Experience with practical applications 
 * Encoding of domain problems into logic, and decoding of logic
   solutions back into the domain 
 * Special automated reasoning techniques for applications 
 * User interfaces (to entire systems, not just the automated
   reasoning component) 
 * System integration 



Submission format:
==================

Submissions should be written in general terms understandable by the
usual audience of the journal.  They will be fully refereed to usual
journal standards.

Submissions should be formatted according to JAR's author guidelines
(see the link on the home page below), and preferably be written in
LaTeX. A LaTeX style file can be obtained here:

    http://www.springeronline.com/authors/jrnlstylefiles


Dates:
======

Submission ..... December 5, 2005
Notification ... January 20, 2006
Camera ready ... March 6,    2006


Websites and Submission procedure:
==================================

Please send an email with the title, authors' names, and abstract
in plain text, and the full paper in PDF-format as an attachment, 
to the following address by December 5:

    
esar-jar AT eprover.org

Please feel free to send any questions or inquiries to this address
as well.  The website for this special issue, containing more useful
information, is available at

    http://www.eprover.org/EVENTS/ESAR-JAR


Deepak Kapur.
Editor-in-Chief,
Journal of Automated Reasoning
Bernd Fischer, Stephan Schulz, Geoff Sutcliffe.
Guest Editors.