11:00 | Opening Session |
11:15 | C. Benzmuller. The Calculemus Research Training Network. A short overview. |
11:45 | Ferruccio Guidi, C. Sacerdoti Coen. Querying Distributed Digital Libraries of Mathematics |
12:30 | Lunch |
14:00 | Manuel Maarek, Virgile Prevosto. The Documentation System of FoC |
14:45 | Claudio Sacerdoti Coen, Stefano Zacchiroli. Brokers and Web-Services for Automatic Deduction: a Case Study |
15:30 | Coffee |
16:00 | Jacques Carette, William Farmer, Jeremie Wajs. Trustable Communication Between Mathematics Systems |
16:40 | Edmund Clarke, Michael Kohlhase, Joel Ouaknine, Klaus Sutner. System Description: Analytica 2 |
17:00 | Andrew Adams, A New Interface to PVS |
17:20 | Martin Pollet, Volker Sorge. Integrating Computational Properties at the Term Level |
17:40 | CALCULEMUS network meeting |
9:00 | Invited talk: Thierry Coquand
(Chalmers University of Technology, Gteborg, Sweden) (joint speaker with TABLEAUX 2003) Dynamical Method in Algebra: a Survey |
10:00 | Jesus Aransay, Clemens Ballarin, Julio Rubio. Towards a higher reasoning level in formalized Homological Algebra |
10:30 | Coffee |
11:00 | Virgile Prevosto, Mathieu Jaume. Making proofs in a hierarchy of mathematical structures |
11:45 | Sylvie Boldo, Marc Daumas, Laurent Théry. Mixing formal proofs and computer algebra about finite precision arithmetic |
12:30 | Lunch |
14:00 |
OUT-OF-TOWN EXCURSION AND SOCIAL DINNER |
9:00 | Invited talk: James Davenport. University of Bath. Definite/indefinite integration |
10:00 | Ulrich Berger, Monika Seisenberger. Inductive definitions versus classical dependent choice in the Minlog system |
10:30 | Coffee |
11:00 | Silvio Ranise. Building Convex Hulls by Combining SAT Solving and Algebric Computing |
11:20 | Hidetsune Kobayashi, Hideo Suzuki, Hirokazu Murao. Rings and Modules in Isabelle/HOL |
11:40 | Wolfgang Windsteiger. Exploring an Algorithm for Polynomial Interpretation in the Theorema System |
12:30 | Lunch |
14:00 |
PANEL DISCUSSION ON OPEN CHALLENGES OF COMPUTERIZED MATHEMATICS
Panel Introduction: Jacques Calmet. Are there true Grand
Mathematical Challenges in Mechanized Mathematics?Joint with TABLEAUX and TPHOLs 2003 |