CS 253 F: Introduction to Logic For Computer Science

This page gives information about the course ``CS 253 F: Introduction to Logic For Computer Science'' taught by the Department of Computer Science and Engineering at the Indian Institute of Technology, Delhi

Also available are the following (at least from within IITD):

HOT NEWS

See Minor 1 solutions.
See sample programs.

Overview

CS 253 F: Introduction to Logic For Computer Science is an introductory course in Symbolic Logic and its applications in computer science. It is intended for Second Year (sophomore) B Tech students, and is a compulsory course for Computer Science majors.

Objectives

Logic has been called "the calculus of computer science". The argument is that logic plays a fundamental role in computer science, similar to that played by calculus in the physical sciences and traditional engineering disciplines. Indeed, logic plays an important role in areas of Computer Science as disparate as architecture (logic gates), software engineering (specification and verification), programming languages (semantics, logic programming), databases (relational algebra and SQL), artificial intelligence (automatic theorem proving), algorithms (complexity and expressiveness), and theory of computation (general notions of computability). (Lifted from Moshe Vardi).

The objective of the course will be to introduce the main notions of mathematical logic: logical notations (syntax) and how to assign meaning to them (semantics). We will motivate some uses for mathematical logic in the field of computer science. We will then study formal frameworks (in the sense of being rigorous as well as in the sense of manipulating "form") for constructing logical arguments (proof theory), studying in particular some deductive systems for propositional and first-order logic. Naturally, we will be concerned with the correctness and completeness of these deductive systems, as well as with the algorithmics.

At the end of the course, I expect every student to know about Propositional and First-order Logic, and how logic may be used in specifying properties. I also expect them to know how to do a proof by induction, and some important meta-theorems about deduction systems.

Course Description

The (new!) Courses of Study booklet has this to say:

CS 253 N: Introduction to Logic For Computer Science

4 Credits: 2-1-2 (2 Lectures a week, one tutorial, two practical hours)
Review of the principle of mathematical induction; the principle of structural induction; review of Boolean algebras; Syntax of propositional formulas; Truth and the semantics of propositional logic; Notions of satisfiability, validity, inconsistency; Deduction systems for propositional logic; Completeness of a deductive system; First order logic; Proof theory for FOL; Introduction to model theory; Completeness and compactness theorems; First order theories. Programming exercises will include representation and evaluation; conversion to normal-forms; tautology checking; proof normalization; resolution; unification; Skolemization; conversion to Horn-clauses; binary-decision diagrams.

Prerequisites

Introductory programming courses (CS110N/CS120N) are the explicit pre-requisites. In addition, to do this course, you should not be afraid of formal mathematics, and should have the ability to think rigorously and program intelligently.

Staff

Teaching Assistants: O

Textbooks

I recommend the following text for this course (it is inexpensive, available and will cover about half the material in the course).
• The Essence of Logic. John Kelly. Prentice-Hall International, 1997. ISBN 81-203-1190-6. (Indian Edition Rs 75/-).
That said, I will not follow any single text book in this course --- for two reasons: (1) I would like to cover the material in a different way; (2) I do not believe it is my job to parrot what appears in a text book. However, I strongly suggest you read the books I recommend to complement the material I discuss in class. I may periodically ask you to read chapters from the texts, and will not hesitate to base assignments and exam questions on that material. Some useful books for learning about logic are:
• Logic for Computer Science Steve Reeves and Michael Clarke. Addison-Wesley, 1990. ISBN: 0-201-41643-3
• Logic for Computer Science. Jean H. Gallier. Harper and Row, New York, 1986.
• First-Order Logic and Automated Theorem Proving. Melvin Fitting. Springer Verlag, Berlin, 1990.
• A Mathematical Introduction to Logic. Herbert B. Enderton. Academic Press, New York, 1972.
• Natural Deduction (A Proof-theoretical study). Dag Prawitz. Almqvist and Wiskell, 1965.
For entertainment, you should read Raymond Smullyan's popular books.

ML-specific reference material (may not be affordable/available in a shop):

1. ML for the Working Programmer by L.C. Paulson, Cambridge University Press.
2. Online SML Tutorial by Bob Harper at CMU.

I will also try to distribute some reading material (but no promises).

Syllabus

I'm going to teach this course a bit differently this time. A list of topics is:
1. Sets and Functions

Resources

• Computing Platform: By now, you ought to have got an account on a machine running in Linux, in the hallowed precincts of the department's Intel or MC Labs. If you don't have an Intel account or can't get one for some reason, you should immediately get an account on the Computer Centre's machine ccsun50 (a Sun) running Solaris (a version of UNIX). I'm going to assume you know your way around in a Unix environment. Here's a list of tools you are likely to use.
• Editors: The editor I prefer is emacs because it provides a customisable programming environment. I get to see my ML code in all its wonderful colours and have a nifty ML mode. For some reason, students here like to use a mere editor called pico and hackers like a beast called vi.
• Language processors: The Standard ML interpreter can be invoked by typing sml at the UNIX prompt.
• Browsers: You may use other browsers such as Netscape Navigator or Microsoft Explorer. You are responsible for learning how to use a browser, and please be aware that browsing is a highly addictive activity.
• Libraries: Believe it or not, there are resources called books. The main library houses many such thingies. You should visit there some time and check them books out. The department also has a small library, which has a few books, mainly research material.

Schedule and Classrooms:

B slot in the time table.

Lectures in VI-301. A room that I detest.
 Monday 09:00-9:55 Wednesday 08:00-8:55 This slot will be used only for make-up classes. Friday 09:00-09:55

Tutorials in room 301.   Mondays and Thursdays, 14:00-14:55.

Make-up lectures, quiz hour (when announced)
Wednesday 08:00 - 09:55

Exam Schedule:
 Minor I August 21, 2000 08:00-09:00 WS 101 (Gp 4) WS 205 (Gps 1-3) Minor II October 5, 2000 08:00-09:00 WS 101 (Gp 4) WS 205 (Gps 1-3) Major

Marks:

 Minors 20% each Major 35% Assignments and Homework 20% Other Assessment 5%

As per the Institute regulations, an ``A'' grade will be awarded only over 80% and no student with less than 30% will be given a passing grade.

An ``I'' grade can only be awarded only in the case of a serious illness during the major exam. A make-up exam will be scheduled at the earliest, and the ``I'' grade will be converted as soon as possible. There will be no make-up tests for the minors.

Grades may be drastically lowered if the student fails to comply with the attendance requirements, or is dishonest.

Other policies:

• Attendance: The institute attendance requirements are quite clear. No student with less than 75% attendance can be awarded a passing grade. Please read institute attendance requirements and comply. Note that the minimum 75% requirement accounts for time lost due to illness.
• Illness: In sickness or ill-health, the course instructor must be intimated at the earliest, and a Medical Certificate from the Institute Sick Bay, or from a doctor from an Institute-recognised hospital covering the period of illness must be furnished at the earliest. Only in the case of serious illnesses will I consider giving an extension on assignments or a make-up test.
• Make-up Tests: Make-up tests (major exams only) will be given only when the student furnishes valid documentation of illness for a period including the day of the exam.
• Late policy: Normally, I will not consider any assignments turned in late. In cases of illness I may consider giving an extension, provided the student informs me as soon as possible. an extension, provided the student informs me as soon as possible.
• Dishonesty: Please read carefully the institute's regulations on dishonesty. Any instance of blatant academic dishonesty will result in my recommendation of the award of an 'F' grade. (I have awared several F grades for this very reason, so don't take this lightly). Minor transgressions, including faking attendance, will result at least in the lowering of a letter grade.

Sanjiva Prasad / Dept. Computer Science and Engineering / IIT Delhi / Hauz Khas/ New Delhi 110016 / sanjiva@cse.iitd.ernet.in