Sunday, May 25th
|
|
Session 1, Chair: Bruno Buchberger |
| 13:00 - 13:10 |
Bruno Buchberger |
Opening |
| 13:10 - 13:30 |
Jörg Siekmann |
Systemintegration for Computer-based Mathematics |
| 13:30 - 14:00 |
Christoph Benzmüller |
The Omega System |
| 14:00 - 14:30 |
Martin Pollet & Quoc Vo Bao |
Proof Planning in Omega |
| 14:30 - 15:00 |
Serge Autexier |
Hierarchical contextual reasoning |
|
Session 2, Chair: Tudor Jebelean |
| 15:30 - 16:00 |
Dieter Hutter |
Management of Change |
| 16:00 - 16:30 |
Axel Schairer |
Transformational approach to management of change |
|
Monday, May 26th
|
|
Session 3, Chair: Wolfgang Windsteiger |
| 9:30 - 10:00 |
Claus-Peter Wirth |
Inductive Theorem Proving |
| 10:00 - 10:30 |
Armin Fiedler |
Tutorial Dialogue with a Mathematical Assistant System |
|
Session 4, Chair: Temur Kutsia |
| 11:00 - 11:30 |
Helmut Horacek |
Proof Presentation in Omega |
| 11:30 - 12:00 |
Erica Melis |
Activemath: A math learning system |
|
Session 5, Chair: Jörg Siekmann |
| 14:00 - 14:20 |
Bruno Buchberger |
Objectives and Design of Theorema |
| 14:50 - 15:20 |
Florina Piroi & Koji Nakagawa |
Aspects of Proof Presentation (slides Piroi, slides Nakagawa) |
| 14:50 - 15:20 |
Tudor Jebelean |
The S-Decomposition Method for Predicate Logic |
|
Session 6, Chair: Christoph Benzmüller |
| 15:50 - 16:20 |
Wolfgang Windsteiger |
The Theorema Set Theory Prover |
| 16:20 - 16:50 |
Temur Kutsia |
Equational Logic Including Sequence Variables |
| 16:50 - 17:20 |
Markus Rosenkranz |
Equation Solving for Operator Domains (extended abstract for ISSAC) |
|
Tuesday, May 27th
|
|
Session 7, Chair: Dieter Hutter |
| 9:30 - 10:00 |
Nikolaj Popov & Laura Kovacs |
Procedural Program Verification within Theorema |
| 10:00 - 10:30 |
Mircea Marin |
Constraint Solving and Sequence Variables |
| 10:30 - 11:00 |
Adi Craciun |
Theory Exploration by Lazy Thinking: A Case Study
(Presentation,
Correctness Proof,
Sample Proof,
Proof by lazy thinking)
|
