Invited Speakers

Hans van Ditmarsch (University of Seville)
Dynamic Epistemic Logic and Belief Revision
18–23 January
[Abstract +]
Epistemic logic models knowledge and belief in multi-agent systems. How to model change of knowledge has been investigated since the 1980s. Following the influential Interpreted Systems approach as in Reasoning about Knowledge by Fagin et al. (1995), a strand of modal logic with epistemic modal operators for knowledge and dynamic modal operators for knowledge change has developed during the 1990s, based on initial contributions by Plaza (1989) and van Benthem (1987/1989). The action model approach proposed by Baltag, Moss, Solecki (1998) has so far been the most influential. The textbook Dynamic Epistemic Logici (van Ditmarsch et al, 2007) gives an overview of these developments, including detailed and full proofs, extensive examples, and exercises including answers. The latest further developments also incorporate factual change, belief revision, and preference change. In this course I propose to teach the basics of Dynamic Epistemic Logic, focussing on the semantics and the applications.
1. Epistemic logic (including group epistemic operators such as common knowledge).
2. Public announcement logic.
3. Action model logic (full expressive power, includes non-public events).
4. Recent developments (factual change, belief revision).
5. Applications and puzzles (communication protocols, 100 prisoners, hangman paradox, …).
Tobias Nipkow (Technische Universität München)
A Practical Introduction to Theorem Proving with the Isabelle System
18–23 January
[Abstract +] | Slides | Printable version
Isabelle/HOL is an interactive theorem prover for HOL, a popular version of higher-order logic. The purpose of this tutorial is to familiarize students and researchers with the basics of specification and proof in Isabelle/HOL. The course combines traditional lectures with on-line demos and offers practical exercises. At the end of the course participants will be able to formalize and prove (with Isabelle's help) simple problems in logic, discrete mathematics and functional programming. The following topics are covered:
- datatypes and recursive functions,
- proof by structural induction and by simplification,
- proofs in propositional logic and predicate logic,
- set theory and inductively defined sets.
Learning how to write formal proofs is like learning any language: it requires practice. Hence the course offers practical exercises that the students are encouraged to solve in the computer lab where Isabelle will be installed. Participants with their own laptop should install Isabelle beforehand. Isabelle can be downloaded here.
Steven Lindell (Haverford College)
Logic and Models of Computation
20–23 January
[Abstract +] | Talk 1 | Talk 2 | Talk 3 | Talk 4 | Talk 5 | Talk 6

History of logic and computation

There's a long and rich history to the mechanization of thought. We will cover the 2,000 year saga from its Aristotelian origins up to its Boolean foundations. Along the way there were many milestones in the history of computing which eventually led to machines that could calculate in logic.

Modern logic and definability theory

We will start with the data models most useful in computing: relational (databases) and functional (data structures). After reviewing the syntax and semantics of first-order logic, we will continue on from there to examine various levels of definability including second-order, and most importantly inductive (fixed-point) definability.

Models of computation and complexity theory

Various types of computer models will be introduced, including sequential (automaton based) and concurrent (circuit based). The asymptotic consumption of resources connects with feasible complexity classes such as logarithmic space and polynomial time. The issue of non-determinism raises fundamental unsolved problems in the field, such as P versus NP.

Descriptive complexity and finite model theory

The definability and complexity theory of the previous lectures are brought together in a machine-independent approach to computation that has illuminated fundamental problems in computational complexity, and also raises fundamental questions of its own. We leave the student with open questions and directions for future study.
Antony Galton (University of Exeter)
Spatial and Temporal Knowledge Representation
26–29 January
[Abstract +] | Talk 1 | Talk 2 | Talk 3 | Talk 4 | References
What is Knowledge Representation? Main Themes
- Representation and reasoning
- Commonsense knowledge
- Quantitative vs qualitative
- Vagueness, uncertainty and granularity
Temporal Knowledge Representation
- States, processes and events
- Modal vs first-order approaches
- Reification
- Formal properties of instants and intervals
- Compositional reasoning
Spatial Knowledge Representation
- Analogies and disanalogies between time and space
- Mereotopology
- Beyond mereotopology: distance, direction, etc
Combining Space and Time
- Spatio-temporal data models
- Qualitative spatial change
- Continuity
- Topological mode spaces
Valentin Goranko (Technical University of Denmark, Lyngby)
Model theory of modal logic
25–29 January
[Abstract (PDF)] | Talk 1 | Talk 2 | Talk 3 | Talk 4 | Talk 5