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
General information about the course is available under the following
Course Description |
The course is being taught in the Fall Semester of year 2000 by
Prasad. Information about this course offering is available under the
Administrative Information and Grading Policy
Also available are the following (at least from within IITD):
See Minor 1 solutions.
See sample programs.
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.
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
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.
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
Dr Sanjiva Prasad
I recommend the following text for this course (it is inexpensive,
and will cover about half the material in the course).
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:
- The Essence of Logic. John Kelly. Prentice-Hall
International, 1997. ISBN 81-203-1190-6.
(Indian Edition Rs 75/-).
For entertainment, you should read Raymond Smullyan's popular books.
- Logic for Computer Science
Steve Reeves and Michael Clarke. Addison-Wesley, 1990.
- 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
ML for the Working Programmer by L.C. Paulson, Cambridge University
Online SML Tutorial
by Bob Harper at CMU.
I will also try to distribute some reading
material (but no promises).
I'm going to teach this course a bit differently this time. A list
of topics is:
- Sets and Functions
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
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
called pico and hackers like a beast called vi.
The Standard ML interpreter can be invoked by typing sml
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.
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.
|| This slot will be used only for make-up classes.
Tutorials in room 301.   Mondays and Thursdays,
Laboratory hours at your convenience
Make-up lectures, quiz hour (when announced)
Wednesday 08:00 - 09:55
|| August 21, 2000
||WS 101 (Gp 4)
WS 205 (Gps 1-3)
|| October 5, 2000
||WS 101 (Gp 4)
WS 205 (Gps 1-3)
|Assignments and Homework
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
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
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
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
/ Dept. Computer Science and Engineering / IIT Delhi / Hauz Khas/ New Delhi
110016 / firstname.lastname@example.org