| 10:30 - 11:00 | Refreshments and Registration |
| 11:00 - 11:15 | Opening Remarks |
| 11:15 - 12:30 | Invited Talk |
| Natarajan Shankar (SRI International) | |
| "Explaining Decision Procedures" Abstract | |
| 12:30 - 14:00 | Lunch |
| 14:00 - 15:30 | Paper Presentations |
| Luís Cruz-Filipe (Instituto Superior Téchnico) and Pierre Letouzey (LMU Munich) | |
| "A Large-Scale Experiment in Executing Extracted Programs" | |
| Martin Pollet (Univ. Saarland) and Volker Sorge (Univ. Birmingham) | |
| "Connecting Logical Representations and Efficient Computations" | |
| Jörn Ossowski and Christel Baier (Univ. Bonn) | |
| "Symbolic Reasoning with Weighted and Normalized Decision Diagrams" | |
| 15:30 - 16:00 | Break |
| 16:00 - 17:30 | Discussion session |
| 9:15-10:30 | Invited Talk |
| Renaud Rioboo (Université Pierre et Marie Curie) | |
| "Concrete Mathematics with the FoCaL Environment" Abstract | |
| 10:30 - 11:00 | Break |
| 11:00 - 12:30 | Paper Presentations |
| Ruth Anne Hardy (Univ. St. Andrews) | |
| "Interactions between PVS and Maple in Symbolic Analysis of Control Systems" | |
| Tobias Schmidt-Samoa (Tech. Univ. Kaiserslautern) | |
| "An Even Closer Integration of Linear Arithmetic into Inductive Theorem Proving" | |
| David Delahaye (CNAM) and Micaela Mayero (Univ. Paris Nord) | |
| "Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System" | |
| 12:30 - 14:00 | Lunch |
| 14:00 - 15:30 | Paper Presentations |
| Aurélie Hurault and Marc Pantel (IRIT) | |
| "Mathematical Service Trading Based on Equational Matching" | |
| Geoff W. Hamilton (Dublin City Univ.) | |
| "Poitín: Distilling Theorems From Conjectures" | |
| Roy L. McCasland (Univ. of Edinburgh), Alan Bundy (Univ. of Edinburgh), and Patrick F. Smith (Univ. of Glasgow) | |
| "Ascertaining Mathematical Theorems" | |
| 15:30 - 16:00 | Break |
| 16:00 - 16:30 | Paper Presentation |
| Louise A. Dennis (Univ. Nottingham), Mateja Jamnik (Univ. Cambridge), and Martin Pollet (Univ. Saarland) | |
| "On the Comparison of Proof Planning Systems LambdaClam, Omega and IsaPlanner" | |
| 16:00 - 17:30 | Closing and Business meeting |