meta data for this page
  •  

Cut-paste from FM minutes: http://www.cse.iitb.ac.in/~csfac/fac/csfac/fac/2012-02-29/

There are three parts in this proposal.

a) Syllabus for a new core course titled 'Logic for Program Correctness'
b) Deletion of some of the related topics from the course CS 208 - 'Automata Theory and Logic' and renaming that course 'Theory of Computation'
c) Dropping 2 other courses titled “Theory of Computation” - CS 319 and CS 331.

As suggested by DUGC, Supratik, Bharat and Om came together to decide the contents of a new core course on Logic. Krishna has also been on emails as she was not able to attend the meetings. It is proposed to replace IC 211 Experimentation and Measurement Lab ( 4 credits) with this new course ( 6 credits). As a result total credits in 3rd semester will be 35 which are comparable to that in 2nd ( 37 credits) and 4th (35 credits) semesters. Total credits for BTech will increase to 254. Please send your comments to me/dugc. Thanks, - Om

The details follow:

I Title of the Course Logic for Computer Science i Credit Structure
L T P C
3 0 0 6
ii Prerequisite, if any - None

Syllabus: <html><pre> 1 Propositional logic: 

      1.1 Declarative sentences
      1.2 Natural deduction
          1.2.1 Rules for natural deduction
          1.2.2 Derived rules
          1.2.3 Provable equivalence
      1.3 Propositional logic as a formal language
      1.4 Semantics of propositional logic
          1.4.1 The meaning of logical connectives
          1.4.2 Soundness of propositional logic
          1.4.3 Completeness of propositional logic
      1.5 Normal forms
          1.5.1 Semantic equivalence, satisfiability and validity
          1.5.2 Conjunctive normal forms and validity
          1.5.3 Horn clauses and satisfiability
      1.6 SAT solvers

2 Predicate logic 

       2.1 Predicate logic as a formal language
          2.1.1 Terms
          2.1.2 Formulas
          2.1.3 Free and bound variables
          2.1.4 Substitution
      2.2 Proof theory of predicate logic
          2.2.1 Natural deduction rules
          2.2.2 Quantifier equivalences
      2.3 Semantics of predicate logic
          2.3.1 Models
          2.3.2 Semantic entailment
          2.3.3 The semantics of equality
      2.4 Undecidability of predicate logic: maybe just mention
      2.5 Expressiveness of predicate logic

3 Program Correctness 

      3.2 Notion of program correctness
          3.1.2 Hoare triples
          3.2.3 Partial and total correctness
          3.3.4 Program variables and logical variables
      3.2 Proof calculus for partial correctness
          4.3.1 Proof rules
          4.3.2 Proof tableaux
      3.3 Proof calculus for total correctness
      3.4 Programming by contract

</pre></html>

Time permitting, other possible applications and tools can be covered.

Textbook: Logic in Computer Science. Huth and Ryan. Cambridge University Press, 2004.

Once this course is introduced, CS 208 - Automata Theory and Logic can be renamed “Theory of Computation” and the following can be dropped from CS 208 syllabus:

“Propositional logic: Review and SAT solving, some puzzle solving, Predicate Logic: Syntax, semantics, quantifier equivalences, notion of undecidability of predicate logic.”

Note that the feedback from CS 208 instructors have been that above material is anyway not being covered in CS 208 due to lack of time.

The syllabus for revised CS 208 - Theory of Computation will be:

Current curriculum:

I Title of the Course Theory of Computation
i Credit Structure
L T P C
3 0 0 6
ii Prerequisite, if any Discrete Structures (CS 207)(for the student)

v Course content
Rudiments of formal languages. Finite state machines(DFA/NFA/epsilon NFAs), regular expressions. Properties of regular languages. My hill-Nerode Theorem. Non-regularity. Push down automata. Properties of context-free languages. Turing machines:Turing hypothesis, Turing computability, Nondeterministic, multi tape and other versions of Turing machines. Church's thesis, recursively enumerable sets and Turing computability. Universal Turing machines. Unsolvability, The halting problem, partial solvability, Turing enumerability, acceptability and decidability, unsolvable problems about Turing Machines. Post`s correspondence problem.

Texts/References:
1. Introduction to Automata Theory, Languages and Computation,
by John. E. Hopcroft, Rajeev Motwani, J. D. Ullman,
published by Pearson Education Asia, 2006.
2. Elements of the Theory of Computation, by H.R. Lewis and C.H.Papadimitrou,
published by Prentice Hall Inc, 1981.

Note that there are 2 other courses titled “Theory of Computation” - CS 319 and CS 331, which should be dropped.