4th International Workshop on Strategies in Automated Deduction (STRATEGIES 2001)

held in conjunction with IJCAR 2001

in Siena, Italy, June 18, 2001




Program

08:50 - 09:00 Opening
09:00 - 10:30 Session 1
09:00 - 10:00 Mechanical Software Verification: High Level Control Aspects from a User's Perspective (INVITED TALK) [abstract, ps]
Wolfgang Goerigk
10:00 - 10:30 A Logic for Rewriting Strategies [abstract, ps]
Richard B. Kieburtz
10:30 - 11:00 Coffee break
11:00 - 12:30 Session 2
11:00 - 11:30 Termination of Rewriting with Local Strategies [abstract, ps]
Olivier Fissore, Isabelle Gnaedig and Hélène Kirchner
11:30 - 12:00 An Algorithm for Guiding Clausal Temporal Resolution [abstract, ps]
M. Carmen Fernandez Gago, Michael Fisher and Clare Dixon
12:00 - 12:30 Goal-Driven Inference Search in Classical Propositional Logic [abstract, ps]
Alexander Lyaletski and Andrey Paskevich
12:30 - 14:00 Lunch break
14:00 - 15:30 Session 3
14:00 - 14:30 A Pragmatic Approach to Reuse in Tactical Theorem Proving [abstract, ps]
Axel Schairer, Serge Autexier and Dieter Hutter
14:30 - 15:00 A Proof-Planning Framework with Explicit Abstractions Based on Indexed Formulas [abstract, ps]
Serge Autexier
15:00 - 15:30 Continuations of Proof Strategies [abstract, ps]
Julian Richardson and Alan Smaill
15:30 - 16:00 Coffee break
16:00 - 17:30 Session 4
16:00 - 16:30 Strategies for Interactive Proof and Program Development in Martin-Löf Type Theory (Extended Abstract) [abstract, ps]
Marcin Benke
16:30 - 17:30 Final Discussion