Decision Procedures for Logical Theories


  • Viorica Sofronie-Stokkermans <>
  • Time and place: Wednesday, 14:00-16:00, Room E 016

    First meeting: Wednesday, 17.04.2013, 14:00-16:00, Room F 330.

  • Motivation [intro.pdf]
  • How to give talks [givingtalks.pdf] (by Uwe Waldmann)
  • (for more advice on giving research talks click here)
  • Background: Logical theories, Decision Procedures;
    Combinations of theories, Combinations of decision procedures;
    The Nelson-Oppen method; Local theories (idea); Hierarchical reasoning (idea) [background1.pdf]
  • Background: Hierarchical reasoning/Local theory extensions [background2.pdf]
  • Background: Unification. Preliminary slides: [background3.pdf] (will be updated on 19.06.2013)

  • News
  • Presentations: Wed. 17.07.2013, Start at 13:00, Room B 227.

    • Irina Karpova
      "Automated complexity analysis based on ordered resolution"
      (D. Basin and H. Ganzinger)
    • Thomas Schmorleiz
      "Towards complete reasoning about algebraic specifications"
      (S. Jacobs and V. Kuncak)
    • Eduard Schleining
      "Unification in the union of disjoint equational theories: Combining decision procedures"
      (F. Baader and K. Schulz)
    • Sonja Polster
      "Unification in the description logic EL"
      (F. Baader and B. Morawska)

  • Next meeting: 19.06.2013: Background information: discuss slides from 5.06 + Unification (Viorica Sofronie-Stokkermans)
  • 5.06.2013: Background information: Hierarchical reasoning/Local theory extensions (slides online)
  • 29.05.2013: Background information: Logical theories, combinations of theories, verification tasks (talk by V. Sofronie-Stokkermans)
  • 22.05.2013: Free (Pfingstferien)
  • 15.05.2013: Individual discussions; Papers assigned
  • 8.05.2013: Individual discussions about the papers
  • 1.05.2013: Free (Maifeiertag)
  • 24.04.2013: How to give talks
  • 17.04.2013: Motivation

  • Description

    General logical formalisms such as predicate logic, set theory, or number theory are undecidable or even not recursively enumerable. However, in applications it is often the case that only special fragments need to be considered, which are decidable and sometimes even have a low complexity: For instance, the theory of integers with addition is decidable; certain fragments of theories of data structures used in verification such as lists, pointers and arrays; as well as some fragments of set theory often used in knowledge representation are decidable as well. The seminar will focus on three orthogonal issues:
    Decidable theories: Identify logical theories which are decidable resp. tractable.

    Methods of proving decidability: Identify general principles for proving decidability.

    Applications: Application domains where decision procedures are used, such as
  • program verification,
  • verification of reactive systems or hybrid systems,
  • knowledge representation, description logics,
  • mathematics.

  • A preliminary list of suggested topics is available here


  • Talk (40 min + 5 min discussions)
  • Written abstract: ~ 5 pages.
    It is recommended to hand in the written abstract 1-2 weeks after the talk.
  • Regular participation