COL703 – Logic for Computer Science

Logicians will often tell you that the primary raison d'être of logic is to systematically evaluate arguments for deductive validity, or something equally abstruse along those lines. So why should you, a computer scientist, bother with logic at all? Because, as anyone who has ever written a program beyond "Hello, world!" knows, writing code is hard. Writing good code is even harder, and this starts even before we have written any code at all! Are you sure that what you think you want is really what you want? Will your code actually work? How reasonable are the assumptions you have made along the way? These are questions that logic can help you think about in a systematic way.

The objective of this course is to learn fundamental ideas that help us create abstract models of systems in the real world, so we can then ensure that they behave as they should. This course will essentially cover concepts related to how to model complex systems abstractly while making good choices, as well as how to reason about these systems automatically, with a view to formal verification.

This fundamental material covered in this course is fairly abstract and theoretical, and will therefore require some mathematical acumen -- students should, at the very least, be able to write and understand rigorous formal proofs, especially those involving various kinds of induction. There will also be some programming involved to implement various concepts. You should have taken at least one of the following courses (or equivalents thereof):

• COL106 (Data Structures & Algorithms).

• COL202 (Discrete Mathematical Structures)

• Minor: 20%. No re-minor will be conducted. If you miss the minor for a medical reason (with appropriate documentation produced within one week of the minor), the major marks will be scaled up accordingly.

• Major: 40%. The syllabus for the major exam will include everything covered in the course.

• Quizzes: 15–20%. There will be some surprise quizzes conducted in class on various days during the semester. Best n-1 out of n will be considered. Absence in a quiz is directly marked 0. No make-up quizzes will be conducted.

• Practicals: 20%. Described in the first lecture.

• In-class participation, attendance etc: 0–5%.

• Best example(s) of real-world situations modelled in logic: 0–5% Bonus.

Audit pass needs at least a B- overall, including at least 10% out of the 15–20% earmarked for quizzes.

Deviation of any sort from the IIT Delhi honour code (copying, plagiarism, collaborating on gradable items where explicitly disallowed etc. – see here for more examples) will result in some manner of grade docking (potentially as bad as a summary fail), and potentially further disciplinary action.

We will follow notes presented in class, for the most part, which will be uploaded here. Some external references for much of the course are listed below (caveat emptor: notation used in these notes/books might significantly differ from the ones used in class).

• Introduction to Formal Logic, by Peter Smith

• Formal Logic: Its Scope and Limits, by Richard C. Jeffrey (also available in the IIT library)

• Hyper-notes for Logic in Computer Science, by Prof. S. Arun-Kumar

• Software Foundations, by various authors

• The Hitchhiker's Guide to Logical Verification, by various authors