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)

• Assignments: 20%. We will follow a graceful degradation policy: For every day that you use beyond the indicated deadline, you lose 20% of marks for that assignment -- if you submit anything later than 5 days past the deadline, it will not be evaluated.

• 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 at various points during the semester. Absence in a quiz is directly marked 0. No make-up quizzes will be conducted.

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

• Pedagogical experiment surveys: 0–5% Bonus.

• "A few of my favourite things": 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 summarily result in an F grade, or in case of audit, an NF, 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