Decision Procedures for Logical Theories

Instructors:

  • Viorica Sofronie-Stokkermans <sofronie@mpi-sb.mpg.de>
  • Uwe Waldmann <uwe@mpi-sb.mpg.de>

    • Time and place: Monday, 14:00-16:00, Room 23, MPI Building

    Preparatory meeting: April 15, 2008; 10:00 c.t.; Rotunda, 6th floor, MPI Building

    Exam certificates can be picked up in the RG1 secretary's office,
    MPI Building (Bldg E1.4), 1st floor, Room 157.
  • Schedule

  • Slides

  • Recommended literature

  • The articles mentioned in the list of suggested topics have been sent by e-mail.
  • A. Bradley and Z. Manna. The Calculus of Computation. Decision Procedures with Applications to Verification. Springer 2007.
    Available from the Semesterapparat (Software Model Checking).

    • Registration:

  • Preliminary registration by e-mail to Viorica Sofronie-Stokkermans

  • Registration: All participants are asked to register in HISPOS until 16.05.2008.
    For this please go to the following url: http://frweb.cs.uni-sb.de/03.Studium/011.HISPOS/
    Note that you should be registered in HISPOS in order to get a grade for the seminar.

    If you cannot register please inform Viorica Sofronie-Stokkermans.

    • Requirements for obtaining credit points:

  • Talk (40 min + 5 min discussions)
  • Written abstract: ~ 5 pages, final version due on July 14, 2008 at latest.
    It is recommended to hand in the written abstract 1-2 weeks after the talk.
  • Regular participation

    • 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 verification, knowledge representation and mathematics.

  • For a list of suggested topics click here

    • Viorica Sofronie-Stokkermans <sofronie@mpi-sb.mpg.de> December 17, 2007.