Decision Procedures and Applications

Instructors:

  • Viorica Sofronie-Stokkermans <sofronie@uni-koblenz.de>
  • Matthias Horbach <horbach@uni-koblenz.de>

    • Time and place: Tuesday, 12:00-14:00, Room E 428

    First meeting: Tuesday, 14.04.2015, 12:00-14:00, Room E 428.

    Slides
  • Motivation [intro.pdf]
  • How to give talks [givingtalks.pdf] (by Uwe Waldmann)
    (for more advice on giving research talks click here)

  • Background Information 1 [slides-background.pdf]
    (Logical theories; decision procedures for simple theories)

  • Background Information 2 [slides-background2.pdf]
    (Combinations of theories; combinations of decision procedures: The Nelson/Oppen Method; Applications: decision procedures for data types (only main ideas))

  • Background Information 3 [slides-background3.pdf]
    (Term rewriting; Abstract reduction systems)
    • English-German Dictionary of Deduction-related Terms

    Schedule

  • 14.04.2015: Introduction, Motivation (V. Sofronie-Stokkermans)
  • 21.04.2015: How to give talks
  • 28.04, 5.05.2015 and 12.05: Individual meetings with the students
  • 19.05.2015: Background Information (V. Sofronie-Stokkermans)
  • 2.06.2015: Background Information (V. Sofronie-Stokkermans)
  • 9.06.2015: Short presentations (5-10 min)
  • 30.06.2015: Background Information (V. Sofronie-Stokkermans)
  • 7.07, 14.07 and 21.07: Presentations

    7.07.2015, 12:00 s.t., Room E428

  • Julia Schönberger:
    "Automata-based decision procedure for Presburger arithmetic"

  • David Friedrich:
    "Abstract Congruence Closure"

    • 14.07.2015, 12:00 s.t., Room E428

  • David Nagel:
    An efficient decision procedure for "Unit Two-Variables per Inequality (UTVPI)" Constraints

  • Shuyi Weng:
    "What's decidable about arrays?"

    • 21.07.2015, 12:00 s.t., Room E428

  • Kilian Laudt:
    "Decision procedures for recursive data structures with integer constraints"

  • Carl Brenk:
    "Terminological cycles in a description logic with existential restriction"
    • Abstracts
  • Deadline: 20.08.2015
  • Length: 5-7 pages (preferred: 5 pages)
  • Language: English or German
  • Recommended style files (latex):
  • Recommended style files (Word): Office-2007-Word.zip

    • 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

    Requirements:

  • Talk (ca 30 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