| Date | Topics details |
|---|
| Jan 4, 5 | No class. Compensation classes on Jan 17
and Jan 24 |
| Jan 9 | Introduction to the course and logistics.
Some interesting problems that can be solved
by studying logic.
Introduction to Propositional Logic |
| Jan 11 | Propositional Logic: Syntax, examples,
formulas as trees. Semantics of propositional
logic: definitions and examples |
| Jan 12 | What we mean by a proof in this course;
Desirable features of a proof system.
Natural Deduction proof system for propositional
logic: explanation of notations, discussion
on rules for conjunction introduction and
elimination, disjunction introduction and elimination
and implication introduction. Illustration
of application of rules through simple examples.
|
| Jan 16 | More proof rules: implication elimination,
negation introduction and elimination,
double negation introduction and elimination,
elimination of "bot". Intuitive justification
for each rule. Simple proofs using these
rules as string transformation templates
|
| Jan 17 | Proofs in natural deduction: examples and
illustrations. Proving Law of Excluded
Middle (LEM) using the double negation
elimination rule and vice versa.
Discussion on the syntactic nature of a
proof; viewing a proof system as a string
transformation system |
| Jan 18 | Intuitive explanations and sketch of proofs of
soundness and completeness of natural deduction
for propositional logic. "Mimicking" truth
tables (semantic structures) in natural deduction
proofs using LEM repeatedly |
| Jan 19 | Notions of semantic and syntactic entailment.
More discussion on soundness and completeness
of natural deduction for propositional logic.
Difficulty of proving that something cannot
be proven by natural deduction; need for
semantic reasoning and algorithms for checking
satisfiability of formulae |
| Jan 23 | Encoding graph reachability as a propositional
logic implication. Using natural deduction
proof rules to prove graph reachability.
Difficulty of showing non-reachability using
natural deduction; role of satisfiability
solvers. Using satisfiability solvers to
disprove semantic entailment, thereby showing
the absence of a natural deduction proof.
A computer program for generating proofs of
valid sequents.
|
Jan 24
(2 lectures) | Normal forms of propositional logic
formulae: negation normal form (NNF),
disjunctive normal form (DNF) and
conjunctive normal form (CNF).
Notions of validity and satisfiability,
and their duality.
Ease of satisfiability checking on DNF
and of validity checking on CNF.
Exponential blowups in converting
arbitrary formulae to semantically
equivalent CNF/DNF formulae.
Notion of equisatisfiability, difference
from semantic equivalence.
Constructing equisatisfiable formula
linear in size to given to given
arbitrary formula. Importance of
3-CNF satisfiability.
|
| Jan 25 | Checking satisfiability of CNF formulae.
Implication graphs and Boolean Constraint
Propagation (BCP). Notions of unit and
pure literals in a CNF formula. Basic
DPLL algorithm with BCP for obtaining
a satisfying assignment of a CNF formula.
|
| Jan 26 | Republic Day
|
| Jan 30 | Muharram
|
| Feb 1 | Tutorial 2. Compensation class on
Wed Jan 24 |
| Feb 2 | Quiz 1
|
| Feb 6 | Finding all satisfying assignments of a
given CNF formula. Introduction to
Horn clauses, Horn formula and the
spirit of logic programming. Discussion
on why checking consistency/satisfiability
of Horn formulae are easier than checking
satisfiability of arbitrary CNF formulae.
|
| Feb 8 | A polynomial-time algorithm to check
satisfiability of Horn formulae; a
few simple extensions. Discussion
on a few other SAT solvers.
Need for a logic richer than propositional
logic. Introduction to predicate logic:
variables, predicates and functions.
|
| Feb 9 | Predicate logic: Syntax and semantics.
Free and bound variables. |
| Feb 13 | Semantics of predicate logic: more
discussion and examples. Domains
(universes) and interpretations
predicate and function symbols.
Propositional logic as a strict sublogic
of predicate logic, expressive power of
formulae with quantifiers.
|
| Feb 14 | Notion of models. Semantics of predicate
logic as dependent on underlying models.
Renaming of bound variables, substitution,
equality predicate. Introduction to
understanding the meaning of implications
in predicate logic. |
| Feb 15 | Clarification on substitution. Sequents
in predicate logic. Natural deduction
proof rules for predicate logic: rules
for propositional logic + rules for
equality introduction and elimination.
|
| Feb 19 | Mid-semester examination |
| Feb 27 | Natural deduction proof rules for
predicate logic: rules for introduction
and elimination of quantifiers.
Illustration of proofs in natural
deduction.
|
| Mar 1 | Quantifier equivalences in predicate
logic. Intuition behind equivalences
and formal proofs of equivalences in
natural deduction.
|
| Mar 2 | More on quantifier equivalences and
effects of permuting quantifiers.
Prenex Normal Forms of predicate logic
formulae. Skolem Normal Form: Role of
Skolem functions, minimizing the arity
of Skolem functions needed for
Skolemization.
|
| Mar 6 | More discussion on Skolem functions,
and Skolem Normal Form. Introduction
to a class of predicate logic formula
for which satisfiability checking is
decidable (computable): the
Bernays-Schonfinkel class, a simple
algorithm for checking satisfiability
of this class of sentences, and
illustrations
|
| Mar 8 | Introduction to the Compactness Theorem
of predicate logic. Sketch of proof of
theorem. Applications of the Compactness
Theorem to prove impossibility of
expressing certain properties of graphs
in predicate logic.
|
| Mar 9 | More discussion on the Compactness Theorem.
Example of a second order logic formula,
and how it can express something that is
not expressible in predicate/first-order
logic.
Introduction to Herbrand Universe and
Lowenheim-Skolem Theorem on existence of
countable models of satisfiable predicate
logic sentences. Introduction to Herbrand's
Theorem on unsatisfiability of predicate
logic sentences.
|
| Mar 13 | Ground terms and clauses.
More on Herbrand's Theorem on
unsatisfiablity of predicate logic
sentences using propositional
unsatisfiability of a finite
set of ground clauses. Illustration
of Herbrand's Theorem.
|
| Mar 15 | Proving propositional unsatisfiability
of ground clauses with the interpretted
equality operator. Techniques for
inferring equalities using
transitivity of equality and
properties of function definition.
|
| Mar 16 | More discussion on inferring equalities
in formulae with uninterpretted
functions. Optimizing the number
of additional constraints that need
to be conjuncted to a given set of
ground clauses to capture the
effect of having equalities.
|
| Mar 20 | Simple programs and expressing
states of programs using first-order
logic formulae. Transforming states
through program statements. Use
of existential quantification for
computing "image" of a state under
a given program statement. Discussion
on why universal quantification
doesn't work for computing images.
|
| Mar 21 | Proving program properties by
using inductive invariants and
considering transformations of
first order logic formulae representing
set of states at different program
locations. Illustration with an
example. |
| Mar 22 | Notion of undecidability in computation.
Use of a simple example to prove that
certain things cannot be computed
algorithmically. Implications and
a few subtleties of this result.
|
| Mar 27 | Undecidability of checking satisfiability of
arbitrary first order logic sentences.
A proof through the encoding of computations
of simple programs and asking whether
a particular location in the program can
be reached.
|
| Mar 28 | Notion of Kripke structures,
path and state formulae.
Syntax of (simplified) path
formulae and state formulae.
Illustration of usage.
Introduction to semantics of
path formulae.
|
| Mar 29 | Semantics of path formulae,
equivalences between different path
formulae.
Illustrations of how certain
properties of paths can be captured
with path formulae.
|
| Apr 3 | Encoding path formulae in first-order
logic. Discussion and illustrations.
|
| Apr 4 | Semantics of state formulae,
extending the definiion of
path formulae using state formulae
(instead of atomic propositions)
as basic building blocks.
The logic CTL*, and the fragment
LTL.
Understanding the meaning of some
interesting LTL formulae.
|
| Apr 5 | Restrictions on CTL* to yield
CTL. Examples of formulae that
are in CTL and not in CTL.
Notion of computation trees and
evaluation of CTL formulae on
trees. Discussion on some commonly
used constructs in CTL formulae
|
| Apr 10 | More discussion on CTL formulae,
constructing composite Kripke structures
from individual Kripke structures,
using CTL and LTL to express interesting
properties of systems: illustrations
|
Apr 10
(2nd lecture) | Showing the sufficiency of a subset of
operators for expressing all CTL
formulae.
Model checking CTL formulae: A state
labeling algorithm for EU formulae.
Illustration with examples.
Discussions on soundness and
completeness of algorithm.
|
| Apr 11 | Algorithms for checking different
CTL formulae on given Kripke structure:
labeling states iteratively for AG,
EG, AU, EU, AR, ER formulae.
Discussions on soundness and completeness
of these algorithms.
Summary of course.
|