Week 
Date 
Main Topics 
Course notes and readings 
Additional readings 
Slides 
Selected exercises 
Solutions to selected exercises 
Assignments and deadlines 
37/01 
12.09 
Introduction to the course.
Brief revision on basics of propositional logic: propositions and logical connectives. Truth tables. Tautologies and propositional logical consequence. Logically correct propositional infere 
Lecture Notes on Classical Logic, (provided on Mondo) Sections 1.1, 1.2

J. van Benthem, H. van Ditmarsch, J. van Eijck, J. Jaspars, Logic in Action, Ch. 2. Open Course Project, University of Amsterdam
See more references below

Provided on Mondo:
Intro to the course
Revision on basics of propositional logic

From the lecture notes:
Revision on propositional logic (as many as needed from the following):
Ex.1.1.8, p.1416: 2a,e; 3c,e; 4a,c.e; 5a,c,e; 6a,c,e; 7b,d,e; 8g,i; 9d,l
Ex.1.2.4, p. 2426: 3a,b; 4b,d, 5a,c,e.

Provided on Mondo.


38/02 
19.09 
Revision on propositional logic:
 propositional logical equivalence and negation normal form;
propositional tableaux.
Classical firstorder logic (FOL): basic consepts. Firstorder structures and languages.
Firstorder terms and formulae. 
Lecture Notes on Classical Logic
Ch.1: 1.3;
Ch.2: 2.3;
Ch.3: 3.1

J. van Benthem, H. van Ditmarsch, J. van Eijck, J. Jaspars, Logic in Action, Ch. 4. Open Course Project, University of Amsterdam
W. Hodges, Elementary Predicate Logic, Sections 113, in: D.M. Gabbay and F.Guenthner (eds.), Handbook of Philosophical Logic. 2nd edition. Vol. l , 1129. Kluwer, 2001.
See more references below 
Provided on Mondo:
Propositional logical equivalence and negation normal form
Propositional tableaux
Firstorder structures and languages

From the lecture notes: (Do as many exercises from each group as needed)
Ex. 1.3.4, p.3031: 2a,f; 3g,h,j; 4a,e.
Ex. 2.3.4, p. 5962: 1c,f,g; 2c,f; 3c; 4d; 5b
Ex. 3.1.4, p.9798, 3+4a,e,h; 6, 7a,f,j,m, 10, 11.

Provided on Mondo.


39/03 
26.09 
Formal semantics of FOL.
Translations between FOL and natural language.
Satisfiability, validity, and logical consequence in FOL

Lecture Notes on Classical Logic, Sections 3.2, 3.3.13.3.3, 3.4.13.4.3 
J. van Benthem, H. van Ditmarsch, J. van Eijck, J. Jaspars, Logic in Action, Ch. 4 and 10. Open Course Project, University of Amsterdam
W. Hodges, Elementary Predicate Logic, Sections 1415, in: D.M. Gabbay and F.Guenthner (eds.), Handbook of Philosophical Logic. 2nd edition. Vol. l , 1129. Kluwer, 2001.
See more references below 
Provided on Mondo:
Semantics of FOL.
Satisfiability, validity, and logical consequence in FOL 
Ex. 3.2.7, p.109111: 1a,b; Selection from: 4a,c,e,g,i,k,m,o,q,s,u,w,y; 5a,c,e,g,i,k,m,p,q,r,t,w,y; 6b,d,f,h,k,l,n; 7a,c,e.
Ex. 3.3.7, p.118122. Selection from: 1b,d,f,h,j,l; 2a,c,e; 3a,c,e,g,i; 4a,c,e,g,i,k,m,o; 5a,c,e,g,i,k,l,m,o,p; 6a,c,e; 7a,b,d,f,h; 10a,d,g;
Ex. 3.4.9, p.138142. Own selection from: 1a,c,e,g,i,k,m,o; 6a,c,e; 7f; 8a,c,e,gi,k; 16; 18a,c,e (only the formalisation and semantic argument) 19a,d

Provided on Mondo 

40/04 
03.10 
Syntax and grammar of FOL.
Logical deduction and deductive systems for FOL: basic concepts.
Semantic tableaux for firstorder logic.
Conjunctive and disjunctive normal forms (CNF and DNF). Propositional Resolution.

Lecture Notes on Classical Logic, Sections 3.3.43.3.6, 3.4.33.4.5, 4.2, 2.5

J. van Benthem, H. van Ditmarsch, J. van Eijck, J. Jaspars, Logic in Action, Ch. 10. Open Course Project, University of Amsterdam 
Provided on Mondo:
Syntax and grammar of FOL.
Semantic tableaux for firstorder logic.
Normal forms (CNF and DNF). Propositional Resolution.

Ex. 3.3.7, p.118122. Selection from: 11a,c,e,g,i; 13a,c,f,g,h,j;
Ex. 4.2.4, p.158162: 1c; 2a,e,g; 4c,d,h,l.
Ex. 2.5.5, p.7577. Own selection from: 4a,c,e; 5a,c,e,g,i; 6a,c,e,g; 7b,d,h

Provided on Mondo 
Assignment 1 posted on Mondo 
41/05 
10.10 
Logical equivalence in firstorder logic. Negating firstorder formulae.
Prenex normal forms, Skolemization, clausal forms.

Lecture Notes on Classical Logic, Sections 2.5, 3.4.53.4.7, 4.4

J. van Benthem, H. van Ditmarsch, J. van Eijck, J. Jaspars, Logic in Action, Ch. 10. Open Course Project, University of Amsterdam 
Provided on Mondo:
Propositional Resolution.
Logical equivalence in firstorder logic. Negating firstorder formulae.
Prenex normal forms, Skolemization, clausal forms.

Ex. 3.4.9, p.138142. 12a,c,h; 13, 14a,c,e,g,i; 15b,d,f,h;
Ex. 4.4.4, p.173. Ex. 2,4,6,10.

Provided on Mondo 

42/06 
17.10
NB: this lecture is moved to 12.10 
Resolution rule for firstorder logic.
Term unification.
Resolution with unification in firstorder logic.
Knowledge reprepresentation and automated reasoning in FOL.
A brief intro to the Automated Theorem Prover SPASS.
Introduction to Logic programming and Prolog. Applications to AI.

Lecture Notes on Classical Logic, Sections 4.5, 5.4
Chapter 1from: Learn Prolog Now! 
J. van Benthem, H. van Ditmarsch, J. van Eijck, J. Jaspars, Logic in Action, Ch. 10. Open Course Project, University of Amsterdam
Stuart Russell and Peter Norvig, Artificial Intelligence: A Modern Approach, Chapter 9: Inference in FirstOrder Logic
Robert Kowalski, Computational Logic and Human Thinking: How to be Artificially Intelligent, Nov 2010.
Also, see list of additional readings below 
Provided on Mondo:
Resolution with unification in firstorder logic.
Resolutionbased Automated Reasoning
Introduction to Logic programming and Prolog (Anders' slides) 
Ex. 4.5.8, p.183187. Ex. 1, 2a,c,e,h; 3a,c,e,h; 4a,c,e,g,i,k; 5b,d,f; 6a,b; 8a,c; 10

Provided on Mondo 
Assignment 1 submission deadline: October 20 
43/07 
24.10 
Introduction to logical methods for program verification.
FloydHoare logic for proving partial correctness of imperative sequential programs.
Practical exercises on Prolog and on FloydHoare logic

The first 2 chapters from: Learn Prolog Now!
Mike Gordon, Background reading on Hoare Logic, Ch.12, pp 732

M. Spivey, An introduction to logic programming through Prolog, PrenticeHall International, 1995. Revised electronic version.Chapters 18
M. Huth and M. Ryan, Logic in Computer Science modelling and reasoning about systems, CUP, 2004. 2nd ed. Chapter 4, pp 256305 (available on Mondo, in the Lecture notes folder)

Provided on Mondo:
Introduction to FloydHoare logic 
Provided on Mondo:
Exercises on Prolog
Exercises on FloydHoare logic


Assignment 2 posted on Mondo 
44 / 8 
31.10 
Propositional dynamic logics of programs (PDL). 
D. Harel, D. Kozen, J. Tiuryn. Dynamic Logic, Chapter in: Handbook of Philosophical Logic, 2nd ed., 2002, vol. 4, pp. 99218, Sections 1,2,4 (provided on Mondo) 
1. J. van Benthem, H. van Ditmarsch, J. van Eijck, J. Jaspars, Logic in Action, Ch. 6.
2. Andre Platzer, Lecture Notes on Dynamic Logic

Provided on Mondo:
Introduction to PDL. 
Provided on Mondo:
Exercises on PDL and selected answers



45/09 
09.11 
Transition systems and computations.
Modal logic for transition systems. 
Lecture notes on Temporal Logics of Computations (provided on Mondo) Chapters 14 
M. Huth and M. Ryan, Logic in Computer Science modelling and reasoning about systems, CUP, 2004. 2nd ed. Chapter 3.1

Provided on Mondo:
Transition systems and computations. Properties of computations. Basic modal logic for transition systems. Unfoldings and bisimulations. 
Selected exercises from the lecture notes:
Section 8.18.2, pp 125128.
Exercises: 5, 6, 10, 13, 14, 15, 16, 17, 18. 

Assignment 2 submission deadline: November 10 
46/10 
16.11 
Linear time temporal logics of computations. LTL.
SPIN: tool for LTL model checking. 
Lecture notes on Temporal Logics of Computations (provided on Mondo) Chapter 5 
M. Huth and M. Ryan, Logic in Computer Science modelling and reasoning about systems, CUP, 2004. 2nd ed. Chapters 3.2, 3.3

To be provided on Mondo:
Linear time temporal logics of computations.
Presentation on SPIN

Selected exercises from the lecture notes:
Section 8.3, pp 129131
Exercises: 28, 29, 30, 31, 32, 33


Assignment 3 posted on Mondo 
47/11 
23.11 
Branchingtime temporal logics of computations. The computation tree logics CTL and CTL*.
Modelchecking in CTL and CTL*. Applications to verification of concurrent and reactive systems. 
Lecture notes on Temporal Logics of Computations (provided on Mondo) Chapter 6 
M. Huth and M. Ryan, Logic in Computer Science modelling and reasoning about systems, CUP, 2004. 2nd ed. Chapters 3.43.7

To be provided on Mondo:
Branching time temporal logics

Selected exercises from the lecture notes:
Section 8.4, pp 132136
Exercises: 36, 37, 30, 41, 43, 53



49/12 
05.12
NB change of date and venue 
Logics for multiagent systems. Alternating time temporal logic. 
Lecture notes on Temporal Logics of Computations (provided on Mondo) Chapter 7 

Provided on Mondo:
Alternating time temporal logics
Exam info

Selected exercises from the lecture notes:
Section 8.5, pp 137139
Exercises: 61, 64, 66, 67 

Assignment 3 submission deadline 
49 
09.12 
Exam 






