cfp Strategies 2001


The Strategies workshop welcomes contributions on search strategies,
search plans, and all control issues -- broadly meant -- that arise
in the design/development/application of automated reasoning systems,
meaning theorem provers of all kinds (fully automated and interactive,
first-order and higher-order) as well as model builders, and systems
that integrate such functionalities.
While the area of automated reasoning, and also the area of logic in
computer science at large, has given traditionally first-class status
to the inference rules and their properties (e.g., completeness),
the Strategies workshop aims at giving equal weight to the control
component and its properties (e.g., fairness, search complexity).
Accordingly, search plans and such are viewed as subject of investigation
in their own right (e.g., how to define them as mathematical objects,
how to measure their search complexity), not only as a fundamental
ingredient in the conception of provers.
************ first  call for papers and participation  **************
************   (with apologies for multiple copies)    **************

  4th International Workshop on Strategies in Automated Deduction
                         (STRATEGIES 2001)

                www: http://www.logic.at/strategies01/

                 held in conjunction with IJCAR 2001

                 in Siena, Italy, June 18 or 19, 2001


Strategies are almost ubiquitous in automated deduction and reasoning  
systems, yet only recently have they been studied in their own
right. The workshop aims at making progress towards a deeper
understanding of the nature of strategies and search plans, their
description, properties, and usage, especially, but not exclusively,
in theorem proving and model building. It provides a common forum for
researchers working on all aspects of strategies, under different
terminologies and in various domains. The workshop continues and
focuses the efforts of three previous workshops held in conjunction
with CADE-14 (1997), CADE-15 (1998), and FLoC'99, as well as of a
special issue of the Annals of Mathematics and Artificial Intelligence
on Strategies in Automated Deduction that is currently in print. 

In view of the increasing importance of strategies in complex
automated reasoning systems, we would like to offer again this forum
at IJCAR 2001, for an active exchange of ideas among researchers, and
the presentation of recent work on and progress in strategy-related
topics. IJCAR 2001 will provide an ideal context to achieve further
progress and stimulate discussion in the field. We expect that the
broad scientific scope of IJCAR (replacing CADE, FTP and TABLEAUX)
will have synergetic effects for the workshop. 


Topics of interest for the workshop include all aspects related to
strategies in automated deduction. The emphasis of the next 
workshop will be on 

- theory and analysis of strategies (e.g., formal approaches for
  abstract representation and comparison of theorem proving strategies
  and their behavior, terminological foundations),
- strategies in (existing) theorem proving systems (e.g.,
  representation and implementation of the proof search model, 
  integration of strategies into this model, flexibility,
  programmability, transparency, role of the user),  
- strategy languages (e.g., adequacy for certain purposes, theoretical
  foundations, practical usefulness, comparison with other approaches,
  applications), and 
- applications and case studies in which strategies play a major role. 


Authors interested in presenting their work related to strategies are
invited to submit an extended abstract of up to 10 pages. Researchers
interested in attending the workshop without giving a talk may send a
position paper of 1-2 pages describing their interest in the mentioned
topics. All submissions should be sent to the Program Chairs
(strategies01@logic.at) in postscript before March 31, 2001. Accepted
contributions will be included in the workshop proceedings which will
be available at the workshop and also on the www.  

Based on the submissions, the Program Chairs will consider the
possibility of a formal publication (e.g., a special issue of a
journal or a volume in a series of electronic proceedings) following
the meeting in Siena, where authors may submit full versions of the
papers presented at the workshop. This will involve another call for
papers and a separate refereeing process. 

In order to keep the workshop reasonable in size, attendance is by
invitation only. However, depending on the number of expected active
participants, we will also consider late requests for participation.  


Wolfgang Goerigk (U. Kiel, Germany): 
  Mechanical Software Verification: High Level Control Aspects from 
  a User's Perspective

William McCune (Argonne National Lab., USA):
  Manual Strategies


Submission deadline:  March 31, 2001
Notification:         April 30, 2001
Final versions:       May 20, 2001
Workshop:             June 18 or 19, 2001
IJCAR 2001:           June 18-23, 2001


Maria Paola Bonacina               U. Iowa (USA)
Bernhard Gramlich                  TU Wien (Austria)


Alessandro Armando                 U. Genova (Italy)
Maria Paola Bonacina (co-chair)    U. Iowa (USA)
Gilles Dowek                       INRIA (France) & ICASE/NASA-Langley (USA)
Ruben Gamboa                       AnythingOvernight.com, Inc., Texas (USA)
Bernhard Gramlich (co-chair)       TU Wien (Austria)
Bernd Loechner                     U. Kaiserslautern (Germany)
Christophe Ringeissen              LORIA-INRIA Nancy (France)


STRATEGIES 2001 website: http://www.logic.at/strategies01/
IJCAR 2001 website:      http://www.dii.unisi.it/~ijcar/
Strategies in Automated Deduction general website: