9:00- 9:45  Invited Talk A Tale of Two Logics, Three Systems, Four Languages, and Fifteen Years Peter F. Patel-Schneider
9:45-10:30 Invited Talk Alessandro Cimatti
10:30-11:00 Coffee
11:00-11:20 Designing an efficient library for propositional reasoning and beyond E. Giunchiglia,  M. Narizzano, A. Tacchella, M. Vardi
11:20-11:40 A Subsumption-Aided Caching Technique Jens Happe
11:40-12:00 Combining Tableaux and Algebraic Decision Procedures for Dealing with Qualified Number Restrictions in Description Logics Volker Haarslev, Martina Timmann, Ralf Moeller
12:00-12:20 Temporal Logic Theorem Proving and its Application to the Feature Interaction Problem Amy Felty
12:20-12:40 Tactical Theorem proving in First order Temporal Logics Claudio Castellini, Alan Smaill
12:30-14:00  Lunch
14:00-14:45 Invited Talk Evaluating General Purpose Automated Theorem Proving Systems Geoff Sutcliffe
14:45-15:30  Invited Talk Gila Kamhi
15:30-16:00 Coffee
16:00-16:20 The Random Modal QBF Test Set Juan Heguiabehere and Maarten de Rijke
16:20-16:40 Improving the Generation of Random Modal Formulae for testing decision procedures Peter Patel-Schneider, Roberto Sebastiani
16:40-17:00 Formulae which Highlight differences between Temporal Logic and Dynamic Logic Provers Ullrich Hustadt, Renate Schmidt
17:00-17:20  Generating Symbolic Model Checking benchmarks by reduction from QBF F. Donini, P. Liberatore, F. Massacci, M. Schaerf
17:20-18:00  Open Discussion Initiators: E. Giunchiglia, F. Massacci