CS208: Automata Theory and Logic
(Spring 2024)


Announcements

  • We will be using Piazza for all discussions in this course. If you have not received a welcome mail yet from Piazza for CS208, please signup here.
  • Doubt clearing session on Wed Mar 27, 6-7pm in SIC 301
  • Tutorial 6 on Wed Mar 27, 9-10.30 pm
  • Tutorial rooms, TA assignment and notes scribing responsibilities can be found here.
  • Please follow lecture notes scribing guidelines strictly.
  • Important announcements will be posted on this webpage, on Piazza and on Moodle. So please keep watching this space.

Teaching Staff

Instructor Supratik Chakraborty
Friendly TAs M. Adarsh Reddy, Ameya P. Deshmukh, Ameya V. Singh, Anish Y. Kulkarni, Anubhav Jana, Arpon Basu, Ashwin Abraham, Kartik P. Gokhale, Y. Koustubh Rao, Lakshya, Nilabha Saha, Parismita Das, Vishal A. Tapase

Hours

What When Where
Lectures
Mon 11:30 Tue 8:30 Thurs 9:30
LA 201, Lecture Hall Complex
Office hour
Wed 17:00-18:00
(by email appointment)
CC 314, New CC-CSE Bldg
Tutorials
Alternate Wed 21:00-22:00 (some sessions may spill a bit beyond 22:00)
CC-101, CC-103, CC-105 (New CC-CSE Bldg) and
SIC 201 (KReSIT Bldg)
Quiz
Wed, Feb 7 and Wed, Apr 3, 21:00-23:30
CC-101, CC-103, CC-105 (New CC-CSE Bldg) and
SIC 201 (KReSIT Bldg)

Grading

Midterm 25%
Endterm 40%
Homeworks 18%
Quizes 14%
Notes scribing 3%

Ground Rules

Textbooks


Online resources


Lecture notes scribing

Problems for solving

Homework, quiz and exam problems

WhenEvaluation typeDue bySolutions
Jan 12 Homework 1 Jan 19, 23:59 (on Moodle)Solutions
Jan 26 Homework 2 Feb 2, 23:59 (on Moodle)Solutions
Feb 7, 21:10 Quiz 1 Feb 7, 23:40Solutions
Feb 27, 8:30 Midsem exam Feb 27, 10:30  
Mar 15 Homework 3 Mar 24, 23:59 (on Moodle)  

Tutorial/Practice Problems

WhenProblems
Jan 10 Tutorial 1 with solutions
Jan 24 Tutorial 2 with solutions
Feb 6 Practice problem set 1 with solutions
Feb 14 Tutorial 3 with solutions
Feb 18 Practice problem set 2   Solutions provided by Navya, checked by instructor
Feb 21 Tutorial 4 with solutions
Feb 22 Practice problem set 3
Mar 13 Tutorial 5
Mar 27 Tutorial 6

Lecture Schedule

DateTopicsReadings, slides, etc.Scribed notes
Jan 4 Introduction, course logistics, understanding computation: the mechanism and calculus; role of logic and automata; how it helps to view some problems through lens of logic and others through lens of automata
Slides
None
Jan 8 Example time-table scheduling problem, and role of logic in modeling specifications; syntax and semantics of propositional logic; parse trees for propositional formulas
Slides,
Huth and Ryan: 1.1, 1.3. 1.4.1, 1.4.2
Consolidated scribed notes
Jan 9 More on semantics of propositional logic; satisfiable, unsatisfiable, valid formulas, semantic entailment and equivalence of formulas, equisatisfiability of formulas, using truth tables to check semantic relations and its obvious drawbck
Slides,
Huth and Ryan: 1.4.1, 1.5.1
Jan 11 Encoding time-tabling problem as propositional logic formula; impracticality of using explicit truth tables and need for proof rules; natural deduction proof rules: "And" and "Or" introduction and elimination rules and their soundness
Huth and Ryan: 1.2
Jan 15 "Implication" and "Negation" introduction and elimination rules, "Bot" elimination and "Double negation" elimination rules and their soundness; use of sub-proofs with assumptions; example proofs using the small repertoire of proof rules
Huth and Ryan: 1.2
Jan 16 Examples of proofs using natural deduction proof rules with help of online tool, notion of syntactic entailment, valid formulas and their syntactic entailment from the empty set of premises, soundness of natural deduction proof system for propositional logic
Huth and Ryan: 1.2, 1.4: 1.4.3
Jan 18 Completeness of natural deduction proof system for propositional logic: proof by mimicing truth table rows in proofs
Huth and Ryan: 1.4: 1.4.4
Jan 23 Completing the argument for completeness of natural deduction proof rules, illustration with example; semantic redundancy of bi-implication and implication operators, sufficiency of {conjunction, negation} or {disjunction, negation} as propositional operators; distributive laws and De Morgan's rules for transforming propositional formulas to semantically equivalent ones; negation normal form (NNF) and conjunctive normal form (CNF) of propositional formulas
Huth and Ryan: 1.4: 1.4.4, 1.5: 1.5.1, 1.5.2
Jan 25 Normal forms of propositional formulas: NNF, CNF, DNF; linear-time algorithm for converting an arbitrary propositional logic formula to NNF; worst-case exponential-time complexity for conversion to CNF/DNF; satisfiability and validity checking of CNF/DNF formulas; Tseitin encoding for obtaining an equisatisfiable CNF formula from an arbitrary propositional logic formula
Huth and Ryan: 1.5.1, 1.5.2
Jan 29 Advantages of Tseitin encoding; Horn clauses and Horn formulas, a polynomial-time algorithm for checking satisfiability of Horn formulas and for finding a satisfying assignment, lifting some of the intuition to general CNF formulas
Huth and Ryan: 1.5.3
Jan 30 Illustrating applicability of Horn satisfiability checking for a simple example; illustrating the difficulty of using Horn formulas in expressing that one of a variable and its complement must be true; DPLL algorithm for checking satisfiability of general CNF formulas
Huth and Ryan: 1.5.3,
DPLL wikipedia page
Feb 1 Understanding unit propagation, pure literal elimination, decision/split and backtrack steps in DPLL; illustrating effects of different choices in running DPLL on an illustrative example; discussion about complexity of DPLL, and how DPLL fares on Horn formulas
DPLL wikipedia page
Feb 5 Horn formulas and backtracking in DPLL; Resolution proof rule, notion of resolvent, soundness and completeness of resolution for checking unsatisfiability of CNF formulas
Slides on resolution from MIT OCW (see upto slide 37)
Feb 6 Propositional formulas as acceptors of 0-1 words, need for richer acceptance mechanisms. Notions of alphabet, (finite) words and languages. Some simple (un)countability factoids about languages. Deterministic finite automata (DFA): basic notion of states, transitions; simple illustrations
Hopcroft, Motwani, Ullman: 1.5, 2.1, 2.2
Feb 12 More on deterministic finite automata; introduction to non-deterministic finite automata (NFA) and acceptance of a word by an NFA; exponential succinctness of NFA compared to DFA
Hopcroft, Motwani, Ullman: 2.3.1, 2.3.2, 2.3.3, 2.3.4, 2.3.6
Feb 13 Formal notation for DFAs and NFAs, subset construction and expressive equivalence of NFAs and DFAs
Hopcroft, Motwani, Ullman: 2.3.5
Feb 14 Inductive proof of equivalence of NFAs and DFAs, efficiently checking if a string is accepted by NFA without constructing entire DFA; introduction to NFAs with ε-transitions
Hopcroft, Motwani, Ullman: 2.3.5, 2.3.6, 2.4, 2.5.1, 2.5.2
Feb 15 NFA with ε-transitions: ε-closure, expressive equivalence with NFA without ε-transitions, examples of NFAs with ε-transitions and their intuitive appeal
Hopcroft, Motwani, Ullman: 2.5.3, 2.5.4, 2.5.5
Feb 17 Regular expressions: syntax and semantics (languages represented by regular expressions), applications, examples of syntactically different expressions representing the same language
Hopcroft, Motwani, Ullman: 3.1, 3.3
Feb 19 Conversion of regular expressions to NFA with ε-transitions, conversion of NFAs without ε-transitions to regular expressions; decision problems for regular language: membership, emptiness, language equivalence, language containment; closure properties of regular languages: set complement, union, intersection
Hopcroft, Motwani, Ullman: 3.2, 4.3.1, 4.3.2, 4.3.3, 4.2.1
Coming soon
Feb 20 Further discussion on closure properties of regular languages: use of product automata and substitutions (substituting regular languages for letters -- a generalization of homomorphisms); Statement of pumping lemma
Hopcroft, Motwani, Ullman: 4.2.1, 4.2.2, 4.2.3, 4.2.4 (recommended, though not covered in lecture), 4.1.1
Coming soon
Mar 11 Further discussion on pumping lemma for regular languages; application of pumping lemma in proving non-regularity of languages; a few variants of pumping lemma for regular languages; non-regular languages that satisfy the pumping lemma
Hopcroft, Motwani, Ullman: 4.1.1, 4.1.2, 4.1.3 (recommended exercises)
Coming soon
Mar 11 (compensation) Minimizing count of states in DFA for a regular language; indistinguishability and distinguishability relation on states, simple algorithm for finding distinguishable (and hence also indistinguishable) states; state minimization algorithm that works by merging all indistinguishable states
Hopcroft, Motwani, Ullman: 4.4.1, 4.4.2, 4.4.3
Coming soon
Mar 12 Proof of minimality of DFA obtained after merging indistinguishable states in a given DFA; uniqueness of minimal DFA for a regular language; Nerode equivalence relation for a language; correspondence between states in minimal DFA obtained by state-minimization algorithm and Nerode equivalence classes for a regular language.
Hopcroft, Motwani, Ullman: 4.4.3, 4.4.4
Coming soon
Mar 12 (compensation) Minimality of DFA constructed from Nerode equivalence classes; Myhill-Nerode theorem and its importance in constructing DFA for regular languages, and to prove non-regularity of other languages. Towards accepting languages beyond regular: adding a stack to an NFA -- pushdown automata (PDA); example of non-regular language accepted by a PDA.
Myhill-Nerode theorem on Wikipedia, Hopcroft, Motwani, Ullman: 6.1.1, 6.1.2, 6.1.3, 6.1.4
Coming soon
Mar 14 Further examples of PDA recognizing a non-regular language by final state. Alternative notion of acceptance of a PDA by empty stack. Reduction of PDA acceptance by final state to PDA acceptance by empty stack
Hopcroft, Motwani, Ullman: 6.2.1, 6.2.2, 6.2.4
Coming soon
Mar 14 (compensation) Reduction of PDA acceptance by empty stack to PDA acceptance by final state; equivalence of acceptance by empty stack and final state; discussion on deterministic and non-deterministic PDAs and their differences. Understanding the structure of a context-free language by observing the build-up and emptying of the stack of a PDA.
Hopcroft, Motwani, Ullman: 6.2.3, 6.3.2 (introduction)
Coming soon
Mar 18 Recurrence relations between languages accepted by a given PDA starting from state q, with symbol X on top of stack, and emptying the stack while reaching state q. Language accepted by a PDA as being generated by a context-free grammar.
Hopcroft, Motwani, Ullman: 6.3.2, 5.1.1, 5.1.2, 5.1.3
Coming soon
Mar 19 More on CFGs and CFLs, parse trees and leftmost derivations, ambiguous grammars, constructing a PDA that accepts by empty stack from a CFG
Hopcroft, Motwani, Ullman: 5.1, 5.2, 5.4
Coming soon
Mar 21 Constructing a PDA from a CFG. Cleaning up CFGs: eliminating useless symbols, epsilon productions and unit productions, Chomsky-Normal Form grammars and their universality; Pumping Lemma for CFLs: use in shown certain languages are not context-free
Hopcroft, Motwani, Ullman: 6.3.1, 7.1, 7.2
Coming soon
Mar 26 Closure of CFLs under union and substitution, non-closure of CFLS under intersection and complementation. Turing Machines (TM): basic definitions, demo of TM runs, acceptance by halting, notions of computing functions and accepting languages
Hopcroft, Motwani, Ullman: 7.3, 8.2
Programmatic simulator for Turing Machines
Coming soon