Alessandro Armando & Silvio Ranise Interactive Development of Provably Sound Decision Procedures . . . . . . . . . . . 1

Simon Anthony & Alan M. Frisch Towards Inductive Constraint Logic Programming . . . . . . . . . . . . . . . . . . . 3

John Bell, Wilfrid Hodges & Graham White The Dynamo Project . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

P. Bellot, J-P. Cottin, A. Demaille, J. Leneutre, E. Zarpas Automated Deduction for Protocols Design . . . . . . . . . . . . . . . . . . . . . . . 7

Alan Bundy Rippling: Greatest Hits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

Andrew Cumming, Helen Lowe, Michael Smyth & Alison Varey Co-operative Theorem Proving for System Development . . . . . . . . . . . . . . . . 12

Carlos Viegas Damásio, Luis Moniz Pereira & Michael Schroeder Bridging the Gap between Theory and Practice: REVISE Progress Report . . . . . 14

Louise Dennis Automating Coinduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

Clare Dixon Implementing Temporal Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

Michael Fisher Clausal Temporal Resolution: Current Work and Future Directions . . . . . . . . . 21

Ian P. Gent Am I Bridging the Gap? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

Andrew Ireland Proof Planning for Imperative Program Proof . . . . . . . . . . . . . . . . . . . . . 25

Robert Johnson Towards Efficient Parallel Temporal Proof . . . . . . . . . . . . . . . . . . . . . . . 27

Manfred Kerber A Call for Standardising Input and Output Formats of Deduction Systems . . . . . 29

Ursula Martin Algebraic Applications of Automated Reasoning Techniques . . . . . . . . . . . . . 31 Fabio Massacci From Sound and Complete to Approximate Deduction . . . . . . . . . . . . . . . . 34 Raul Monroy Proof Planning the Verification of CCS Programs . . . . . . . . . . . . . . . . . . . 36 Chris Preist . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Chris Price . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Marco Roveri & Adolfo Villafiorita Using Abstraction to Prove Theorems in Boolean Algebra . . . . . . . . . . . . . . 40 Andreas Schöter Implementing Stratified Default Reasoning . . . . . . . . . . . . . . . . . . . . . . . 42 André Trudel Implementing Point Based First Order Temporal Logics . . . . . . . . . . . . . . . . 44 Lincoln A. Wallen Bridging the Gap between Theory and Practice: A Different Kind of Theory …. 46 Toby Walsh Statistical Computational Mechanics: Statistical Mechanics Applied to Computation 48