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