Das Programm des Deduktionstreffens 1998

Montag, 5.10.98

8:30	-	9:00	Registrierung der Teilnehmer vor Raum 1402
9:00	-	10:15	Session I
9:00	-	9:15	Begüßung der Teilnehmer durch Reinhold Letz und Tobias Nipkow
9:15	-	9:45	Francois Bry, Sunna Torge (LMU München) Die EP-Tableau-Methode
9:45	-	10:15	Thomas Rudlof (LMU München) SHR Tableau: A Framework for Automated Model Generation
10:15	-	10:45	Alexander von Drach, Tim Geisler, Sven Panne, David Sacher (LMU München) Eine abstrakte Maschine zur Modellgenerierung mit PUHR-Tableaux
10:45	-	11:15	Pause
11:15	-	12:15	Session II
11:15	-	11:45	Burkhart Wolff (Uni Freiburg) Funktionales Design und Implementierung von Grafischen Benutzungsoberflächen für Theorembeweiser
11:45	-	12:15	Markus Wenzel (TU München) Isabelle/Isar - Intelligible semi-automated reasoning
12:15	-	14:00	Mittagspause
14:00	-	16:30	Systemdemos
14:00	-	14:15	Kurzvortrag (Raum 1562): Christoph Weidenbach (MPI für Informatik, Saarbrücken) SPASS, Beweiser für Prädikatenlogik erster Stufe
14:15	-	16:30	Systemdemos: Raum 1562: Slim Abdennadher, Thom Frühwirth, Michael Marte (LMU München): Ein constraintbasierter Stundenplaner für das Institut für Informatik Christoph Benzmüller et. al. (Uni Saarbrücken): OMEGA Christoph Weidenbach (MPI für Informatik, Saarbrücken): SPASS, Beweiser für Prädikatenlogik erster Stufe Andreas Wolf, Gernot Stenz (TU München): p-SETHEO, strategie-paralleler Beweiser Raum 1565: Felix Joachimski, Monika Seisenberger et. al. (LMU München): Das Minlog-System Tim Geisler et al. (LMU München): SatAM - Satchmo Abstract Machine Cornelia Pusch, Markus Wenzel et. al. (TU München): Java-Formalisierung mit Isabelle Markus Wenzel et. al. (TU München): Das Isabelle/Isar-System
16:30	-	18:00	Fachgruppensitzung (Raum 1562)
19:30	-		Abendessen im Botticellizimmer im "Ratskeller" am Marienplatz

Dienstag, 6.10.98

9:00	-	10:30	Session III
9:00	-	9:30	Cornelia Pusch (TU München) Correctness of the Java Bytecode Verifier
9:30	-	10:00	Leonor Prensa Nieto (TU München) The Gries/Owicki Method in Isabelle/HOL
10:00	-	10:30	Reinhold Letz, Gernot Stenz (TU München) Neudesign von Setheo in Scheme (Extended Abstract)
10:30	-	11:00	Pause
11:00	-	12:30	Session IV
11:00	-	11:30	Uwe Waldmann (MPI für Informatik, Saarbrücken) Erweiterung von Reduktionsordnungen zu ACU-kompatiblen Reduktionsordnungen
11:30	-	12:00	Andreas Nonnengart (MPI für Informatik, Saarbrücken) Elimination von Prädikatvariablen und ihre Anwendung in der Verifikation hybrider Systeme
12:00	-	12:30	Bernhard Beckert (Uni Karlsruhe) Integrierter Deduktiver Software-Entwurf
12:30	-	14:00	Mittagspause
14:00	-	15:00	Session V
14:00	-	14:30	Klaus Schulz (LMU München) Entscheidbarkeit von Kontextunifikationsproblemen mit zwei Variablen
14:30	-	15:00	Bertram Fronhöfer (TU München) Proof Search in Acyclic Matrix Graphs
15:00	-	15:30	Pause
15:30	-	16:30	Session VI
15:30	-	16:00	Marc Fuchs (TU München) Generation of Clausal Lemmas with Genetic Programming
16:00	-	16:30	Matthias Eberl (LMU München) Normalisierung durch Auswertung
16:30			Ende

Zurück zur Hauptseite