CS 253 F: Introduction to Logic For Computer Science

General information about the course is available under the following headings:

 Overview | Objectives | Course Description | Prerequisites

 Staff | Textbooks | Syllabus | Resources | Administrative Information and Grading Policy

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

• e-mail to the course instructor.
• Assignments.
• Tests and quizzes from this semester
• Some sample programs
• Student roll lists and markssorted by group and then entry.
• On-line feedback form

HOT NEWS

Overview

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

CS 253 N: Introduction to Logic For Computer Science

4 Credits: 2-1-2 (2 Lectures a week, one tutorial, two practical hours)

Prerequisites

Staff

Textbooks

• The Essence of Logic. John Kelly. Prentice-Hall International, 1997. ISBN 81-203-1190-6. (Indian Edition Rs 75/-).

• 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.

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

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.

Administrative Information

Schedule and Classrooms:

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.

Laboratory hours at your convenience

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:

Grading Policy:

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.