CS206: Formal Methods in Computer Science
(Spring 2008)


Announcements


Teaching Staff

Instructor Supratik Chakraborty
Friendly TAs Kaustubh Nimkar Kedar Joglekar Abhisekh Sankaran

Hours

What When Where
Lectures
Wed 9.30-11.00
Fri 9.30-11.00
Room A1, Maths Bldg.
Tutorials
Thurs 10.30-11.30
Room A1, Maths Bldg.
Office hour
Tues 17:30-18:30
CFDVS Lab 1 (Maths basement)
(by prior email appointment)

Lecture/Tutorial Reschedules

Lecture/tutorial on Rescheduled to
Fri Jan 11 (lecture)
Fri Jan 18 (8.30-9.30)
Wed Jan 16 (lecture)
Tue Jan 22 (9.30-10.30)
Thurs Jan 17 (tutorial)
Wed Jan 16 (9.30-11.00)
Fri Jan 25 (lecture)
Thurs Jan 24 (14.45-16.15)
Thurs Jan 31 (tutorial)
Wed Jan 30 (9.30-11.00)
Wed Jan 30 (lecture)
Thurs Jan 31 (10.30-11.30)

Grading

Midterm 30%
Endterm 50%
Homeworks and quizzes 20%

Important points ...

  • All exams are open book and notes.
  • Homeworks are due in class one week after they are given.
    The problems are meant to test your understanding of the subject and your creativity. Late turn-ins will be penalized.
  • Mutual discussion on assignments and practice questions is encouraged. However, copying solutions from others will be severely penalized.
  • There is zero tolerance for dishonest means like copying solutions from others.
    Anybody found indulging in such activities will be very severely penalized (including FF/FR grade). The onus will be on the supposed offender to prove his/her innocence.

Reading Material

  • Logic in Computer Science: Modeling and Reasoning about Systems by Michael Huth and Mark Ryan,   paperback edition published by Cambridge University Press.
  • Lecture notes.

References for the more interested ...

  • A note on checking satisfiability of 2-CNF formulae in propositional logic.
  • A nice online resource centre on Foundations of Mathematics.
  • Formal Methods educational resources from the world-wide web Formal Methods page.
  • Original paper on the DPLL procedure: A machine program for theorem-proving by M. Davis, G. Logemann and D. Loveland, in Communications of the ACM, Volume 5(7), July 1962, pages: 394-397. Downloadable from ACM Portal if you are accessing from IITB.
  • A wonderful tutorial on propositional satisfiability and beyond was presented by Prof. Roberto Sebastiani in CADE 2003. The original tutorial slides are no longer accessible from Prof. Sebastiani's webpage, but a google search using keywords "sebastiani propositional satisfiability" may fetch you the slides in PDF.
  • Natarajan Shankar's notes for his Fall 2003 course on Little Engines of Proof at Stanford University. Check the slides on Davis-Putnam and Stålmarck's methods if you are interested. You must of course familiarize yourself with the notation by looking at a few prior slides on the same website.
  • A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula by G. Stålmarck , U.S. Patent No. 5 276 897, European Patent No. 0403 454. You can search the patent websites (e.g. US Patent Office ) to download these patents.
  • Prover Technologies , the company that thrives on logic and proof systems (Stålmarck's patented procedure for determining propositional logic theorems is used in Prover' s tools).
  • A tutorial on Stålmarck's proof procedure for propositional logic by M. Sheeran, G. Stålmarck, Proceedings of the 2nd Intl. Conf. on Formal Methods in Computer-Aided Design, FMCAD'98, Palo Alto, CA, USA, 4--6 Nov 1998. Currently downloadable from citeseer . A journal version of this paper appeared in Formal Methods in System Design, Vol. 16, No. 1, Jan 2000. Formal Methods in System Design is published by Springer.
  • SATLive! All the latest happening on the satisfiability problem. You can check out the "10 most visited links" on this webpage to find out about several public domain SAT solvers, like zChaff from Princeton University.
  • SAT Research at Princeton: Contains a repository of some interesting papers describing how modern SAT solvers are engineered.
  • A good set of slides prepared by Prof. S. Ramesh on material relevant to this course. Look at slides 59-113 for First Order Logic.
  • Another good set of lecture notes on Introduction to Logic by Prof. Stanley N. Murris from University of Waterloo.

Homeworks, Exams, Tutorials ... all the fun part!

Questions from earlier years' course home pages 2005 , 2006 , 2007
Tutorial 1 Jan 10
Tutorial 2 Jan 16
Tutorial 3 Jan 24
Tutorial 4 Jan 30
Tutorial 5 Feb 7
Tutorial 6 Feb 14
Tutorial 7 Feb 28
Tutorial 8 Mar 13
Tutorial 9 Mar 18
Tutorial 10 Mar 27
Quiz 1 [ PDF ] Feb 1 (10.00-11.00)
Compensation Quiz 1 [ PDF ] Feb 8 (8.30-9.30)
Homework 1 [ PDF ] Due by Feb 13
Midsem exam [ PDF ] Feb 21
Quiz 2 [ PDF ] Mar 19 (9.30-11.00)
Homework 2 [ PDF ] Due by April 1

Lecture Schedule

Date Topics details
Jan 2 Introduction and Logistics. Brushing up the basics of propositional logic: syntax and semantics.
Jan 3 Semantics of propositional logic. Introductory notion of a proof, notation and terminology used in natural deduction proofs, simple natural deduction proof rules for propositional logic
Jan 4 More natural deduction proof rules for propositional logic, simple proofs using a restricted set of proof rules, multiple proofs of the same facts.
Jan 9 Discussion on a complete set of natural deduction proof rules for propositional logic, derived rules, examples of proofs and illustrations.
Jan 11 No lecture. Compensation lecture on Fri, Jan 18
Jan 16 No lecture. Tutorial session shifted from Thurs, Jan 17. Compensation lecture on Tues, Jan 22
Jan 18
(regular +
compensation
lecture)
Using propositional logic to encode constraints from diverse problems: Sudoku puzzle solving, finding cycles in finite graphs. Relation between a solution of the original problem and a satisfying assignment of the corresponding propositional logic formula
Jan 22
(compensation
lecture)
More on encoding constraints using propositional logic. Introductory discussion on finding satisfying assignments of a given propositional logic formula. Proving unsatisfiability through natural deduction proofs.
Jan 23 Notions of satisfiability of propositional formulae, syntactic and semantic entailment; brief discussion on soundness and completeness of natural deduction proof system for propositional logic. Towards decision procedures for propositional logic: introduction to Binary Decision Diagrams (BDDs)
Jan 24 Reduced Ordered Binary Decision Diagrams (ROBDDs): Shannon's expansion, definitions, examples, discussion. Dependence of structure of ROBDD on variable order. Canonicity of ROBDDs for a given variable order. Constructing an ROBDD for a given propositional logic formula and given variable order. Understanding some high-level intuition behind "good" variable orders.
Jan 31 Intuition behind combining ROBDDs for subformulae to obtain ROBDDs for larger formulae: potential problems and solutions. Overview of Apply and Reduce algorithms for ROBDDs. Elaboration on Reduce algorithm.
Feb 1 Review of Reduce algorithm and discussion on Apply algorithm for ROBDDs. Use of dynamic programming and memoization in constructing ROBDDs, complexity of above algorithms.
Feb 6 Notions of equisatisfiability and equivalidity. Deriving an equisatisfiable formula in a special form (conjunctive normal form) from an arbitrary propositional logic formula in linear time.
Feb 8 Normal forms for propositional logic: CNF, DNF. Discussion on and distinction between semantic equivalence, equisatisfiability and equivalidity of formulae. Reducing one class of problems to another, and getting a feel of which problems are hard, based on the knowledge that satisfiability checking for propositional logic formulae in CNF is hard.
Feb 13 Review of normal forms, and notions of equisatisfiability and equivalidity. k-CNF formulae and satisfiability solving for propositional logic. DPLL algorithm, and its variants. Introduction to Horn formulae.
Feb 15 Horn formulae and satisfiability checking. Comparison of DPLL with Horn-SAT checking algorithm. Discussion of some heuristics used for choosing splitting variables in DPLL: Boolean Constraint Propagation and implication graphs.
Feb 27 Introduction to Predicate Logic: motivation for using predicates and functions, syntax and semantics of quantifier-free fragment of predicate logic
Feb 29 Equality as a special binary predicate, quantifier-free fragment of predicate logic with equality. Natural deduction rules for introducing and eliminating equality in proofs. Illustration of interesting formulas in quantifier-free fragment of predicate logic with equality.
Mar 5 Notion of a model and satisfiability of predicate logic formulae. Discussion on checking satisfiability of formulae in the quantifier-free fragment of predicate logic, with and without equality as a special predicate. Need for quantifiers, and introduction to universal and existential quantifiers.
Mar 7 More about quantifiers. Bound and free variables, renaming of bound variables. Substituting a term for a free variable in a formulae containing bound variables. Natural deduction rules for proofs involving quantifiers: illustration with examples.
Mar 12 Quantifier equivalences and relations between different quantified formulae. Natural deduction proofs for these relations, intuition behind these relations.
Mar 14 Soundness and completeness of natural deduction proof system for predicate logic (completeness discussed without proof). Inadequacy of a complete proof system for algorithmically deciding whether a predicate logic formula is satisfiable. Need for an incomplete decision procedure for predicate logic, Preliminary discussion on uncomputability.
Mar 19 Quiz 2
Mar 26 Discussion and illustration of the concept of uncomputability. Satisfiability checking of predicate logic formulae being undecidable. Introduction to Compactness Theorem.
Mar 28 Discussion on Compactness Theorem, sketch of proof, some interesting consequences of Compactness Theorem