[om-a] STRATEGIES'04 -- 1st CFP

[Thierry Boy de la Tour]

*********************************************************************
************ first  call for papers and participation  **************
************   (with apologies for multiple copies)    **************
*********************************************************************


   5th International Workshop on Strategies in Automated Deduction
                         (STRATEGIES 2004)

          http://www-leibniz.imag.fr/~boydelat/Strategies04/

                    Held in conjunction with IJCAR
                     Cork, Ireland, July 4, 2004


BACKGROUND AND AIMS

Strategies are almost ubiquitous in automated deduction and reasoning
systems, because the rules at the heart of such systems are non-deterministic,
and need to be complemented by strategies, or search plans, responsible for
controlling them. The role that search plans play in making the resulting
procedures capable of solving efficiently interesting problems is no less
than that played by the inference systems themselves, since typical
deduction paradigms (e.g., generation of consequences, subgoal-reduction,
generation of instances, case analysis, enumeration) generate very large or
infinite spaces of choices.
These considerations apply to both fully automated systems (theorem provers,
model builders, rewriting engines, decision procedures) and interactive
ones (proof assistants and verification systems), and impact them at all
levels, from abstract definition to design and implementation.
The combination of automated components (e.g., theorem provers and
decision procedures) as well as their integration within interactive
systems to generate the reasoning environments of the future poses new
control problems and puts the study of strategies at the forefront.


HISTORY AND VENUE

Following the tradition of the STRATEGIES workshops held at CADE-14 (1997),
CADE-15 (1998), FLoC 1999 and IJCAR 2001, the fifth workshop in the
series will be held before IJCAR 2004 in Cork, Ireland.
Full versions of selected papers from the 1999 workshop appeared as volume
29 of the Annals of Mathematics and Artificial Intelligence (February 2001),
and selected papers from the 2001 workshop appeared as Volume 58 Issue 2 of
Electronic Notes in Theoretical Computer Science (October 2001).


TOPICS OF INTEREST

The workshop on Strategies in Automated Deduction is the primary forum
for the communication of new results on control strategies and search plans
in automated theorem proving, automated model building, decision procedures,
interactive proof assistants, proof planners, and logical frameworks,
in first-order (including propositional and purely equational as special
cases), modal (e.g., temporal) and higher-order logics.

Sample topics include:

Theory:
* Models of search spaces and languages or mathematical formalisms
   to define strategies and prove properties about them, including
   machine-independent evaluation and comparison of strategies;
* Analysis of the search space (e.g., regularities, symmetries,
   classification, stratification);
* Strategy analysis (e.g., formal approaches for the machine-independent
   evaluation and comparison of deduction strategies);

Definition, design, implementation and application:
* Meta-level features (e.g., pre-processing, compilation, lemmatization,
   caching, usage of semantics or domain knowledge);
* Strategies in (existing) systems (e.g., implementation of the proof
   search model, flexibility and programmability of strategies,
   role of the user);
* Applications and case studies in which strategies play a major role.

Specialization and integration:
* Strategies devoted to specific theories including inductive theories,
   arithmetic, decidable theories, and combinations of theories;
* Control issues and strategies in the integration of systems.


SUBMISSIONS

Researchers are invited to submit an extended abstract of up to 10 pages
or to send a position paper of 1-2 pages.
Authors of accepted extended abstracts will be invited
to present their work at the workshop. Authors of position papers
will be invited to participate, and may be invited to give shorter talks
if time allows it.
All submissions should be sent to the Program Chairs
(strategies04 at imag.fr) in Postscript before April 19, 2004.
Accepted contributions will be included in the workshop proceedings
which will be available at the workshop and on the WWW.

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


INVITED TALKS

Two or three invited talks are being planned.


IMPORTANT DATES

Submission deadline:  April 19, 2004
Notification:         May 21, 2004
Final versions:       June 4, 2004
Workshop:             July 4, 2004
IJCAR:                July 6 - July 8, 2004


ORGANIZATION

Maria Paola Bonacina         Universita` degli Studi di Verona (Italia)
Thierry Boy de la Tour       IMAG Grenoble (France)


PROGRAM COMMITTEE

Myla Archer                        Naval Research Laboratory (USA)
Maria Paola Bonacina (co-chair)    Universita di Verona (Italia)
Thierry Boy de la Tour (co-chair)  IMAG Grenoble (France)
Amy Felty                          University of Ottawa (Canada)
Ruben Gamboa                       University of Wyoming (USA)
Andreas Herzig                     IRIT Toulouse (France)
Aaron Stump                        Washington University in St. Louis (USA)
Armando Tacchella                  Universita di Genova (Italia)


FURTHER INFORMATION

STRATEGIES 2004 website:   http://www-leibniz.imag.fr/~boydelat/Strategies04/
IJCAR 2004 website:        http://4c.ucc.ie/ijcar/
STRATEGIES series website: http://www.logic.at/strategies/

*********************************************************************
--
om-announce at openmath.org  -  public announcements concerning OpenMath
Post discussion to om at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-announce-owner at openmath.org for assistance with any problems