[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] [CFP] STRATEGIES 2002 (fwd)
---------- Forwarded message ----------
Date: Wed, 19 Dec 2001 11:46:02 +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,
objforum@prg.oxford.ac.uk, 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@sun1.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
Subject: [CFP] STRATEGIES 2002
*********************************************************************
************ first 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
(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.
Attendance is by invitation only but late requests for participation
will be considered.
INVITED TALKS
Two or three invited talks are being planned.
IMPORTANT DATES
Submission deadline: April 22, 2002
Notification: June 1, 2002
Final versions: June 26, 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!"