Temporal logic in artificial intelligence

Davide Bresolin
Dipartimento di Matematica, Università degli Studi di Padova,


Formal logic has had a central place in the study of artificial intelligence since its first conception in the 1950s. Why is this so? Logic has not been made formal just to make it suitable for computers and robots. Formal logic is also a tool for humans. Just as we could write, and execute, our grocery list and daily schedules in a computer program, so we could make our daily inferences by means of deduction in formal logic. Moreover, formal logic wasn’t even invented for machines, but to regiment and explicate human scientific reasoning.

The course will give an introduction to modal logic and temporal logic for students of the BMCS doctoral program. It will give the basics facts about modal and temporal logic, to provide a common ground for further study. Then, it will show why modal and temporal logics have become over the past 50 years very useful and important in computer science, and particularly for the formal specification, verification and synthesis of computerised systems of various nature


- Brief history and philosophical origins of modal and temporal logic.
- Reasoning about time: linear and branching time temporal logic.
- Modelling and formalising reactive systems with temporal logic.
- Applications of temporal logic in computer science: specification, verification and synthesis. The model checking problem .

Introductory reading

Peter Øhrstrøm and Per Hasle. Modern temporal logic: The philosophical background. In: Logic and the Modalities in the Twentieth Century, volume 7 of Handbook of the History of Logic, pages 447 – 498. North-Holland, 2006.

Clarke E.M. (2008) The Birth of Model Checking. In: 25 Years of Model Checking. Lecture Notes in Computer Science, vol 5000. Springer, Berlin, Heidelberg.

Course requirements
The course does not presuppose any previous background in formal logic nor in artificial intelligence.

Examination modality

Course material, enrollment and last minute notifications
Made available by the teacher at this Moodle address

4 May 2021, 16:30-18:30
5 May 2021, 16:30-18:30
11 May 2021, 16:30-18:30

Room 1BC50, Dept of Mathematics; Zoom link in case of quarantined students will be in the Moodle page of the course.

<< Courses in 2020-2021