| Date || Topics details |
| Jan 2 || Introduction and Logistics. Brushing up the
basics of propositional logic: syntax and
| 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 |
| 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 |
| 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,
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
| Feb 6 || Notions of equisatisfiability and equivalidity.
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
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
| 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
| 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
| 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
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