| Date | Topics details |
|---|
| Jul 24 | Course overview, prerequisites and logistics.
Quick introduction to propositional logic.
Proofs as mathematical objects with reference
to propositional logic |
| Jul 28 | No class. Compensation class on Aug 5 |
| Jul 31 | More on proofs, with examples of proofs
in propositional logic. Notion of a theorem.
Semantics of propositional logic, notions
of assignments, satisfiability, tautology.
Completeness theorem of propositional logic.
|
| Aug 4 | More discussion on completeness theorem for
propositional logic. Normal forms.
Notions of satisfiability
and consistency and their equivalence.
Compactness theorem for propositional logic.
|
| Aug 5 | More on compactness theorem, consistency and
satisfiability. Ground resolution as a sound
and complete deductive system for propositional
logic. Introductory concepts in first-order
logic. Using compactness theorem of propositional
logic to reason about unsatisfiability of
certain classes of formulae in first-order logic.
|
| Aug 7 | No class due to Convocation.
Compensation class on Aug 20. |
| Aug 11 | Substitution and renaming of bound
variables in first-order logic formulae.
Axioms and inference rules for first-order logic.
Lifting propositional proof skeletons
to first-order logic through substitution.
Semantics of first-order logic:
interpretations, models, notions of
tautology/validity and satisfiability |
| Aug 14 | No class.
Compensation class on Aug 27. |
| Aug 18 | No class.
Compensation class on Sept 5. |
| Aug 20 | More on semantics of first-order logic and
interpretations (structures). Prenex and
Skolem normal forms: notions of Skolem
functions and constants. Herbrand structures
and their importance in checking satisfiability
of first-order logic formulae. |
| Aug 21 | Herbrand structures and Herbrand's theorem on
unsatisfiability of first-order logic formulae.
Existence of countable models for satisfiable
first-order formulae. Lowenheim's theorem.
Equivalence of the notions of consistency and
satisfiability in first-order logic. Towards
a proof of the generalized completeness theorem
in first-order logic. |
| Aug 25 | Proof outlines of generalized completeness
theorem of first-order logic, Godel's
completeness theorem, Lowenheim-Skolem
theorem and compactness theorem of first-order
logic. An interesting graph-theoretic
application of the compactness theorem.
|
| Aug 27 | A special formulation FO(=) of first-order logic:
having equality as an interpretted predicate.
Equality axioms and consequences. Properties of
the equality predicate.
|
| Aug 28 | More discussion on FO(=). Reducing sat
problem of FO(=) to that of first-order
logic without equality. Completeness,
compactness and consistency results of FO(=)
being similar to those of first-order logic
without equality. Introduction to
resolution in first-order logic, notion of
unification. |
| Sep 1 | Resolution in first-order logic and adequacy
for checking unsatisfiability. Unification,
most general unifiers and an algorithm for
calculating a most general unifier. |
| Sep 4 | Proof of correctness of unification algorithm
and why it always computes a most general
unifier. Craig's interpolation theorem:
proof in propositional logic, intuition behind
proof in first order logic. Some applications
in different areas. |
| Sep 5 | Proof of Craig's interpolation theorem in first
order logic, some applications of interpolants.
Bernays-Schonfinkel-Ramsey class of first order
logic formulas, and small model property of this
class. Revisiting Herbrand models, and first order
logic formulae with equality. |
| Sep 8 | Introduction to partially ordered sets.
Definitions of chains, antichains, order-isomorphism.
Covering relation of a partial order,
Hasse diagrams and their utility in visualizing
partial orders. |
| Sep 11 | Maps between partial orders: order preserving
maps, order embeddings and order isomorphisms.
Examples of orders isomorphic to the Boolean
lattice. Constructing complex partial orders
through cross-product of simpler partial orders:
interpretation in Hasse diagrams.
|
Sep 15
Sep 18 | No classes: Midsem week |
| Sep 22 | Products, linear sums and disjoint unions of
partial orders, and their interpretation in
Hasse diagrams. Order ideals and filters,
the partial order of order ideals, and its
relation to the original partial order.
|
| Sep 25 | Partial order of order ideals (down sets)
and order filters (up sets), constructing
down (and up) sets of posets obtained by
combining smaller posets, counting
cardinalities of order ideals of finite
posets, anti-chains and order ideals,
duality of order ideals and order filters,
example problems from posets and order
ideals |
| Sep 29 | Lattices and complete lattices: introduction
and examples. Finite and infinite lattices
and some basic properties. Dual lattices,
duality of meet and join, basic results about
meet and join. The lattices of order ideals
and order filters.
|
| Oct 2 | No class: Gandhi Jayanti |
| Oct 6 | Lattice as an algebraic structure, connection
with lattice as an ordered set, sublattices and
examples, products of lattices, lattice homomorphisms.
|
| Oct 9 | Lattice homomorphisms, embeddings and isomorphisms.
Lattice ideals and filters.
|
| Oct 13 | No class: Maharashtra elections. Compensation
class on Oct 15. |
| Oct 15 | More on lattice ideals and filters, further characterizations
of complete lattices.
|
| Oct 16 | Some characterizations of complete lattices and
examples, Knaster-Tarski fixpoint theorem and some
applications, structure of the poset of
fixpoints of an order-preserving map on a
complete lattice.
|
| Oct 20 | Chain conditions (ACC and DCC). Posets with chain
conditions and their properties. Chain conditions
and complete lattices.
|
| Oct 23 | Join- and meet-irreducible elements, join-
and meet-dense subsets. Chain conditions
and join-dense and meet-dense sets.
|
| Oct 27 | Reconstructing lattices from the set of
join- and meet-irreducible elements.
Powerset lattices and lattice of downsets
of a poset, and the set of join- and
meet-irreducible sets of these lattices.
Isomorphism between a poset and the
set of join-irreducible elements of
the lattice of its down-closed sets.
Galois connections between posets.
|
| Oct 29 | More on Galois connections, examples of
application in abstract reachability
analysis. Modular and distributive
latices and their properties. The
M3-N5 theorem.
|
| Oct 30 | No class |
| Nov 3 | More on modular and distributive lattices:
sub-lattices, products, homomorphic images.
Notion of complements and Boolean lattices.
Properties of Boolean lattices.
Finite Boolean lattices and their relation
to powerset lattices.
|
| Nov 6 | Birkhoff's representation theorem for finite
distributive lattices and some applications,
atoms in a lattice, special role of atoms in
Boolean lattices, product of finite
distributive lattices and disjoint union
of their join-irreducible elements. |
| Nov 10 | Symbolic representation of finite sets and
finite graphs using propositional logic
formulae, encoding operations on graphs as
propositional logic operations, symbolic
breadth-first search (BFS) in a graph using
propositional operations, importance of SAT
solvers in bounded symbolic BFS. |
| Nov 13 | Using propositional SAT solving for bounded
search in finite graphs. Basic DPLL
algorithm for propositional SAT solving.
Encoding infinite graphs using
quantifier-free fragments of first-order
logic with interpretted predicates and
functions, illustration through example of
linear arithmetic on integers. Bounded
reachability in such inifinite graphs using
SAT solving for special quantifier-free
fragments of first-order logic. Using a
DPLL SAT solver and a linear program solver
to solve SAT problems in quantifier-free
fragment of linear arithmetic. Wrap-up of
course. |