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 highlevel 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.
kCNF 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
HornSAT 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
quantifierfree fragment of predicate
logic 
Feb 29  Equality as a special binary predicate,
quantifierfree fragment of predicate
logic with equality. Natural deduction
rules for introducing and eliminating
equality in proofs. Illustration of
interesting formulas in quantifierfree
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 quantifierfree 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
