Homepage: http://www.logic.at/strategies/
Series of workshops on strategies in automated deductions. The page contains links to systems providing strategies.
From the Call for Papers
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.
CategoryConference