We expect students to be comfortable with the basics of theoretical computer science (fi nite state automata and regular languages of finite words, and what does it mean for a problem to be EXPTIMEhard, undecidable, etc.) as taught, for example, in a book like Sipser's Introduction to the Theory of Computation. Students should also be familiar with the syntax and semantics of predicate logic.
Knowledge of the course "Automata, Logic and Games" would be helpful, but not essential (for students who have not taken this course, the proposers will recommend additional background reading from the course notes/slides).
This is a reading course run by the Department of Computer Science for MFoCS students only.
For expressive logics such as first-order logic, key analysis problems, such as whether a sentence is satisfiable, or whether one sentence follows from another, are undecidable. There are two standard responses to regain decidability: one can restrict the structures considered or one can restrict the logic. A surprising development is that these two kinds of restrictions are interconnected. In particular, one can obtain decidable logics (with no restriction on the structures) using decidability results that restrict the structures.
The aim of this course is to follow the development of this idea from work in modal logic that is several decades old, to more recent examples representing some of the most expressive decidable logics. We will see how tree automata are the key to reasoning about logics on restricted structures, and how unravellings and simulations are the key to transferring these results to general structures. We will also discuss some applications of the results in ontological reasoning and databases.
Prof Micheal Benedikt
Students will be able to:
1) explain the main technique for getting from decidability results on restricted structures to decidability results for logics over all structures;
2) understand how the method can be used to analyse a variety of highly expressive logics, and to solve problems in ontological reasoning and databases.
Bisimulation games and unravellings. Tree decompositions and encodings. Two-way alternating tree automata. Analysing the mu-calculus with backwards modalities using automata. Analysing guarded logics using automata. Applications to closed and open world query answering problems.