S. Autexier, Ch. Benzmüller, C. E. Brown, D. Dietrich, M. Schiller and J. Zimmer
 |
||||
 Infos |
Systems |
Exercises |
Presentations |
Literature |
|
||||
Topic:
Some top mathematical assistant systems of our times are going to be evaluated in some paradigmatic applications and an acount on their special features, application domains, pros and cons,and the personal experiences with them is to be given in the seminar.
Time and Venue:
Preparation meeting (Vorbesprechung): Wednesday, April 19th, 2006, Room 407, 15 c.t.
Second meeting: Wednesday, April 26th, 2006, 14 c.t.
The "hard-working phase" will be in the week 31st Juli - 6th August
The presentations will be held on the 25th of August
Seminar: The seminar will consist of different working phases. Important to note is that approx. 3 students will form one team in the seminar. In the first working phase (Introduction Phase, approx. 4 weeks, beginning of SS06) each team will have to get familiar with the mathematical assistant systems they are supposed to work with -- typically each team will work with two systems. In the second phase (Warm-up Phase, approx. 8 weeks, mid till end of SS06) each team will work on some formalization problems we will set up. In the third phase (Hard-Working/Hot Phase, 31st Juli - 6th August) we will carry out the actual system comparison. We will then distribute a carefully selected choice of problems from mathematics and formal methods and ask the teams to try to formalize and verify them within their mathematical assistant systems. During this phase we expect that the students spent at least 6-8 hours a day on this task. The aim is to push the formalization and verification as far as possible in each system. During each phase the teams shall take detailled notes. This notes will later be turned into presentations at the very end of the seminar (25th of August). In this fourth phase of the seminar each student will have to present part of their groups work in a carefully worked out half hours presentation.
Language:
English
Registration:
Registration is possible at the preparation meeting.