Selected Topics in Automated Reasoning

Instructor:

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

    • Time and place:

  • Lecture: Thursday, 16:00-18:00, Room 21, MPI building.
  • Exercises: Monday, 12:30-14:10, Room 21, MPI building.

    • Preparatory meeting: Thursday, April 23, 2009, in room 24, MPI building.

  • Registration: The participants are asked to register in HISPOS.
     This is possible between 15.05.2009 and 03.06.2009.
     In case of technical problems please send an e-mail to: studium@cs.uni-sb.de

  • Exam: The exam will be oral. It will take place on Thursday, July 30, 2009, from 15:00 to 18:00 in the MPI Building, Rotunda, 6th floor.
    A summary of topics for the exam is available here.

  • Question and answer session: As a preparation for the exam, there will be a "Question and answer" session on Wednesday, July 29, at 14:00. I would greatly appreciate it if you would send me your questions by e-mail in advance.
  • You can get the certificates in Jeniffer Mueller's office (RG1 secretary, MPI building, 6th floor, Room 602).
    The grades will be announced in HISPOS by August 10th, 2009.
  • News and Schedule

  • Slides and literature

  • Exercises

    • Contents

     The goal of this lecture is to present the recent results in automated reasoning and their applications in verification, knowledge representation, logic and algebra
  • Structure of the lecture

    • Motivation

     One of the most important research objectives in mathematics and computer science is to obtain means of reasoning in and about complex systems. These can be, for instance:
  • complex mathematical theories
  • programs, or more general reactive or hybrid systems
  • large, distributed databases
  • or very complex systems (e.g. reactive or hybrid systems with embedded software, whose behavior is controlled by databases, reasoning about knowledge and belief, or planning mechanisms).
    • Proving properties of such systems is extremely important. In safety-critical systems even small mistakes can provoke disasters. Since the amount of data which has to be handled in all the application domains mentioned above is usually huge, computer support is necessary. General-purpose programs for solving all types of problems mentioned above do not exist. However, for concrete application domains automatic procedures exist. The goal of this lecture is to present specific domains in mathematics, logics, verification and knowledge representation for which efficient methods for automated reasoning exist.

    Recommended literature

    Course material from other lectures

    Propositional logic, first-order logic

    Decision procedures

    Lecture Notes