Decision Procedures for Logical Theories


Instructors:

  • Viorica Sofronie-Stokkermans <sofronie@uni-koblenz.de>
  • Matthias Horbach <horbach@uni-koblenz.de>
  • Time and place: Wednesday, 14:00-16:00, Room E 016

    First meeting: Wednesday, 23.04.2013, 14:00-16:00, Room E 016.


    Slides
  • Motivation [intro.pdf]
  • How to give talks [givingtalks.pdf] (by Uwe Waldmann)
  • (for more advice on giving research talks click here)
  • Background Information (Logical theories; decision procedures for simple theories) [slides-background.pdf]
  • Background Information (Combinations of logical theories; decision procedures for combinations of theories; applications) [slides-background2.pdf]
  • Verification by Abstraction-Refinement: Slides by Javier Esparza

  • Schedule

  • 23.04.2014: Introduction, Motivation (V. Sofronie-Stokkermans)
  • 30.04.2014: How to give talks
  • 1.05-15.05.2014: Individual meetings with the students
  • 21.05, 28.05, 4.06: Background Information (V. Sofronie-Stokkermans)
  • 18.06.2014: Short presentations (5-10min)
  • 11.07.2014: Presentations (14:00s.t.-18:00, Room B 227)
    • Bastian Krayer: ``Automata approach to Presburger arithmetic''
    • Daniel Enkirch: ``An efficient decision procedure for Unit Two-Variables per Inequality (UTVPI)} Constraints''
    • Christian Schlöffel: ``Reasoning about functions over numeric domains and applications in hybrid automata''
    • Scarlett Grenzemann: ``A decidable fragment of a theory of pointers''
    • Adrian Willems: ``Verification of safety properties for a system of trains''
    • Marcel Heinz: ``Verification by abstraction/refinement''
  • Abstracts
  • Deadline: 1.09.2014
  • 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 (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