Week / lecture 
Date 
Main Topics 
Course notes and readings 
Additional readings 
Slides 
Selected exercises 
Solutions to selected exercises 
Assignments and submission deadlines 
36/01 
02.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 inferences. 
Lecture Notes on Classical Logic, (Provided on Athena) Sections 1.11.3
Alternatively: Sections 1.11.3 from the book Logic as a Tool (available from the SU library)


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

From the lecture notes: (Do as many exercises from each group as needed)
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 (moved to Lecture 2)
Ex.1.2.4, p. 2426: 3a,b; 4b,d, 5a,c,e (carried over from Lecture 1) 
Provided on Athena 

37/02 
09.09 
Revision on propositional logic:
 Propositional logical equivalence and negation normal form.
 Conjunctive and disjunctive normal forms (CNF and DNF).
 Basic concepts of logical deductive systems
 Propositional tableaux.
 Propositional Resolution.

Lecture Notes on Classical Logic, Ch.2: 2.1, 2.3, 2.5, 3.1
Alternatively:
Sections 2.1, 2.3, 2.5, 3.1 from the book Logic as a Tool (available from the SU library)

J. van Benthem, H. van Ditmarsch, J. van Eijck, J. Jaspars, Logic in Action, Ch. 4. Open Course Project, University of Amsterdam
See more references below 
Provided on Athena:
Propositional logical equivalence and negation normal form. Conjuncive and disjunctive normal forms (CNF and DNF).
Basic concepts of logical deductive systems
Propositional tableaux
Propositional Resolution.

From the lecture notes:
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. 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 Athena 

38/03 
16.09 
Classical firstorder logic (FOL): basic consepts. Firstorder structures and languages.
Firstorder terms and formulae.
Formal semantics of FOL. Evaluation games.
Translations from FOL to natural language.

Lecture Notes on Classical Logic, Sections 3.2
Alternatively:
Sections 3.2 from the book Logic as a Tool (available from the SU library) 
W. Hodges, Elementary Predicate Logic, Sections 115, in: D.M. Gabbay and F.Guenthner (eds.), Handbook of Philosophical Logic. 2nd edition. Vol. l , 1129. Kluwer, 2001.
J. van Benthem, H. van Ditmarsch, J. van Eijck, J. Jaspars, Logic in Action, Ch. 4 and 10. Open Course Project, University of Amsterdam
Richard Zach, Sets, Logic, Computation, An Open Logic Text, Ch.5
See more references below 
Provided on Athena:
Firstorder structures and languages. Firstorder terms and formulae. Semantics of FOL. Evaluation games. Translations between FOL and natural language. 
From the lecture notes:
Ex. 3.1.4, p.9798, 3+4a,e,h; 6, 7a,f,j,m, 10, 11.
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.
For additional exercises:
Howard Pospesel and David Marans, Arguments: Deductive Logic Exercises (2nd ed, 1978, Prentice Hall)

Provided on Athena 

39/04 
26.09 
Translations from natural language to FOL.
Syntax and grammar of FOL.
Satisfiability, validity, and logical consequence in FOL

Lecture Notes on Classical Logic, Sections
3.3.13.3.6, 3.4.13.4.5.
Alternatively:
Sections
3.3.13.3.6, 3.4.13.4.5
from the book Logic as a Tool (available from the SU library)

J. van Benthem, H. van Ditmarsch, J. van Eijck, J. Jaspars, Logic in Action, Ch. 10. Open Course Project, University of Amsterdam
Richard Zach, Sets, Logic, Computation, An Open Logic Text, Ch.5
See more references below 
Provided on Athena:
Syntax and grammar of FOL.
Satisfiability, validity, and logical consequence in FOL

From the lecture notes:
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; 11a,c,e,g,i; 13a,c,f,g,h,j;
Ex. 3.4.9, p.138142. Own selection from: 1a,c,e,g,i,k,m,o,q,r; 6a,c,e; 7f; 8a,c,e,g,i,k;

Provided on Athena 

40/05 
30.09 
Logical deduction and deductive systems for FOL: basic concepts.
Semantic tableaux for firstorder logic.
Logical equivalence in firstorder logic. Negating firstorder formulae.
Prenex normal forms, Skolemization, clausal forms. (These topics are not required for the intro version)

Lecture Notes on Classical Logic, Sections 4.2, 3.4.53.4.7, 4.4
Alternatively:
Sections 4.2, 3.4.53.4.7, 4.4 from the book Logic as a Tool (available from the SU library)

J. van Benthem, H. van Ditmarsch, J. van Eijck, J. Jaspars, Logic in Action, Ch. 10. Open Course Project, University of Amsterdam
See more references below 
Provided on Athena:
Semantic tableaux for firstorder logic.
Logical equivalence in firstorder logic. Negating firstorder formulae.
Prenex normal forms. Skolemization, clausal forms.

From the lecture notes:
Ex. 3.4.9, p.138142. Own selection from: 12a,c,h; 13, 14a,c,e,g,i; 15b,d,f,h; 16; 18a,c,e (only formalisation and semantic argument) 19a,d
Ex. 4.2.4, p.158162: 1c; 2a,e,g; 4c,d,h,l.
Ex. 4.4.4, p.173. Ex. 2,4,6,10.

Provided on Athena 
Assignment 1 posted. Submission deadline: 13.00 on October 16.

41/06 
07.10 
Resolution rule for firstorder logic.
Term unification.
Resolution with unification in firstorder logic.
(The topics above are not required for the intro version)
Applications to AI: Knowledge reprepresentation and automated reasoning in FOL
A brief intro to the Automated Theorem Prover SPASS.

Lecture Notes on Classical Logic, Sections 4.5, 5.4
Alternatively:
Sections 4.5, 5.4 from the book Logic as a Tool (available from the SU library)

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 
To be provided
Resolution with unification in firstorder logic.
Resolutionbased Automated Reasoning

From the lecture notes:
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 Athena 

41/07 
10.10 
Introduction to logical methods for program verification.
FloydHoare logic for proving partial correctness of imperative sequential programs.
Introduction to Logic programming. Practical introduction to Prolog. (by Anders Lundstedt)

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

Robert Kowalski, Logic programming History
M. Huth and M. Ryan, Logic in Computer Science modelling and reasoning about systems, CUP, 2004. 2nd ed. Chapter 4, pp 256305 (available on Athena). Book available from the SU library.
M. Spivey, An introduction to logic programming through Prolog, PrenticeHall International, 1995. Revised electronic version. Chapters 18

Provided on Athena:
Introduction to FloydHoare logic
Introduction to Logic programming and Prolog (Anders' slides) 
Provided on Athena:
exercises on FloydHoare logic from the book "Logic in Computer Science modelling and reasoning about systems" by M. Huth and M. Ryan
Exercises on Logic programming and Prolog (by Anders)

Provided on Athena:
Selected solutions of exercises on FloydHoare logic 

42/ 08 
14.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 Athena)

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
Rob Goldblatt, Logics of Time and Computations, CSLI pubblications, 2nd ed., 1992. Chapter 10

To be provided
Introduction to PDL

Provided on Athena:
Exercises on PDL

Provided on Athena:
solutions to selected exercises on on PDL 
Assignment 1 submissions closed
Assignment 2 posted. Submission deadline: 13.00 on October 31.

44/09 
28.10 
Logicbased model checking: brief intro
Transition systems and computations.
Modal logic for transition systems.
Unfoldings and bisimulations of transition systems. 
Lecture notes on Temporal Logics of Computations (provided on Athena) Chapters 14
(For a more detailed exposition see: S. Demri, V. Goranko, M. Lange: Temporal Logics in Computer Science, CUP, 2016, Chapters 3,4,5) 
Selected readings from the Handbook of Model Checking, Springer, 2017:
 E. Clarke, T. Henzinger, H. Veith, Introduction to Model Checking, Section 1.1
 N. Piterman, A. Pnueli, Temporal Logic and Fair Discrete Systems. Sections 2.1, 2.2
M. Huth and M. Ryan, Logic in Computer Science modelling and reasoning about systems, CUP, 2004. 2nd ed. Chapter 3.1 
Provided on Athena
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. 
Provided on Athena 
Assignment 2 submission closed 
45/10 
04.11 
The linear time temporal logic of computations LTL. 
Lecture notes on Temporal Logics of Computations (provided on Athena)
Chapter 5

Selected readings from the Handbook of Model Checking, Springer, 2017:
 E. Clarke, T. Henzinger, H. Veith, Introduction to Model Checking, Section 1.2.4
 N. Piterman, A. Pnueli, Temporal Logic and Fair Discrete Systems. Section 2.3
M. Huth and M. Ryan, Logic in Computer Science modelling and reasoning about systems, CUP, 2004. 2nd ed. Chapters 3.2, 3.3
For a more detailed exposition see: S. Demri, V. Goranko, M. Lange: Temporal Logics in Computer Science, CUP, 2016, Chapter 6

Provided on Athena
Linear time temporal logics of computations

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

46/11 
11.11 
Branchingtime temporal logics of computations. The computation tree logics CTL and CTL*.

Lecture notes on Temporal Logics of Computations (provided on Athena)
Chapter 6

Selected readings from the Handbook of Model Checking, Springer, 2017:
 E. Clarke, T. Henzinger, H. Veith, Introduction to Model Checking, Section 1.2
 N. Piterman, A. Pnueli, Temporal Logic and Fair Discrete Systems. Section 2.4, 2.6.
M. Huth and M. Ryan, Logic in Computer Science modelling and reasoning about systems, CUP, 2004. 2nd ed. Chapters 3.43.7
For a more detailed exposition see: S. Demri, V. Goranko, M. Lange: Temporal Logics in Computer Science, CUP, 2016, Chapter 7

Provided on Athena:
Branching time temporal logics

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

Provided on Athena 
Assignment 3 posted. Submission deadline: 13.00 on November 26. 
47/12 
18.11

Modelchecking in CTL. Applications to verification of concurrent systems.
nuXmv: a tool for symbolic model checking (Anders) 
Lecture notes on Temporal Logics of Computations (provided on Athena)
Chapter 6

Selected readings from the Handbook of Model Checking, Springer, 2017:
 N. Piterman, A. Pnueli, Temporal Logic and Fair Discrete Systems. Section 2.42.6
M. Huth and M. Ryan, Logic in Computer Science modelling and reasoning about systems, CUP, 2004. 2nd ed. Chapters 3.43.7
For a more detailed exposition see: S. Demri, V. Goranko, M. Lange: Temporal Logics in Computer Science, CUP, 2016, Chapter 7 
Provided on Athena:
Branching time temporal logics: full set of slides
Presentation on nuXmv (Anders)

Selected exercises from the lecture notes (carried over from Lecture 11):
Section 8.4, pp 132136
Exercises: 36, 37, 41, 43, 53

Provided on Athena 

48/13 
25.11 
Logics for multiagent systems.
The multiagent temporal logic ATL
Concluding remarks on the course.
Exam info. 
Lecture notes on Temporal Logics of Computations (provided on Athena)
Chapter 7

3For a more detailed exposition see: S. Demri, V. Goranko, M. Lange: Temporal Logics in Computer Science, CUP, 2016, Chapter 9
Nils Bulling, Valentin Goranko, Wojciech Jamroga: Logics for reasoning about strategic abilities in multiplayer games, in: Models of Strategic Reasoning: Logics, Games and Communities, J. van Benthem, S. Ghosh, R. Verbrugge (eds.), Springer, LNCS/FoLLI series, vol. 8972, 2015, pp. 93136.
R. Alur, T.A. Henzinger, and O. Kupferman. Alternatingtime temporal logic. Journal of the ACM 49:672713, 2002 Sections 13.

Provided on Athena:
Alternating time temporal logics
General exam info 
Selected exercises from the lecture notes:
Section 8.5, pp 137139
Exercises: 61, 64, 66, 67 
Provided on Athena 
Assignment 3 submission: 13.00 on Nov 26. 
49/14 
02.12 
Feedback on Assignment 3
Final discussion and group consultation on the course






Assignment 3 submissions closed 
50 
09.12 
Exam







