 Shawn Hedman, A First Course in Logic: An Introduction to
Model Theory, Proof Theory, Computability and Complexity , Reprinted in 2006,
Oxford Texts in Logic, Oxford University Press (Text for course) .
 Michael Huth and Mark Ryan, Logic in Computer Science: Modelling
and Reasoning about Systems , Second Edition,
Cambridge University Press (Text for course) .
 B. A. Davey and H. A. Priestley, Introduction to
Lattices and Orders, Second edition, Cambridge University Press,
2001 (Text for course)
 D. Kroening and O. Strichman, Decision Procedures:
An Algorithmic Point of View , Springer, 2008
(Reference)
 An excellent set of lectures notes on the NelsonOppen decision
procedure by Prof. George Necula (Univ. of California, Berkeley)
 An excellent tutorial
introduction to Separation Logic by Peter O'Hearn. The first part of the tutorial is mostly relevant
for what we have covered in class about separation logic.
 A short introduction to Hoare Logic and the use of separation logic in proving properties of programs.
Note that the semantics of x > y as given in the slides is slightly different from what we have studied in class. We will use the semantics studied in class, i.e. one that uses dom(h) = {x}, instead of dom(h) contains x
Current Reading List
 Chapters 1 and 2 of Logic in Computer Science:... by M. Huth and
M. Ryan
 Chapters 1, 2 and 3 of A First Course in Logic: ... by
Shawn Hedman.
 Chapters 2 and 10 of Decision Procedures:
An Algorithmic Point of View by D. Kroening and O. Strichman
(available in Central Library)
Lecture Schedule
Date  Topics details  
Jul 29  Course overview and prerequisites.
Syntax and semantics of first order logic (FOL),
notion of structures 
Aug 1  Notion of free and bound variables in FOL, examples
of interesting firstorder structures: graphs,
relational databases, integers; expressing properties
of these structures using FOL formulae, notions of
satisfiability and validity 
Aug 5  Undecidability of FOL, semantic and syntactic entailment
in FOL, introduction to a proof system for FOL.

Aug 8  A closer look at proof systems: dealing with propositional
operators, soundness and completeness of proof systems,
a proof of completeness theorem of propositional logic

Aug 12  Compactness Theorem of propositional logic, and some
applications in lifting results from finite structures
to infinite structures

Aug 15  Independence Day

Aug 19  Using Compactness Theorem of propositional logic
to show some inexpressibility results.
Prenex normal forms and Skolem normal form in FOL.
Skolemization and Skolem functions. Notion of
equisatisfiability; equisatisfiability of a FOL
formula and its Skolemized form.

Aug 22  Study of Skolem normal form formulas: Herbrand
universe, Herbrand interpretation of functions,
Herbrand structures. Sufficiency of Herbrand
structures for checking satisfiability of Skolem
normal form formulas. Herbrand's unsatisfiability
Theorem.

Aug 26  More on Herbrand structures and their implications;
decidability of some fragments of FOL,
Compactness Theorem of FOL (in the countable case),

Aug 29  Compactness Theorem of FOL, and applications in
proving inexpressibility results in FOL.

Sep 2  Convering FOL formulae with equality to equisatisfiable
formulae without equality; illustration using examples.
Using Compactness Theorem
of FOL to show Completeness Theorem of FOL in a
restricted setting.

Sep 5  Decision procedures and their significance in
applications.
Resolution in propositional logic: resolvents,
resolution algorithm, termination of the algorithm,
examples

Sep 7  Resolution in firstorder logic: generalizing
resolvents from those studied in propositional logic,
most general unifier, algorithm for finding most
general unifier of a set of literals and its proof
of correctness, resolution algorithm for first order
logic and its correctness.

Sep 9, 12, 16  Midsemester week 
Sep 13  Midsemester exam 
Sep 23  Discussion on solutions of midsemester exam.
Introduction to Reduced Ordered Binary Decision
Diagrams (ROBDDs): Shannon decomposition,
ifthenelse operator and DAGbased representation
of propositional logic formulae.

Sep 26  Further discussion on ROBDDs: computing the ROBDD
of f op g from ROBDDs of f
and g for any binary operator
op. Importance of getting a good
ordering of variables in ROBDDs. Introduction to
DavisPutnamLovelandLongemann (DPLL) algorithm
for deciding CNF propositional logic formulae.

Sep 30  Further discussion on the DPLL algorithm,
backtracking and backjumping. Introduction to
satisfiability modulo theories (SMT), examples
of theories: arrays, lists, uninterpretted
functions with equality, linear arithmetic over
integers, linear arithmetic over reals.

Oct 3  Notion of pure formulae and mixed formulae,
purification of formulae in a combination of
theories, using propositionalization of theory
predicates and DPLL to reduce satisfiability
checking of arbitrary formulae in a combination
of theories to satisfiability checking of a
conjunction of literals, each of which is pure.

Oct 7  NelsonOppen algorithm for checking satisfiability
of a conjunction of pure literals, using
decision procedures of individual theories.
Notion of equality propagation, soundness of
NelsonOppen algorithm. Conditions on theories
for completeness of algorithm: stablyinfinite
and convex theories.

Oct 10  Proof of completeness of NelsonOppen algorithm
for combinations of stablyinfinite and convex
theories. Dealing with theories that do not
satisfy these requirements in practice.

