|
Courses and Workshops
|
| Title: | Hybrid logics |
| Lecturer(s): | Massimo Franceschet (University of Amsterdam) and Balder ten Cate (University of Amsterdam) |
| Type: | Introductory Course |
| Section: | Logic and Computation |
| Week: | Second | | Time: | 11.00-12.30 (Slot 2) |
| Webpage: | http://staff.science.uva.nl/~francesc
|
| Reader: | Download | | Room: | A2 |
Description Hybrid languages extend traditional modal and temporal languages by
providing mechanisms for naming states and referring to states by their
names. These mechanisms increase the expressive power of the languages
while preserving, in some cases, their nice computational and
model-theoretic properties.
This course provides an introduction to hybrid logic, with special
emphasis on expressivity and reasoning. We start the course with a gentle
introduction to hybrid logic, explaining the motivation behind it and
discussing sound and complete proof systems that have been introduced in
the literature (in particular tableaux). After this introductory part
(first class), the course is divided in two main parts.
* The first part concerns the model-theoretic properties of hybrid
logic. The topics we will discuss include expressivity, frame
definability and interpolation. Each of these notions will be
explained, and no substantial background knowledge on model theory
is required (Classes 2 and 3).
* The second part concerns the computational behaviour of hybrid
logic. It includes a survey of decidability and complexity of the
satisfiability and model checking problem for various hybrid
languages. Finally, an example of a concrete application for hybrid
logic model checking is presented: the evaluation of queries and
constraints for semistructured data (Classes 4 and 5).
|
© 2003, 2004 LORIA, Carlos Areces. |
2004-09-07
| |
