Home | Impressum | Sitemap | KIT
Termine

  • bis 09. Okt. 2011

    Einreichung von Vorträgen

  • 20. Okt. 2011

    Anmeldung: ab 11:30 Uhr

    Beginn: 12:45 Uhr

  • 21. Okt. 2011

    Ende: 18 Uhr

Deduktionstreffen 2011

Organisatorisches

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

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

Am Donnerstag, den 20.10. besteht die Möglichkeit eines gemeinsamen Mittagessens in der Mensa für alle Teilnehmer, die bereits um 11:30Uhr anwesend sind. Der Treffpunkt dazu ist direkt vor dem Vortragsraum um 11:30Uhr.

Eingeladene Vorträge

  • Ulrich Furbach: First-order Tableaux in Open Domain Question Answering

    In a first part of the talk the hyper tableau calculus and its implementation is reviewed and its extension for equality handling is discussed. In a second part we introduce the application within LogAnswer. LogAnswer is an open domain question answering system; it receives a natural-language question regarding any topic, and it returns a natural-language answer found in a knowledge base. The knowledge base consists of several parts: A formal logical representation of a snapshot of the entire German Wikipedia. These are 12 millions sentences which are transformed semi-automatically into a logical representation. A second part consists of background knowledge, e.g. knowledge about spatial and temporal relations, which is necessary to answer arbitrary natural language questions. Currently we are working on integrating external ontologies like Cyc and webservices.

  • Thomas Sturm: Effective Quantifier Elimination - Implementations, Applications, Perspectives

    Effective quantifier elimination procedures for first-order theories provide a powerful tool for generically solving a wide range of problems based on logical specifications. In contrast to general first-order provers, quantifier elimination procedures are based on a fixed set of admissible logical symbols with an implicitly fixed semantics. This admits to make use of subalgorithms from symbolic computation. The talk gives an overview of several theories that admit quantifier elimination and for which there are implementations available in our open-source software Redlog. The focus is on real quantifier elimination and its applications and on recent research on quantifier elimination for the integers. We are also going to consider parametric quantified SAT-solving as an example for effective quantifier elimination over initial Boolean algebras.

  • Christof Teuscher: A Modern Perspective on Turing's Unorganized Machines

    Turing proposed unorganized machines and evolutionary search in a 1948 National Physical Laboratory (NPL) report entitled "Intelligent Machinery." These machines have very similar properties to what is today known as random Boolean networks, which have been used as models for genetic regulatory networks. In addition, the concept of (self-) assembling simple compute nodes that are interconnected in unstructured ways has gained significance with the advent of nano- and molecular electronics over the last decade. In this talk I will first present Turing's various original unorganized machines, extensions to them, and then relate the work to contemporary random Boolean networks, nano- and molecular electronics, and computing theory. I will illustrate that many of Turing's original ideas are more than ever current, influential, and deeply fascinating.


Programm

Donnerstag, 20.10.2011

  • 11:30-12:45: Registrierung
  • 12:45-13:00: Begrüßung
  • 13:00-14:00: Eingeladener Vortrag (gemeinsam mit COMPUTING 2011)
    Christof Teuscher (Portland State University, USA)
    A Modern Perspective on Turing's Unorganized Machines
  • 14:00-14:30: Kaffeepause
  • 14:30-16:00: Vorträge Postersession I
    • Serge Autexier (DFKI Bremen)
      Structure Formation in Formal Theories
    • Christian Doczkal (Universität des Saarlandes)
      Constructive Formalization of Modal Logic
    • Denis Lohner (Karlsruher Institut für Technologie)
      Formalisierung eines Datenfluss-Analyse-Frameworks in Isabelle/HOL
    • Andreas Lochbihler (Karlsruher Institut für Technologie)
      Animating the Formalised Semantics of a Java-like Language
    • Tianhai Liu (Karlsruher Institut für Technologie)
      Bounded Verification of Java Programs using SMT
    • Marc Brockschmidt (RWTH Aachen)
      Termination Graphs for Java Bytecode
    • Stephan Falke (Karlsruher Institut für Technologie)
      Termination Analysis of C Programs using Term Rewriting Techniques
    • Fabian Emmes (RWTH Aachen)
      A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems
  • 16:00-16:30: Kaffeepause
  • 16:30-17:30: Postersession I
  • 17:30-18:00: Business Meeting der Fachgruppe
  • 19:30-: Abendessen im Hoepfner Burghof

Freitag, 21.10.2011

  • 09:00-10:00: Eingeladener Vortrag
    Ulrich Furbach (Universität Koblenz-Landau)
    First-order Tableaux in Open Domain Question Answering
  • 10:00-10:30: Kaffeepause
  • 10:30-12:30: Postersession II
    • Björn Pelzer (Universität Koblenz-Landau)
      Erweiterung deduktiver Fragebeantwortung (Expanding Deductive Question Answering)
    • Patrick Wischnewksi (Max-Planck-Institut für Informatik)
      YAGO++ Query Answering
    • Claudia Schon (Universität Koblenz-Landau)
      Instance-Level Deletion for ALC Knowledge Bases
    • Markus Bender (Universität Koblenz-Landau)
      Extending the E-Hyper Tableau Calculus
    • Tobias Tebbi (Universität des Saarlandes)
      Correctness of Tableau-Based Decision Procedures with Backjumping
    • Stephan Schulz (TU München)
      Practical Performance of Fingerprint Indexing for Paramodulation
    • Christian Schwarz (Universität Koblenz-Landau)
      Modelling a Real-Time Control System using Parameterized Linear Hybrid Automata
  • 12:30-14:00: Mittagessen
  • 14:00-15:00: Eingeladener Vortrag
    Thomas Sturm (Max-Planck-Institut für Informatik)
    Effective Quantifier Elimination - Implementations, Applications, Perspectives
  • 15:00-15:30: Kaffeepause
  • 15:30-17:30: Postersession III
    • Christoph Zengler (Universität Tübingen)
      Boolean Gröbner Bases in SAT Solving
    • Andreas Kübler (Universität Tübingen)
      New Approaches to Boolean Quantifier Elimination
    • Paolo Marin (Universität Freiburg)
      Incremental QBF Solving and its Use in Partial Design Verification
    • Stefan Kupferschmid (Universität Freiburg)
      Craig Interpolation for Non-linear Constraints
    • Christoph Gladisch (Karlsruher Institut für Technologie)
      Verification-based Satisfiability Proving
    • Daniel Bruns (Karlsruher Institut für Technologie)
      Semantics of Model Fields Inspired by Epsilon Terms
    • Aboubakr Achraf El Ghazi (Karlsruher Institut für Technologie)
      A Dual-Engine for Early Analysis of Critical Systems