Abbreviations

For more information about the lecture halls and seminar rooms, see our lecture room page. The names listed under "Technical Assistance" are student volunteers who will act as a contact person for technical questions of the lecturers and workshop speakers during the course or workshop.

Interval temporal logics

Interval-based temporal reasoning arises naturally in a variety of disciplines, incl. philosophy, linguistics, artificial intelligence, computer science. Yet, interval temporal logics are less studied and popular than point-based temporal logics, and one of the main reasons for this is the higher conceptual and computational complexity of the former. Undecidability is a common feature of most systems of interval logics, so the search for expressive yet decidable systems of interval logics is a problem of vital importance in that area. In this course we will provide a detailed introduction to interval temporal logics, and will discuss problems, techniques, and results on expressiveness, axiomatizations, (un)decidability, and tableau-based decision procedures for interval logics. Many exercises and open problems will be offered throughout the course. Course Outline: Day 1: Introduction to interval structures and logics. - Interval structures and relations. - Halpern-Shoham logic of intervals HS and some important fragments. Basic semantics of interval logics. - Venema's logic CDT. - Metric interval logics. - Overview of duration calculus and other interval-based logics. Day 2: Expressiveness. - Standard translation. - Comparing expressiveness of interval logics and FOL. Some expressive completeness results. - Interval logics and algebras of relations. Day 3: (Un)decidability - Undecidability results for HS and fragments of it. - Decidability via semantic restrictions and reduction to point-based logics. Day 4: Representation theorems, axiomatic systems, and tableau. - Representation theorems for interval structures. - Axiomatic systems for interval logics: some results and open problems. - General tableau procedure for interval logics. Day 5: Tableau-based decision procedures - Tableau-based decision procedures for interval neighbourhood logics and logics of subintervals. - Concluding remarks: research directions and open problems.