Deduktionstreffen 2010

Organisatorisches

Das Deduktionstreffen findet auf dem Campus Süd des KIT im Gebäude 50.41 (Allgemeines Verfügungsgebäude, AVG) im Raum 045/046 statt.

Die Dauer der Vorträge beträgt 6 Min (exklusive einer kurzen Diskussion im Anschluss). Die Vorträge dienen als "Teaser" für eine anschließende Diskussion am Poster, für die etwas mehr als eine Stunde eingeplant ist. Die Größe der Poster für die Postersession sollte DIN A0 nicht überschreiten.

Am Montag, 20.09. besteht die Möglichkeit eines gemeinsamen Mittagessens in der Mensa für alle Teilnehmer, die bereits um 13Uhr anwesend sind. Der Treffpunkt dazu ist direkt vor dem Vortragsraum um 13:00Uhr.

Eingeladene Vorträge

Matthias Baaz: Towards a proof theory of analogical reasoning
In this lecture we compare three types of analogies based on generalizations and their instantiations:
1. Generalization w.r.t. to invariant parts of proofs (e.g., graphs of rule applications etc.).
2. Generalization w.r.t. to an underlying meaning. (Here proofs and calculations are considered as trees of formal expressions. We analyze the well-known calculation of Euler demonstrating that the 5th Fermat number is compound.)
3. Generalization w.r.t. to the premises of a proof. (This type of analogies is especially important for juridical reasoning.)
Gregor Snelting: Quis Custodiet Ipsos Custodes?

Programm

Montag, 20.09.2010

13:00-14:00: Registrierung
14:00-15:00: Eingeladener Vortrag
Matthias Baaz (Technische Universität Wien)
Towards a Proof Theory of Analogical Reasoning
15:00-15:30: Kaffeepause
15:30-17:30: Postersession I
- Anni-Yasmin Turhan (Technische Universität Dresden)
  Computing Generalizations in the Description Logic EL through Completion
- Björn Pelzer (Universität Koblenz-Landau)
  Logische Fragebeantwortung in der Praxis
- Claudia Schon (Universität Koblenz-Landau)
  Linkless Normal Form for ALC Concepts
- Patrick Wischnewski (Max-Planck-Institut für Informatik, Saarbrücken)
  On the Saturation of YAGO
- Christian Doczkal (Universität des Saarlandes)
  Formalizing Tableaux Decision Procedures in Coq
- Dominik Dietrich (DFKI Bremen)
  Declarative Tactics
- Jörg Siekmann (DFKI Saarbrücken)
  IFCOLOG
17:30-18:00: Business Meeting der Fachgruppe
19:00-: Abendessen im Restaurant Hoepfner Burghof

Dienstag, 21.09.2010

09:00-10:00: Eingeladener Vortrag
Gregor Snelting (Karlsruher Institut für Technologie)
Quis Custodiet Ipsos Custodes?
10:00-10:30: Kaffeepause
10:30-12:30: Postersession II
- Alexander Lux (Technische Universität Darmstadt)
  Information Flow Control and Timing Channels
- Bernhard Beckert (Karlsruher Institut für Technologie)
  Testing Program Verification Systems
- Stephan Falke (Karlsruher Institut für Technologie)
  Termination Analysis of While-Programs Using Term Rewriting Techniques
- Nathan Wasser (Technische Universität Darmstadt)
  Avoiding Unnecessary AC(I)-Matchers
- Stephan Schulz (Technische Universität München)
  Fingerprint Indexing for Paramodulation
- Thomas Ströder (RWTH Aachen)
  Termination Graphs for Real Programming Languages
12:30-13:30: gemeinsames Mittagessen
13:30-15:30: Postersession III
- Carsten Fuhs (RWTH Aachen)
  Synthesizing Shortest Straight-Line Programs over GF(2) using SAT
- Carsten Ihlemann (Max-Planck-Institut für Informatik, Saarbrücken)
  Hierachical Reasoning in Combination of Theories
- Chad Brown (Universität des Saarlandes)
  Reducing Theorem Proving to a Sequence of SAT Problems
- Francis Gasse (Max-Planck-Institut für Informatik, Saarbrücken)
  Reasoning for Expressive Description Logic via SAT
- Florian Merz (Karlsruher Institut für Technologie)
  Low-level bounded model checking
- Florian Rabe (Jacobs University Bremen)
  Formalizing Model Theory
- Ewaryst Schulz (DFKI Bremen)
  Formalizing the Calculation Method of an Industrial Standard
15:30-16:00: Kaffeepause, Ende