Decision Procedures and Applications
Viorica Sofronie-Stokkermans <firstname.lastname@example.org>
Markus Bender <email@example.com>
Time and place: Tuesdays, 12:00s.t.-14:00, Room B227
First meeting: 25.10.2016
English-German Dictionary of Deduction-related Terms
- 25.10.2016: Introduction, Motivation (V. Sofronie-Stokkermans)
- 31.10.2016, 8.11.2016, 15.11.2016, 6.12.2016, 9.12.2016 and 11-13.01.2017:
Individual meetings with the students
- 17.01.2017, 12:30-14:00: Short presentations (~ 5 min)
- 24.01.2017: "How to give talks" (V. Sofronie-Stokkermans)
- 31.01.2017: Background Information: Term rewriting systems (V. Sofronie-Stokkermans)
- 7.02.2017: Background Information: Theories (including the theory of uninterpreted functions + congruence closure); Combinations of decision procedures (definitions + the Nelson-Oppen combination method) (V. Sofronie-Stokkermans)
- 14.02.2017: Introduction to modal logic (V. Sofronie-Stokkermans)
- 10.03.2017: First version of the slides due
- 24.03.2017: 13:00 s.t., Room B 227:
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.
Application domains where decision procedures are used, such as
A preliminary list of suggested topics will be available soon.