| Date | Topics details |
|---|
| Jan 6 | Introduction to the course and logistics.
Introduction to Propositional Logic, its
syntax and semantics. |
| Jan 7 | More on semantics of propositional logic.
Explanation of notations.
Natural deduction calculus for propositional
logic. |
| Jan 11 | Proof rules in natural deduction and their
justification. Examples of using rules to
syntactically prove a sequent. |
| Jan 12 | A (large) set of common-knowledge rules for
natural deduction based proofs. Discussion
on usage of these rules through examples. |
| Jan 13 | A small and complete set of rules for natural
deduction based proofs. Derivation of other
rules from the above set: Proof by Contradiction,
Law of Excluded Middle, Modus Tollens.
Illustration of usage of proof rules. |
| Jan 18 | Discussion on soundness and completeness of
natural deduction for propositional logic.
Proof of soundness. |
| Jan 20 | Proof of soundness continued: discussion on
mathematical induction and use of structural
induction to prove soundness of natural deduction
for propositional logic. |
| Jan 25 | Proof of completeness of natural deduction
for propositional logic. |
| Jan 27 | Completing the "completeness proof" of
natural deduction for propositional logic.
Semantic equivalence of formulae, and
syntactic means to establish semantic
equivalence. Use of semantic equivalence
to arrive at minimal sets of connectives
for propositional logic. |
| Jan 28 | Notions of validity and satisfiability.
Conjunctive normal form (CNF) of propositional
logic formulae. Validity checking in CNF. |
| Feb 1 | Dual roles of validity checkers and satisfiability
checkers. CNF SAT for propositional logic.
Notion of equisatisfiable formulae. |
| Feb 3 | More on equisatisfiability. Implication-free
formulae and Negation Normal Form (NNF).
A linear time technique for converting a formula
to an equisatisfiable CNF formula: labeled CNF
procedure. Examples of formulae conversions that
preserve semantics and/or satisfiability. |
| Feb 4 | Notion of k-CNF formulae. Sufficiency of 3-CNF
for all propositional logic formulae. Converting
arbitrary k-CNF formulae into equisatisfiable
3-CNF formulae.
Surprise Quiz 1
|
| Feb 8 | DPLL satisfiability solving framework for
propositional logic formulae in CNF. Horn clauses
and Horn formulae. An efficient algorithm for
checking satisfiability of Horn formulae.
|
| Feb 10 | Introduction to Predicate Logic. Motivation
for a logic richer than propositional logic.
Notions of terms, functions and predicates.
Definition of predicate logic syntax. Notion
of quantifiers, scope of quantifiers and free
and bound variables.
|
| Feb 11 | More on free and bound variables. An operational
informal semantics of predicate logic. Illustration
of evaluation of predicate logic formulae over
finite sorts.
|
| Feb 15 | Substitution of terms for free variables in
predicate logic formulae: caveats and pitfalls.
Formal semantics of predicate logic:
Models and environments (variable assignments)
for evaluating formulae. Inductive definition
of semantics.
|
| Feb 17 | More on semantics of predicate logic. Constructing
models and counterexamples of given formulae.
Illustration of formulae for which counterexamples
cannot be obtained, discussion of reasoning
involved.
|
| Feb 18 | "Positive" role of syntactic transformations in
proving validity of predicate logic implications.
Natural deduction for predicate logic: proof rules
for equality and universal quantification.
Illustration with examples.
|
| Feb 21-25 | Mid-semester examination week |
| Mar 1 | Recap of natural deduction proof rules for universal
quantification. Proof rules for existential
quantification. Examples of natural deduction proofs
in predicate logic, as extension of proofs in
propositional logic. Discussion on soundness and
completeness of natural deduction for predicate
logic ("proof" of completeness excluded).
Satisfiability and validity of predicate logic
formulae. Intuition behind why these questions are
much harder for predicate logic than for
propositional logic.
|
| Mar 3 | Undecidability of predicate logic: notion of
undecidability, a simple problem and a
simple proof of its undecidability. Post's
Correspondence Problem (PCP) as an undecidable
problem: statement of problem, examples,
reduction of validity checking of predicate
logic to PCP.
|
| Mar 4 | More on reduction of validity checking of
predicate logic to PCP, impossibility of
a validity checker for predicate logic.
Prenex normal form: definition, notions of
prefix and matrix, PCNF and PDNF formulae.
Illustration of prenex normal forms through
examples.
|
| Mar 8 | Institute Holiday |
| Mar 10 | More on prenex normal forms. Quantifier
equivalences and intuition behind their proofs.
Role of quantifier equivalences in deriving
prenex normal forms of arbitrary predicate logic
formulae.
|
| Mar 11 | More on prenex normal forms: role of variable
renaming and quantifier equivalences.
Skolem normal form: definition, intuition behind
Skolem functions, equisatisfiability of an
arbitrary predicate logic formula and its
Skolem normal form. Illustration of Skolem
normal form through examples.
|
| Mar 15 | More on Skolem normal forms, reducing the
arity of skolem functions wherever possible.
Use of SNF for checking validity and contradiction
of predicate logic sentences.
|
| Mar 17 | More on use on SNF for checking validity of
predicate logic sentences. Compactness Theorem:
a simplified version, and its utility in checking
entailment of a sentence by a set of sentences.
|
| Mar 18 | Discussion on some implications of the
compactness theorem, and proofs of the same.
|
| Mar 22 | More elaboration and clarifications on
Compactness Theorem, two different variants.
Herbrand's Theorem and its use in
unsatisfiability checking.
Definition and illustration of Herbrand universe,
ground terms, predicates and clauses.
Semi-decidability of satisfiability checking for
predicate logic.
|
| Mar 24 | Illustration through example of use of Herbrand's
theorem in proving validity of predicate logic
sentences.
Summary discussion on validity-checking and
satisfiability-checking of predicate logic
sentences. Introduction to use of predicate
logic in proving properties of simple programs.
|
| Mar 25 | More on using predicate logic in proving
properties of programs in Floyd-Hoare
style. Notion and importance of loop
invariants, illustration through examples.
|
| Mar 29 | Illustration of how proof subgoals change
with different syntactic constructs used
in a program. Use of predicate logic in
proving properties of hardware circuits,
illustration through reasoning
about state reachability in sequential
circuits.
|
| Mar 31 | Introduction to temporal logics and Kripke
structures as models of temporal logics.
Linear Temporal Logic (LTL): its syntax
and semantics. |
| Apr 1 | More on LTL syntax and semantics, relations
between LTL operators, expressing useful
properties of state transition systems in
LTL |
| Apr 7 | More on LTL operators and their relations.
Detailed study of an arbitration example:
constructing composite Kripke structure
from individual Kripke structures, expressing
starvation-freeness and safety properties
as LTL properties. |
| Apr 8 | Modeling concurrent finite-state programs
accessing a critical section, using Kripke
structures. Expressing properties about
such programs in LTL. |
| Apr 12 | Computation Tree Logic (CTL): syntax and
semantics. Difference between branching
(tree-structured) view of time and
linear view of time. |
| Apr 14 | More on CTL syntax and semantics.
Unrolling a Kripke structure to obtain a
computation tree, notions of state
formulae and path formulae. Scope of quantifiers
in CTL formulae. |
| Apr 15 | Expressing properties of Kripke structures using
CTL. Relations between CTL operators.
Relation between expressiveness of CTL and LTL
- examples of properties that can be expreseed in
one but not in the other.
|
Apr 15
(2nd lecture) | More on relations between
different CTL operators. Expressing CTL
formulae in terms of a restricted set of
operators. Explicit-state model checking
algorithm for CTL. Summary of topics studied
in this course. |