Preface Volume 58, Issue 2

AbstractThis issue contains revised versions of selected papers presented at the 4th International Workshop on Strategies in Automated Deduction (STRATEGIES 2001). The workshop was held in conjunction with the (first) International Joint Conference on Automated Reasoning (IJCAR 2001) in Siena, Italy, on June 18, 2001. More information on the workshop series and its subject is available here.Strategies are almost ubiquitous in automated deduction and reasoning systems, because the inference rules at the heart of such systems are typically non-deterministic in nature, and need to be complemented by another component, usually called strategy or search plan, which is responsible for the control of the inference rules. For instance, in fully automated theorem proving, the search plan selects the inference rule and the premises for the next step in the derivation, which involves prioritizing inferences rules (e.g., contraction-first search plans), heuristics to sort the database of existing formulae or to sort open subgoals, and criteria, also typically heuristic in nature, to prune the search space. Similar considerations apply to decision procedures, model building methods, rewriting engines, where the rewriting strategy selects redex and rule for the next step, and, at a higher level of abstraction, logical frameworks. In interactive systems, tactics define conditions for the application of inference rules, and in turn tacticals may control the application of tactics; it is still the control component of the proof assistant that is responsible for requesting the user to instantiate variables, or select lemmas.Not only strategies are necessary to turn a non-deterministic inference system into a mechanical procedure, but the role they play in making the procedure efficient, and capable of solving interesting problems, is no less than that played by the inference system itself. This is because most deduction paradigms (generation of consequences, subgoal-reduction, generation of instances, case analysis, enumeration) generate a very large space of choices, so that sophisticated strategies are essential to implement them efficiently.Nevertheless, only recently strategies have been studied in their own right in automated deduction. The series of workshops on “Strategies in Automated Deduction,” or STRATEGIES for short, 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 are all aspects related to strategies in automated deduction, including: •theory and analysis of strategies (e.g., formal approaches to the abstract representation and comparison of strategies and their behavior, terminological foundations);•strategies in (existing) theorem proving systems (e.g., implementation of the proof search model, integration of strategies into this model, flexibility, programmability, transparency, role of the user);•meta-level features (e.g., pre-processing, compilation, lemmatization, caching, usage of semantics or domain knowledge);•strategy languages (e.g., adequacy for certain purposes, theoretical foundations, practical usefulness, comparison with other approaches, applications);•specialized strategies (e.g., for specific theories including inductive, arithmetic, decidable theories, and their combinations); and•applications and case studies in which strategies play a major rolein automated theorem provers, automated model builders, 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.Based on the careful refereeing process for STRATEGIES 2001, the following papers were selected for this issue: •Mechanical Software Verification: High Level Control Aspects from a User's Perspective by Wolfgang Goerigk•A Logic for Rewriting Strategies by Richard B. Kieburtz•Termination of Rewriting with Local Strategies by Olivier Fissore, Isabelle Gnaedig and Hélène Kirchner•A Proof-Planning Framework with Explicit Abstractions Based on Indexed Formulas by Serge Autexier•A Pragmatic Approach to Reuse in Tactical Theorem Proving by Axel Schairer, Serge Autexier and Dieter HutterThe program committee of STRATEGIES 2001 consisted of Alessandro ArmandoU. Genova (Italy)Maria Paola Bonacina (co-chair)U. Iowa (USA)Gilles DowekINRIA (France) & ICASE/NASA-Langley (USA)Ruben GamboaAnythingOvernight.com, Inc., Texas (USA)Bernhard Gramlich (co-chair)TU Wien (Austria)Bernd LöchnerU. Kaiserslautern (Germany)Christophe RingeissenLORIA-INRIA Nancy (France)Regarding the refereeing process we are very grateful to the program committee and to the additional external referees. Furthermore we would like to thank Michael Mislove, Managing Editor of the ENTCS series, for his technical assistance with using the ENTCS format.November 15, 2001 Maria Paola Bonacina and Bernhard Gramlic