CALCULEMUS 2003
Preliminary Schedule

 

WEDNESDAY, SEPTEMBER 10, 2003

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-14:00

 

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-16:00

 

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

 

 

 

 

 

 

 

 

THURSDAY, SEPTEMBER 11, 2003

9:00 am


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-11:00

 

Coffee

 

11:00

Mathieu Jaume,Virgile Prevosto. 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-14:00

 

Lunch

 

14:00

 

OUT-OF-TOWN EXCURSION
AND SOCIAL DINNER

 

 

 

FRIDAY, SEPTEMBER 12, 2003

c

 

 

 

 

 

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-11:00

 

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-14:00

 

Lunch

 

 

14:00


PANEL DISCUSSION ON OPEN CHALLENGES OF COMPUTERIZED MATHEMATICS
Joint with TABLEAUX  and TPHOLs 2003



Panel Introduction:    Jacques  Calmet, Are there true Grand Mathematical Challenges in Mechanized Mathematics?

 

 

15:30-16:00

 

Coffee

 

 

16:00


PANEL DISCUSSION (continued)

 

17:00