Stockholm university logo, link to start page
Gå till denna sida på svenska webben

Logic in Computer Science and Artificial Intelligence

The course will introduce some of the most successful areas of applications of logic to computer science and artificial intelligence.

After a general revision of classical first-order logic as general language for knowledge representation, the course will present first-order resolution with unification as a practical method for automated reasoning. Then, the basics of logic programming and Prolog will be discussed briefly. The second part of the course is on logical methods for program verification based on Floyd-Hoare method for proving program correctness, further formalised in the propositional dynamic logic of programs PDL. The third part of the course will present the basic theory and applications of temporal logics for formal specification of properties of transition systems and computations in them, and for their formal verification by means of model checking. The last topic in this part will be on logics for multi-agent systems. The course will aim at providing sound theoretical background and conceptual understanding as well as practical knowledge and skills. It will involve exercises and hands-on experience with some popular implemented tools for automated reasoning, for logic programming and for model checking. The course is intended mainly for students in computer science and in philosophy, but is also relevant to students in mathematics.

  • Course structure

    Course webpage


    There will be 3 mandatory written assignments during the course, each consisting of a set of exercises. Two of the assignments will include practical sections. The assignments will be to be posted on Mondo 2 weeks before the submission deadline. Students must do these exercises individually and prepare written reports with their solutions. Strict dates for submission of the assignment reports will apply. The assignments will be checked and corrected by the lecturer, returned to the students for feedback, and then returned back to the lecturer. These assignments will be taken into account in the final grade.

  • Schedule

    The schedule will be available no later than one month before the start of the course. We do not recommend print-outs as changes can occur. At the start of the course, your department will advise where you can find your schedule during the course.
  • Course literature

    Note that the course literature can be changed up to two months before the start of the course.

    Valentin Goranko: Logic as a Tool (Wiley & Sons 2016)
    David Harel, Dexter Kozen & Jerzy Tiuryn: Dynamic Logic (MIT Press 2000)
    Michael Huth & Mark Ryan: Logic in Computer Science (Cambridge University Press, 2nd ed. 2004)
    Stephane Demri, Valentin Goranko & Martin Lange: Temporal Logics in Computer Science (Cambridge University Press 2016)

    Additional literature selected by the teacher.

  • Contact

    Student Councellor Sama Agahi