| Session 1 | Welcome and Invited Talk | Chair: Alessandro Armando |
|---|---|---|
| 8:45 - 9:00 | Welcome and techicalities | The Organizers |
| 9:00 - 10:00 | Teaching Mathematics across the Internet | Gaston Gonnet |
| 10:00 - 10:30 | Coffee Break | |
| Session 2 | Protocols and Combination of Systems | Chair: Gaston Gonnet? |
| 10:30-11:00 | Communication Protocols for Mathematical Services based on KQML and OMRS | Alessandro Armando, Michael Kohlhase, Silvio Ranise |
| 11:00-11:30 | Interfacing Computer Algebra and Deduction Systems via the Logic Broker Architecture | Alessandro Armando, Daniele Zini |
| 11:30-12:00 | O-ANTS -- An open aproach at combining Interactive and Automated Theorem Proving | Christoph Benzmüller and Volker Sorge |
| 12:00 - 14:00 | Lunch | |
| Session 3 | Formalization | Chair: Tudor Jebelean |
| 14:00 - 14:30 | Developement of the Theory of Continuous Lattices in Mizar | Grzegorz Bancerek |
| 14:30 - 15:00 | Defining Power Series and Polynomials in Mizar | Piotr Rudnicki, Christoph Schwarzweller, and Andrzej Trybulec |
| 15:00 - 15:30 | On the EA-style integrated processing of self-contained mathematical texts | Anatoli Degtyarev, Alexander Lyaletski, Marina Morokhovets |
| 15:30-16:00 | Panel Discussion | |
| 16:00 - 16:30 | Coffee Break | |
| Session 4 | Computer Algebra with Theorem Provers | Chair: Alan Bundy |
| 16:30 - 17:00 | Logic and dependent types in the Aldor Computer Algebra System | Simon Thompson |
| 17:00 - 17:30 | Definite Integration of Parametric Rational Functions | A. A. Adams |
| 17:30 - 18:30 | Business Meeting | |
| 20:00 -- | Conference Dinner |
| Session 5 | Invited talk (joint with ISSAC) | |
|---|---|---|
| 9:00 - 10:00 | Representing and handling mathematical concepts by humans and machines | Henk Barendregt, Arjeh M. Cohen |
| 10:00 - 10:30 | Coffee Break | |
| Session 6 | Theorem Proving with CAS 1 | Chair: Steve Linton? |
| 10:30 - 11:00 | The THEOREMA Project: A Progress Report | B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, W. Windsteiger |
| 11:00 - 11:30 | Exploring Properties of Residue Classes | Andreas Meier, Volker Sorge |
| 11:30 - 12:00 | Towards Learning New Methods in Proof Planning | Mateja Jamnik, Manfred Kerber, Christoph Benzmueller |
| Session 7 | Systems | Chair: Andrew Adams |
| 12:00 - 12:15 | System Description: SINGULAR - A Computer Algebra System for Polynomial Computation | G.-MM. Greuel, G. Pfister, Hans Schoenemann |
| 12:15 - 12:35 | demo announcements | |
| 12:35 - 14:00 | Lunch | |
| Session 8 | Theorem Proving with CAS 2 | Chair: Manfred Kerber |
| 14:00 - 14:30 | How to find symmetries hidden in combinatorial problems | Noriko Arai, Ryuji Masukawa |
| 14:30 - 15:00 | Using Meta-variables for Natural Deduction in Theorema | Boris Konev, Tudor Jebelean |
| 15:00 - 15:30 | How to formally and efficiently prove Prime(2999) | Olga Caprotti, Martijn Oostdijk |
| 15:30 - 16:00 | Coffee Break | |
| Session 9 | Posters and Demos | Chair: Olga Caprotti |
| 16:00 - 17:00 | Short talks introducing the posters and Demos (3-4 minutes each) | 17:00 - 18:30 | Poster Presentations and System Demos |