We all know that logic underlies all digital technology, just like calculus underlies all
engineering, in the form of bits and logic gates.
But the relation between computer science and logic goes much deeper than that.
Originally, logic was used by the Greek Sophists to demonstrate the correctness of their argument in
The ambiguity of human languages asked for formulations propositions and arguments in a symbolic
This lead to the development of logic as a field in its own right starting with the end of the
At that time, the hope was to find one logic that would allow the formalisation of all of
mathematics by finite means and thereby provide an absolutely correct foundation.
This hope was shattered by Gödel's incompleteness theorem, and thus contemporary logic studies
various logical systems that are adjusted to different purposes.
However, the work of Gödel also showed an intimate relationship between logic and computation.
This is where this course comes in:
We will study propositional and first-order logic from the perspective of computer science,
including proof systems, algorithms, limitations and the relation to computation.
The course gives an introduction to the field of mathematical logic by presenting the syntax and
semantics of propositional logic and of the richer language of first-order logic.
The goal is to enable students to formally specify and verify properties of systems by means of
syntactic formulas and proof systems.
We also investigate algorithmic proofs and the use of logic to describe computations.
Finally, we will understand how logic can be used to describe computations and how it is limited
in a similar way as computers.
The most updated version of the timetables can be found on the students' website:
Mode of instruction
Self-study of lecture notes, complemented with in-depth video tutorials and Q&A sessions.
Weekly assignments will be provided and questions will be answered by the course team.
Students will be evaluated on the basis of a written examination complemented with take-home
Examination is worth 70% of the final grade (with a minimum of 5.5).
The remaining 30% is from the average grade of take-home assignments (the best 80%).
At least half of the take-home assignments have to be completed.
A retake is offered for the exam.
The main source of information are the lecture notes provided during the course.
Additionally, the following sources can be consulted for further study.
Michael R. A. Huth and Mark D. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004.
Jon Barwise and John Etchemendy. Language, Proof and Logic, CSLI Publications, 1999.
Sara Negri and Jan von Plato. Structural Proof Theory
Jean H. Gallier. Logic for Computer Science, John Wiley & Sons, 1987.
J.F.A.K. van Benthem, H.P. van Ditmarsch, J. Ketting, J.S. Lodder, and W.P.M. Meyer-Viol. Logica voor informatica, derde editie Pearson Education, 2003.
A complete list of literature will be in the lecture notes and on the course homepage.
Signing up for classes and exams
In MyTimetable kun je alle vak- en opleidingsroosters vinden, waarmee jij je persoonlijke rooster kunt samenstellen. Onderwijsactiviteiten waarvoor je in uSis staat ingeschreven, worden automatisch in je rooster getoond. Daarnaast kun je My Timetable gemakkelijk koppelen aan een agenda-app op je telefoon en worden roosterwijzigingen automatisch in je agenda doorgevoerd; bovendien ontvang je desgewenst per e-mail een notificatie van de wijziging.
Voor meer informatie over Brightspace kun je op deze link klikken om de handleidingen van de universiteit te bekijken. Bij overige vragen of problemen kan contact opgenomen worden met de helpdesk van de universiteit Leiden.
Onderwijscoördinator Informatica, Riet Derogee