Rome Meeting of the Math-Assistant Project

March 16 - 19
Universita degli Studi di Roma Tre, Rome, Italy

This programme is very provisional, and will evolve in the next days. Please send me the abstracts to your talks.

14:00-14:45 Session 1: Opening (Chair: ??)
- 14:00 Alfonso Miola: Welcome and what we expect from the meeting
- 14:15 Jacques Calmet and Jörg Siekmann: Visionary statements on what Mathematical Assistants are all about
  Views of Computer Algebra / New Trends in Automated Theorem Proving
- 14:30 Karsten Homann and Michael Kohlhase: Status of the TMR Network application
- 14:50 Discussion
15:10 coffee break
15:30-16:40Session 2: Presentation of the hosting Group (Chair: ??)
- 15:30 Alfonso Miola:Who is who (and what he/she is doing)
- 15:40 G. Cioni:An Approach to Class Reasoning in Symbolic Computation
- 16:00 W. Gehrke:Exploiting SML for Experimenting with Algebraic Algorithms
- 16:20 M. Temperini:Enhanced Strict Inheritance
16:40-18:40Session 3: Formalization of Mathematics (Chair: ??)
- 16:40 Andrzej Trybulec: The Mizar Language. Selected Topics.
- 17:40 Erik Barendsen:Formalizing equational reasoning in proof systems based on type theory
- 18:10 Hugo Elbers: Construction of short formal proofs of primality
20:30 Dinner

9.00 to 11.00 Session 4 Plan-Based Theorem Proving (Chair: ??)
- 9.00 to 10:00 Michael Kohlhase and Jörg Siekmann: OMEGA: Towards a mathematical assistant
- 9.00 to 10:00 Helen Lowe: Co-operative Theorem Proving
11:00-11:30 coffee break
11:30 to 12.30 Session 5 Theorem Proving with Abstraction (Chair: ??)
- 11:30 to 12.30 Fausto Giunchiglia: Activities in interactive theorem proving in the Mechanized Reasoning Group
12:30 - 14:00 Lunch break
14.00 to 16.00 Session 6 Computer Algebra I (Chair: ??)
- 14:00 to 15.00 Bruno Buchberger: Overview on the Apply Math Project at RISC
- 15:00 to 16.00 Dongming Wang: Clifford Algebra, Non-commutative Gröbner Bases and Geometry Theorem Proving
16:00 - 16:30 coffee break
16:30 to 18.30 Session 7 Computer Algebra II (Chair: ??)
- 16:30 to 17.30 Jacques Calmet and Karsten Homann: Environments for Doing Mathematics by Cooperative Problem Solving
- 17:30 to 18.30 Alfredo Ferro: ETNA: a proof checker based on computable set theory techniques
20:30 Dinner

9.00 to 10.00 Session 8 Remaining Talks (Chair: ??)
- 9:00 to 10.00 Laurent Thery and Loic Pottier:Research Activities at INRIA Sophia Antipolis
10:00 - 10:30 coffee break
10:30-13:00 Session 9: Discussion (Chair: ??)
- General Discussion
- How can we refine the next application for the EU TMR programme
13:00 Lunch
Afternoon: Voyage home.

Last updated March 13. (Michael Kohlhase)