| Date | Topics details |
|---|
| Jan 3 | Introduction to the course and logistics.
Some interesting problems that can be solved
by studying logic. A few brain-teasers to
be solved by students without using formal
logic.
Introduction to Propositional Logic |
| Jan 5 | Syntax and semantics of propositional logic.
Explanation of notations.
|
| Jan 6 | Introduction to natural deduction calculus for
propositional logic.
Proof rules in natural deduction and their
justification. Examples of using rules to
syntactically prove a sequent.
|
| Jan 10 | A small and complete set of rules for natural
deduction based proofs. Derivation of other
rules from the above set: Law of Excluded Middle
(LEM), Modus Tollens.
Illustration of usage of proof rules. |
| Jan 12 | Discussion on soundness and completeness of
natural deduction for propositional logic.
Intuitive justification for claim of soundness
|
| Jan 13 | The duality of natural deduction based reasoning
and truth-table based reasoning for propositional
logic. Illustration of duality through concrete
examples. |
| Jan 17 | Mimicking truth tables in natural deduction
proofs. Discussion on generality of this method
and its use in proving the completeness of
natural deduction for propositional logic.
|
| Jan 18 | Outline of the proof of completeness of
natural deduction for propositional logic:
Discussion on the special role of Law of
Excluded Middle in such proofs. Discussion
on the role of proof rules involving two
operators (like LEM or double negation
elimination) |
| Jan 19 | Some more perspective on the soundness and
completeness of natural deduction for propositional
logic. Notions of syntatic and semantic
equivalences.
Normal forms of propositional logic formulae:
negation normal form (NNF), conjunctive normal
form (CNF), disjunctive normal form (DNF). Proof
that any formula can be converted to a semantically
equivalent CNF formula.
|
| Jan 27 | Notions of validity and satisfiability of
propositional logic formulae, duality
between them. A linear-time procedure to check
validity of formulae in CNF, and to check
unsatisfiability of formulae in DNF. Discussion
on complexity involved in transforming a
formula to a seamtically equovalent CNF or DNF
formulation.
|
| Jan 31 | Notions of semantic equivalence and
equisatisfiability, differences between the two
notions. Illustration with examples.
|
| Feb 1 | Quiz 1 |
| Feb 2 | More on CNF satisfiability. Converting an
arbitrary propositional logic formula to an
equisatisfiable CNF formula, proof of
equisatisfiability.
|
| Feb 3 | Some motivation for studying satisfiability of
CNF formulae: reducing the problem of finding
if a graph can be partitioned into a set of
cycles to propositional satisfiability, illustration
of how different assertions about the graph
and about our desired solution can be cast into
propositional logic |
| Feb 7 | More of reducing graph problems to propositional
satisfiability. Determining satisfiability of
simple CNF formulae. Introduction to Horn clauses
and Horn formulae. Intuition behind finding
satisfiability of Horn formulae efficiently.
|
| Feb 8 | An efficient algorithm for determining
satisfiability of Horn formulae.
Introduction to the basic ideas of DPLL
framework for satisfiability solving
of CNF formulae: use of pure literals
and unit clauses |
| Feb 14 | More on the DPLL class of algorithms
for propositional satisfiability:
choosing literals to split.
A recursive DPLL algorithm, and a
simple illustration of how it works.
Introduction to Stalmarck's method
of refuting propositional logic
formulae: basic idea of using triplets
and equivalence classes of literals,
rules for inferring literal equivalences
from and-triplets and existing
equivalences.
|
| Feb 15 | More on Stalmarck's method: rules for
inferring literal equivalences from
boolean equivalence triplets.
Lookahead (LA) steps as applications of
LEM, inferring new equivalences of
literals from lookahead rules, application
of LA(k) and LA*(k), and description of
the overall Stalmarck's procedure.
Example illustrating use of Stalmarck's
procedure. |
Feb 16
8:30-9:30am | Deficiencies of propositional logic and
need for a richer logic. Introduction
to predicate logic as an enriching of
propositional logic. Syntax of predicate
logic |
Feb 16
10:35-11:30am | Notions of free and bound variables
in predicate logic formulae.
A simple bottom-up technique for
determining variable bindings and
scopes of bound variables.
Introduction to semantics of predicate
logic: notions of model and
environment, recursive definition
of semantics |
| Feb 28 | More on semantics of predicate logic. Discussion
on substitution and caveats in performing
substitution. The equality predicate and
its special role. Natural deduction proof
rules for equality introduction and elimination.
|
| Mar 1 | More on natural deduction proof rules: equality
rules, rules for introducing and eliminating
quantifiers. |
| Mar 2 | Illustration of usage of natural deduction proof
rules through example proofs. |
| Mar 7 | Discussion on soundness and completeness of the
natural deduction proof system for predicate logic.
Introduction to the notion of uncomputability
(undecidability) |
| Mar 8 | Discussion on semi-decidability of validity
checking and satisfiability checking
for predicate logic. Intuition for the
semi-decidability of these problems.
Approaches for incomplete validity checking.
|
| Mar 9 | Quantifier equivalences in predicate logic.
Prenex normal forms and use of quantifier
equivalences in obtaining prenex normal forms.
|
| Mar 14 | Skolem normal form (SNF) and Skolem functions.
Equisatisfiability of a formula and its
SNF.
|
| Mar 15 | Institute Holiday |
| Mar 16 | Illustration of skolemization through examples.
Relation between a model for a formula and
the augmented model of its SNF. |
| Mar 21 | Illustration of skolemization through examples.
Relation between a model for a formula and
the augmented model of its SNF. |
Mar 21
3:00-4:00 pm | Bernays-Schonfinkel class as a simple decidable
syntactic fragment of predicate logic. Discussion
on linear model sizes of sentences in this
class. |
| Mar 22 | Notions of ground terms, ground clauses and
Herbrand Universe. Herbrand's Theorem for
unsatisfiable predicate logic formulae.
Illustration through examples. |
| Mar 23 | More on application of Herbrand's Theorem.
Introduction to Compactness Theorem for predicate
logic. Discussion on implications of Compactness
Theorem |
| Mar 28 | Quiz 2 |
| Mar 29 | No class |
| Mar 30 | Institute Holiday |
| Apr 4 | Introduction to Computation Tree Logic
(CTL) and its syntax, and how it
forms a useful fragment of predicate logic
|
| Apr 5 | Some more predicate logic and model theory:
Discussion on Compactness Theorem and its
application in proving the non-existence of
certain predicate logic formulae
|
| Apr 6 | More discussion on Compactness Theorem
through examples. Showing that evenness of
cardinality of universe can't be expressed
in predicate logic without using function
symbols or predicate symbols other than
equality. |
| Apr 7 | Relation between Herbrand's Theorem and
Compactness Theorem; more examples. Summary
of our study of predicate logic and
the need for richer logics. |
| Apr 11 | Introduction to Kripke structures and the notion
of checking properties about infinite paths in
Kripke structures. Computation Tree Logic (CTL)
as a special fragment of predicate logic suitable
for such reasoning. |
| Apr 12 | Elaboration on CTL and its syntax,
usage. Discussion on special quantifier
structures in CTL.
Notion of computation tree obtained from
a Kripke structure and evaluating CTL
formulae on labeled trees.
|
Apr 12
2:00-3:30 pm | Semantics of CTL; examples of useful properties
expressed using CTL. Introduction to CTL
model checking and what it entails.
|
| Apr 13 | CTL model checking algorithm based on fixpoint
semantics; example of use of CTL model checking
algorithm. Summary of topics covered in course
|