[Prev][Next][Index][Thread]
STRATEGIES 2001 (call for participation, prelim. program)
*********************************************************************
CALL FOR PARTICIPATION AND PRELIMINARY PROGRAM
*********************************************************************
4th International Workshop on Strategies in Automated Deduction
(STRATEGIES 2001)
www: http://www.logic.at/strategies01/
Siena, Italy, June 18, 2001, in connection with IJCAR 2001
BACKGROUND, AIMS AND TOPICS
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.
Topics of interest for the workshop include all aspects related to
strategies in automated deduction. The emphasis of this year's
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.
IMPORTANT DATES
Early registration: May 15, 2001
STRATEGIES 2001: June 18, 2001
IJCAR 2001 workshops: June 18-19, 2001
IJCAR 2001: June 20-23, 2001
REGISTRATION
For details of registration, please see the webpages at
http://www.dii.unisi.it/~ijcar/ and http://www.logic.at/strategies01/.
PRELIMINARY WORKSHOP PROGRAM (June 18, 2001)
8:50- 9:00 Opening
9:00-10:00 Manual Strategies (INVITED TALK)
William McCune
10:00-10:30 Termination of Rewriting with Local Strategies
Olivier Fissore, Isabelle Gnaedig and Helene Kirchner
10:30-11:00 Coffee
11:00-11:30 A Logic for Rewriting Strategies
Richard B. Kieburtz
11:30-11:50 An Algorithm for Guiding Clausal Temporal Resolution
M. Carmen Fernandez Gago, Michael Fisher and Clare Dixon
11:50-12:10 Regular Form of Derivations in Calculi with both
Equality and non-Equality Predicates
Anatoli Degtyarev
12:10-12:30 Goal-Driven Inference Search in Classical
Propositional Logic
Alexander Lyaletski and Andrey Paskevich
12:30-14:00 Lunch
14:00-15:00 Mechanical Software Verification: High Level Control
Aspects from a User's Perspective (INVITED TALK)
Wolfgang Goerigk
15:00-15:30 A Pragmatic Approach to Reuse in Tactical Theorem
Proving
Axel Schairer, Serge Autexier and Dieter Hutter
15:30-16:00 Coffee
16:00-16:30 A Proof-Planning Framework with explicit Abstractions
based on Indexed Formulas
Serge Autexier
16:30-16:50 Continuations of Proof Strategies
Julian Richardson and Alan Smaill
16:50-17:10 Strategies for Interactive Proof and Program Development
in Martin-L"of Type Theory (extended abstract)
Marcin Benke
17:10-18:00 Final discussion
PROGRAM COMMITTEE
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 Löchner, U. Kaiserslautern (Germany)
Christophe Ringeissen, LORIA-INRIA Nancy (France)
FURTHER INFORMATION
http://www.logic.at/strategies01/
*********************************************************************