Strategies In Automated Deduction

Series of workshops on strategies in automated deductions. The page contains links to systems providing strategies.

• Copenhagen 2002: http://www-leibniz.imag.fr/ATINF/strategies02/

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.