Admission requirements
Not applicable.
Description
Logic is both the origin of computer science and at its very foundation. Digital computers work with logic gates to manipulate bits, but the connection between computer science and logic goes much deeper than that. The history of logic is complex and begins with the philosophy and debates of ancient Greece, India and China, as the study of the relations of propositions and arguments. Motivated by the ambiguity of human language, mathematics of the late 19th century started to develop logic as a field in its own right with the hope of finding a universal language and absolutely correct foundation that would allow the formalisation of all mathematical proofs. This hope was shattered by Gödel's incompleteness and Church's undecidability theorems. But these results required a formal definitions of computation, which lead to the theory of computation that we know today. The boundary between logic and computer science is blurred and insights in logic lead to new methods of computation or visa versa.
In this course, you will learn what formal logic is and about its relationship to computer science. In particular, we will study propositional and first-order logic, including proof systems, algorithms, limitations and the relation to computation.
Course objectives
The course gives an introduction to mathematical logic and its computational aspects. Specifically, the course will enable you to
know how the syntax of propositional logic (PL) and first-order predicate logic (FOL) is formed;
formalise propositions in PL and FOL;
carry out syntactic operations on formulas through iteration (e.g., computing free variables);
rename variables and carry out substitution in FOL;
give semantics to formulas in PL and FOL, and decide semantic properties of formulas;
prove PL and FOL sequents in natural deduction;
compute conjunctive normal forms of PL formulas;
formalise knowledge bases as Horn clause theories in PL and FOL, and carry out deduction via algorithms (in the case of PL) or via uniform proofs (in case of FOL) in such theories;
formalise and reason about uniqueness and other properties involving the identity of objects in FOL with equality
recognise and compute with primitive recursive functions;
understand the various limitations of FOL in terms of expressiveness, completeness and decidability
Timetable
The most updated version of the timetables can be found on the students' website:
You will find the timetables for all courses and degree programmes of Leiden University in the tool MyTimetable (login). Any teaching activities that you have sucessfully registered for in MyStudymap will automatically be displayed in MyTimetable. Any timetables that you add manually, will be saved and automatically displayed the next time you sign in.
MyTimetable allows you to integrate your timetable with your calendar apps such as Outlook, Google Calendar, Apple Calendar and other calendar apps on your smartphone. Any timetable changes will be automatically synced with your calendar. If you wish, you can also receive an email notification of the change. You can turn notifications on in ‘Settings’ (after login).
For more information, watch the video or go the the 'help-page' in MyTimetable. Pleas note: Joint Degree students Leiden/Delft have to merge their two different timetables into one. This video explains how to do this.
Mode of instruction
Weekly lectures, complemented with lecture notes and some in-depth video tutorials.
Exercise classes, during which students can work on and ask questions about the weekly assignments
and homework.
Assessment method
Students will be evaluated on the basis of a written examination complemented with homework
assignments.
Examination is worth 70% of the final grade.
The remaining 30% is from the average grade of homework assignments, where the worst two
homework grades will be dropped.
At least half of the homework assignments have to be completed (empty or non-sense submissions do
not count).
A retake is offered for the exam.
The course is passed with a minimum of 5.5 as final grade.
This means that the homework grade can compensate the exam grade.
Reading list
The main source of information are the lectures and 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 can be found in the lecture notes.
Registration
From the academic year 2022-2023 on every student has to register for courses with the new enrollment tool MyStudymap. There are two registration periods per year: registration for the fall semester opens in July and registration for the spring semester opens in December. Please see this page for more information. An exemption is the fall semester for 1st year bachelor students, the student administration will enroll this group.
Please note that it is compulsory to both preregister and confirm your participation for every exam and retake. Not being registered for a course means that you are not allowed to participate in the final exam of the course. Confirming your exam participation is possible until ten days before the exam.
Extensive FAQ on MyStudymap can be found here.
Contact
Course email, 2223-S2 Introduction to Logic
Discord server (link will be provided on Brightspace)
Remarks
Website: Introduction to Logic 2023