[DL] 1st cfp: Automated Reasoning and Mathematics: Essays in Memory of William McCune

[Maria Paola Bonacina]

                       FIRST CALL FOR PAPERS

               Automated Reasoning and Mathematics:
                Essays in Memory of William McCune

                 Submission Deadline: March 1st, 2012
  <http://profs.sci.univr.it/~bonacina/McCuneBook/McCuneBook.html>


AIM

   This is a book of collected articles presenting research in
   all aspects of automated reasoning and its applications to
   mathematics to honor the memory of William W. (Bill) McCune
   and contribute to preserving his legacy.

   Bill McCune (http://www.cs.unm.edu/~mccune/) had an enormous
   impact on automated reasoning, especially with the development
   of a series of systems of astounding power, robustness, and
   portability, including the theorem provers Otter, EQP, Prover9,
   the parallel prover ROO, the proof checker Ivy, and the model
   builder MACE, preceded by the prototype SAT-solver ANL-DP.

   Bill McCune applied these systems to solve open problems in
   mathematics and logic, culminating with the fully automated
   solution in 1996 of the Robbins problem that had challenged
   mathematicians for over sixty years. This result brought
   unprecedented visibility to the field of automated deduction.
   For all his achievements, Bill McCune received the Herbrand
   Award in the year 2000 (http://www.cadeinc.org/).


SCOPE

   We invite high-quality submissions on the general topic of
   automated reasoning and its applications, especially but not
   exclusively in mathematics, with connections to any of
   Bill McCune's research areas:

   * Automated theorem proving
   * Automated model building and constraint solving
   * Implementation of and practice with automated reasoners
   * Algorithmics for automated reasoners: unification,
     matching, rewriting, indexing
   * Inference control, search plans and semantic guidance
     for automated reasoners
   * Proof checking, proof presentation, proof explanation
   * Application of automated reasoners in mathematics,
     logic, combinatory logic, many-valued logic, algebraic
     structures and their axiomatizations, set theory
   * Applications related to formal methods


PUBLICATION DETAILS

   It is expected that the book will be published in the Festschrift
   subseries of the Springer LNAI/LNCS series.


SUBMISSION INSTRUCTIONS

   While it is expected that most of the papers will be regular
   technical papers, a few papers that combine scientific content
   with recollections of Bill McCune's work and personality,
   as can be written by those who worked with him, are also sought.

   All papers will be refereed by anonymous peer reviewers, and
   read by the editors, according to the highest standards in terms
   of originality, significance, technical quality, and readability.

   Submissions must be in English and standard conforming pdf
   format. They must be unpublished and not submitted for
   publication elsewhere. However, significantly extended versions
   of papers published at conferences are welcome. Submissions
   of any length will be considered, but final versions may be
   limited by the editors depending on the totality of submissions.
   Authors are strongly encouraged to produce their papers in LaTeX.

   Detailed instructions for electronic submission via EasyChair
   will be published at the book website. Formatting
   instructions and the LNCS style files can be obtained via
   http://www.springer.de/comp/lncs/authors.html.


SUBMISSION DEADLINE: March 1st, 2012

   In order to facilitate the planning of the book, authors are
   invited to notify the editors as soon as possible of their
   intention to submit with proposed topic and length. Early
   submission would be especially helpful for completing the
   review process sooner.


EDITORS

   Maria Paola Bonacina   Universita` degli Studi di Verona
   Mark E. Stickel        SRI International