- 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) .
- Peter B. Andrews, An Introduction to Mathematical Logic
and Type Theory: To Truth Through Proof, 2nd edition, Springer, 2002
(Reference)
- B. A. Davey and H. A. Priestley, Introduction to
Lattices and Orders, Second edition, Cambridge University Press,
2001 (Text for course)
- L. Libkin, Elements of Finite Model Theory, Springer, 2004
(Reference)
- D. Kroening and O. Strichman, Decision Procedures:
An Algorithmic Point of View , Springer, 2008
(Reference)
- J.C.M. Baeten, T. Basten and M.A. Reniers, Process Algebra:
Equational Theories of Communicating Processes ,
Cambridge Tracts in Theoretical Computer Science, Cambridge University
Press, 2010
(Reference)
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.
Lecture Schedule
| Date | Topics details | |
|---|
| Jul 22 | Course overview, prerequisites and logistics.
Syntax and semantics of first order logic,
notion of structures, properties of graphs
expressed in first order logic |
| Jul 26 | Notions of validity and satisfiability,
natural deduction proof system for propositional
logic: soundness and examples of usage |
| Aug 2 | Completeness of natural deduction for propositional
logic, extending to a natural deduction proof system
for first order logic, statement of compactness
theorem and its use in proving expressive limitations
of first order logic. |
Aug 5
(extra class) | A simple proof of compactness theorem of
propositional logic, applications of compactness
theorem |
| Aug 9 | More applications of compactness theorem,
understanding where Axiom of Choice is used in
proving compactness theorem, Prenex normal forms
and Skolem normal form for first-order logic
formulas, notion of Skolem functions. |
|