Logic in Computer Science and Artificial Intelligence

More about the course

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.

Teaching platform: See Canvas page.

Instructor Autumn term 2026: Valentin Goranko.

Instruction format: Lectures and exercises.

Examination: Home assignments.