| Sunday July 5. | ||
| 14:00 - 14:30 | Albert Brandl, Mandana Eibegger, Hans Hirschberger, Georg Moser | AutoMod: An Integrative Approach to Automated Model Building |
| 14:30 - 15:00 | Frieder Stolzenburg | Loop-Detection in Hyper-Tableaux by Powerful Model Generation |
| 15:00 - 15:30 | Sorin Stratulat | Applying semantic subsumption rules in the context of inductive proofs |
| 15:30 - 16:00 | Break | |
| 16:00 - 16:30 | Thomas Baar, Bernd Fischer, Dirk Fuchs | Experiments with ATP Integration in a Software Engineering Application |
| 16:30 - 17:00 | Ingo Dahn, Andreas Haida, Thomas Honigmann, Christoph Wernhard | Using Mathematica and Automated Theorem Provers to Access a Mathematical Library |
| 17:00 - 17:30 | Uwe Petermann | Integrating Deduction and Computation |
| Monday July 6. | ||
| 09:00 - 09:30 | Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn, Peter Schmitt | Integrating Automated and Interactive Theorem Proving |
| 09:30 - 10:00 | Lawrence C. Paulson | A Generic Tableau Prover and its Integration with Isabelle |
| 10:00 - 10:30 | Gernot Stenz | Proof Transformations for Integrating Automated and Interactive Theorem Provers |
| 10:30 - 11:00 | Break | |
| 11:00 - 11:30 | Alessandro Armando, Piergiorgio Bertoli, Alessandro Coglio, Fausto Giunchiglia, Jose Meseguer, Silvio Ranise, Carolyn Talcott | Open Mechanized Reasoning Systems: a Preliminary Report |
| 11:30 - 12:00 | The Theorema Group | Theorema: An Integrated System for Computation and Deduction in Natural Style |
| 12:00 - 12:30 | Jörg Meyer and Arnd Poetzsch-Heffter | Constructing Verification Environments for Object-oriented Programs |