Theorema-Ultra-Omega'05 Workshop


November 14-15th 2005
Saarland University, Germany

  • Organizers: Serge Autexier and Christoph Benzmüller
  • Workshop Place: The workshop will take place on the Campus of the Saarland University (interactive map) in the new Computational Linguistic (C7.4, in the bottom part of the yellow part in that interactive map) building.
  • The workshop fee will amount to 40 EUR and includes the lunches, coffee break and the workshop dinner on monday evening.
  • Traveling and Hotels: Traveling information to the University Campus ( interactive map ) Saarbrücken can be found here . A selection of hotels as well as a link to the Saarbrücken Tourist's office can be found here. For a map see below.
  • Get-Together: On sunday evening from 7:30pm on we plan to have an informal get-together at the restaurant "Stiefelbräu", (Zum Stiefel 2, 66111 Saarbrücken). Mind the fact that there are next to each other a restaurnt "Zum Stiefel" and the restaurant "Stiefelbräu". For a map see below.
  • Workshop dinner: The workshop dinner will be on monday, november 14th at "Le Bouchon" (Am Staden 18). For a map see below.
  • Maps:
    • Online bus schedules: We recommed to take a bus from the bus station Rathaus (see below for the map). Take either bus Nr. 11 or Nr. 19 both towards "Dudweiler Dudoplatz" and get off at the station "Universität Campus" (the first on the campus, in the red part of the interactive map; Bus Nr. 11 leaves "Rathaus" at 8:00am and then every 30min; Bus Nr. 19 leaves 8:08am and then every 15min).
    • Map1: A map locating the bus station for the buses 11 and 19, the selected hotels, the pub-restaurant "Stiefelbräu" and the central station (gray streets are pedestrian zones).
    • Map2: A map locating the bus station for the buses 11 and 19, the some of the selected hotels, the pub-restaurant "Stiefelbräu" and the restaurant "Le Bouchon" (gray streets are pedestrian zones).

Program

Monday november 14th 2005
Session 1Theorema 1
9:00 -- 9:15 Jörg Siekmann Welcome and Overview of Computer Science in Saarbrücken (PPT, PDF)
9:30 -- 10:30 Bruno Buchberger and Adrian Craciun Algorithm Synthesis by Lazy Thinking: Case Study Gröbner Bases (Mathematica NB, PDF)
10:30 -- 11:00Coffee break
Session 2Theorema 2
11:00 -- 11:30 Martin Giese Towards an effective Reflection Mechanism in Theorema (Mathematica NB, PDF)
11:30 -- 12:00 Temur Kutsia Matching with regular constraints (PDF)
12:00 -- 14:00Lunch
Session 3Ultra & Theorema
14:00 -- 14:30 Fairouz Kamareddine MahLang, a framework for computerising mathematics (PDF)
14:30 -- 15:00 Manuel Maarek Towards an Object-Oriented Structure of Mathematical Text (PDF)
15:00 -- 15:30 Wolfgang Windsteiger The CreaComp project: Theorema for computer supported teaching and learning of mathematics (PDF)
15:30 -- 16:00Coffee break
Session 4Theorema 3
16:00 -- 16:25 Florina Piroi und Camelia Rosenkranz Organizational Tools in Theorema
16:25 -- 16:50 Markus Rosenkranz Using Polynomial Structures in Reasoning with Reflexion (PDF)
16:50 -- 17:15 Laura Kovacs Imperative Program Verification in Theorema (PDF)
17:15 -- 17:40 Nikolaj Popov Functional Program Verification in Theorema (PS)
17:40 -- 18:05 Robert Vajda Finding Witness Terms in ETRCF by Quantifier Elimination Techniques (Mathematica NB, PDF)
19:30 -- Workshop Dinner



Tuesday november 15th 2005
Session 5Omega
9:00 -- 9:15 Christoph Benzmüller & Jörg Siekmann General introduction to OMEGA (PPT, PDF)
9:15 -- 10:00 Serge AutexierArchitecture of the new OMEGA system + The CORE Calculus (PDF)
10:00 -- 10:15 Dominik DietrichThe new task-level and the new proof-planner (PDF)
10:15 -- 10:30 Marc WagnerPLATO (PDF)
10:30 -- 11:00Coffee break
Session 6Math. Services and Logical Foundations
11:00 -- 11:30 Jürgen ZimmerMathServ -- Semantic Reasoning Web Services (PDF)
11:30 -- 12:00 Chad E. BrownThe Foundation of Grundlagen (PDF)
12:00 -- 14:00Lunch
Session 7Math. Knowledge: Management, Representation and Documents
14:00 -- 14:30 Dieter HutterManagement of Change
14:30 -- 14:50 Martin PolletA Tough Nut for Mathematical Knowledge Management (PDF)
14:50 -- 15:10 Armin FiedlerVeriMathDoc
15:10 -- 15:30 Henri LesourdTeXmacs
15:30 -- 16:00Coffee break
Session 8Dialog
16:00 -- 16:20 Christoph BenzmüllerThe DIALOG Project (PDF)
16:20 -- 16:40 Mark BuckleyThe Dialog-Manager (PDF)
16:40 -- 17:00 Marvin SchillerGranularity (PDF)
17:00 -- 17:30 Dimitra Tsovaltzi Automatic Dialogue Adaptive Feedback for Tutoring Proving (PDF)
17:30 -- 18:00 Erica Melis ActiveMath: Update 2005 (PPT, PDF)

Participants

Serge Autexier
Markus Aderhold
Christoph Benzmüller
Bruno Buchberger
Chad E. Brown
Mark Buckley
Adrian Craciun
Dominik Dietrich
Armin Fiedler
Andreas Franke
Martin Giese
Helmut Horacek
 Dieter Hutter
Fairouz Kamareddine
Laura Kovacs
Teimuraz Kutsia
Henri Lesourd
Manuel Maarek
Roy McCasland
Erica Melis
Alberto Gonzalez Palomo
Florina Piroi
Nikolaj Popov
Martin Pollet
 Georg Regensburger
Camelia Rosenkranz
Markus Rosenkranz
Marvin Schiller
Jörg Siekmann
Dimitra Tsovaltzi
Robert Vajda
Marc Wagner
Wolfgang Windsteiger
Magdalena Wolska
Alexander Zapletal
Jürgen Zimmer

Previous workshop in 2003
Serge Autexier
Last modified: Mon Dec 19 10:41:48 CET 2005