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
|