[Date Prev][Date Next] [Chronological] [Thread] [Top]

[mizar] [2nd CFP] STRATEGIES 2002 (fwd)


---------- Forwarded message ----------
Date: Fri, 15 Mar 2002 10:17:46 +0100
From: Thierry Boy de la Tour <Thierry.Boy-de-la-Tour@imag.fr>
To: uitp@dcs.gla.ac.uk, info-hol@jaguar.cs.byu.edu, imps@linus.mitre.org,
     twelf-list@cs.cmu.edu, rewriting@ens-lyon.fr, atp@logic.tuwien.ac.at,
     theorem-provers@ai.mit.edu, theorynt@listserv.nodak.edu,
     nqthm-users@cli.com, acl2@lists.cc.utexas.edu, qed@mcs.anl.gov,
     wollic@di.ufpe.br, aisb@cogs.sussex.ac.uk, appsem@cs.chalmers.se,
     behavior@cs.ucsd.edu, calculemus-ig@dist.unige.it,
     caml-list@pauillac.inria.fr, ccl@ps.uni-sb.de, clp@comp.nus.edu.sg,
     comlab@comlab.ox.ac.uk, complog@cs.nmsu.edu,
     compulog-deduction@cs.bham.ac.uk, constraints-list@cwi.nl,
     coq-club@pauillac.inria.fr, eacsl@dimi.uniud.it,
     fg121@sunjessen46.informatik.tu-muenchen.de, formal-methods@cs.uidaho.edu,
     IFCoLog-all@dfki.de, isabelle-users@cl.cam.ac.uk, lego-club@dcs.ed.ac.uk,
     lics-request@email.mathematik.uni-freiburg.de, logic-ml@logic.jaist.ac.jp,
     logic@math.ufl.edu, logic-list@Helsinki.FI, mizar-forum@mizar.uwb.edu.pl,
     pvs@csl.sri.com, softtech@cs.uu.nl, softverf@nist.gov, stp@dcs.gla.ac.uk,
     theory-logic@cs.cmu.edu, types@cis.upenn.edu
Newsgroups: comp.theory, comp.ai, comp.constraints, comp.lang.prolog,
    sci.logic
Subject: [2nd CFP] STRATEGIES 2002


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


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

             http://www-leibniz.imag.fr/ATINF/strategies02/

                Held in conjunction with CADE at FLoC
                  Copenhagen, Denmark, July 26, 2002


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 CADE-18 at FLoC 2002 in Copenhagen.
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.


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 search plans and prove their properties;
* 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 thereof;
* Control issues and strategies in the integration of systems.


SUBMISSIONS

Authors are invited to submit an extended abstract of up to 10 pages.
Researchers interested in attending the workshop without giving a talk
are invited to send a position paper of 1-2 pages.
All submissions should be sent to the Program Chairs
(mailto:strategies02@cs.uiowa.edu) in Postscript before April 22, 2002.
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 22, 2002
Notification:         May 24, 2002
Final versions:       June 7, 2002
Workshop:             July 26, 2002
CADE:                 July 27-30, 2002
FLoC:                 July 20 - August 1, 2002


ORGANIZATION

Maria Paola Bonacina               University of Iowa (USA)
Thierry Boy de la Tour             IMAG Grenoble (France)


PROGRAM COMMITTEE

Maria Paola Bonacina (co-chair)    University of Iowa (USA)
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)
Dieter Hutter                      DFKI Saarbruecken (Germany)
Reinhold Letz                      Technische Universitaet Muenchen (Germany)


FURTHER INFORMATION

STRATEGIES 2002 website:   http://www-leibniz.imag.fr/ATINF/strategies02/
CADE 2002 website:         http://www.uni-koblenz.de/~cade-18/
FLoC 2002 website:         http://floc02.diku.dk/
STRATEGIES series website: http://www.logic.at/strategies/

*********************************************************************


-- 

   Thierry Boy de la Tour                       INPG - Laboratoire LEIBNIZ
  Phone: (33) 4 76 57 46 68                     46, avenue Felix Viallet
   FAX : (33) 4 76 57 50 81                     38031 GRENOBLE cedex
 e-mail: Thierry.Boy-de-la-Tour@imag.fr         FRANCE
       "Hypocrite lecteur, --- mon semblable, --- mon frere!"