Decision Procedures for Logical Theories
Instructors:
Viorica Sofronie-Stokkermans <sofronie@mpi-sb.mpg.de>
Uwe Waldmann <uwe@mpi-sb.mpg.de>
Time and place: Tuesdays, 9:00ct - 11:00; Room 24, MPI Building
exception on November 15, 2005: 9:00ct - 11:00;
Room 015, Computer Science Building (E 1.3, previously 45)
Registration: by e-mail to Viorica Sofronie-Stokkermans
Requirements for obtaining credit points:
Talk (45 min); Written abstract
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;
the universal theories of data structures such as lists 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.
Suggested Topics
Slides
Schedule
Viorica Sofronie-Stokkermans
<sofronie@mpi-sb.mpg.de>
November 8, 2005.