Last update: 18/11/2024, 11.45
Mail to V.Goranko
Date 11/09/2024
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;
-- Propositional logical equivalence and negation normal form;
Conjunctive and disjunctive normal forms (CNF and DNF).
Lecture Notes on Classical Logic (provided on Athena:) Sections 1.1-1.3
Alternatively: Sections 1.1-1.3 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. 2. Open Course Project, University of Amsterdam
See more references below
Introduction 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.14-16: 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. 24-26: 3a,b; 4b,d, 5a,c,e
Ex. 1.3.4, p.30-31: 2a,f; 3g,h,j; 4a,e.
Date 18/09/2024
Revision and further topics of propositional logic:
-- Propositional tableaux.
-- Clausal forms. Propositional Resolution.
Revision on classical first-order logic (FOL):
-- First-order structures and languages.
-- First-order terms and formulae.
Lecture Notes on Classical Logic, Ch.2: 2.1, 2.3, 2.5, 3.1
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
W. Hodges, Elementary Predicate Logic, Sections 1-15, in: D.M. Gabbay and F.Guenthner (eds.), Handbook of Philosophical Logic. 2nd edition. Vol. l , 1-129. Kluwer, 2001.
See more references below
Basic concepts of logical deductive systems
Propositional tableaux
Propositional Resolution.
Revision on classical first-order logic (FOL): Part I
From the lecture notes:
Ex. 2.3.4, p. 59-62: 1c,f,g; 2c,f; 3c; 4d; 5b
Ex. 2.5.5, p.75-77. Own selection from: 4a,c,e; 5a,c,e,g,i; 6a,c,e,g; 7b,d,h
Ex. 3.1.4, p.97-98, 3+4a,e,h; 6, 7a,f,j,m, 10, 11.
Date 25/09/2024
Revision on classical first-order logic (FOL):
Translations from FOL to natural language.
Translations from natural language to FOL.
Formal semantics of FOL. Evaluation games.
Syntax and grammar of FOL.
Lecture Notes on Classical Logic, Sections 3.1, 3.2, 3.3
Sections 3.1, 3.2. 3.3 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 and 10. Open Course Project, University of Amsterdam
Richard Zach, Sets, Logic, Computation, An Open Logic Text, Ch.5
See more references below
First-order structures and languages. First-order terms and formulae. Semantics of FOL. Evaluation games. Translations between FOL and natural language.
Syntax and grammar of FOL.
Ex. 3.2.7, p.109-111: 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.
Howard Pospesel and David Marans, Arguments: Deductive Logic Exercises (2nd ed, 1978, Prentice Hall)
Date 02/10/2024
Revision on classical first-order logic (FOL):
Satisfiability, validity, and logical consequence in FOL
Syntax and grammar of FOL.
Lecture Notes on Classical Logic
Sections
3.3, 3.4.1-3.4.5
Sections
3.3, 3.4.1-3.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
Syntax and grammar of FOL.
Satisfiability, validity, and logical consequence in FOL
Ex. 3.3.7, p.118-122. 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.138-142. Own selection from: 1a,c,e,g,i,k,m,o,q,r; 6a,c,e; 7f; 8a,c,e,g,i,k;
Assignment 1 to be posted.
Date 07/10/2024
Semantic tableaux for first-order logic.
Logical equivalence in first-order logic. Negating first-order formulae.
Prenex normal forms, Skolemization, clausal forms.
Lecture Notes on Classical Logic, Sections 3.4.5-3.4.7, 4.1, 4.2, 4.4
Sections 3.4.5-3.4.7, 4.1, 4.2, 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
Semantic tableaux for first-order logic.
Logical equivalence in first-order logic. Negating first-order formulae.
Prenex normal forms. Skolemization, clausal forms.
From the lecture notes:
Ex. 3.4.9, p.138-142. 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.158-162: 1c; 2a,e,g; 4c,d,h,l.
Ex. 4.4.4, p.173. Ex. 2,4,6,10.
Date 09/10/2024
Resolution rule for first-order logic.
Term unification.
Resolution with unification in first-order logic.
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
Sections 4.5, 5.4 from the book Logic as a Tool (available from the SU library)
Alexander Leitsch, Resolution theorem proving: a logical point of view, in: In Logic Colloquium ’01 (pp. 3-42). Association of Symbolic Logic, 2005, A K Peters, Ltd.
Chapter 5. First-Order Logic With Equality , Lecture notes / Book chapter by ??.
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 First-Order Logic
Also, see list of additional readings below
Resolution with unification in first-order logic.
Resolution-based Automated Reasoning
From the lecture notes:
Ex. 4.5.8, p.183-187. Ex. 1, 2a,c,e,h; 3a,c,e,h; 4a,c,e,g,i,k; 5b,d,f; 6a,b; 8a,c; 10
Date 16/10/2024
Introduction to Logic programming and Prolog.
Introduction to logical methods for program verification.
Floyd-Hoare logic for proving partial correctness of imperative sequential programs.
The first 2 chapters from: Learn Prolog Now!
Mike Gordon, Background reading on Hoare Logic, Ch.1-2, pp 7-32
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 256-305 (available on Athena). Book available from the SU library.
Vladimir Lifschitz, What Is Answer Set Programming?, AAAI 2008.
Andrew Cropper, Sebastijan Dumancic, Inductive logic programming at 30: a new introduction
Introduction to Floyd-Hoare logic
Introduction to Logic programming and Prolog (John's slides)
Exercises on Floyd-Hoare 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
Selected solutions of exercises on Floyd-Hoare logic
Date 23/10/2024
Practical introduction to SWI Prolog.
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. 99-218, 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
Introduction to PDL
Exercises on PDL
Solutions to selected exercises on on PDL
Submission of Assignment 1.
Assignment 2 to be posted.
Date 28/10/2024
Logic-based 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 1-4
(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
Transition systems and computations. Properties of computations. Basic modal logic for transition systems. Unfoldings and bisimulations.
Selected exercises from the lecture notes:
Section 8.1-8.2, pp 125-128.
Exercises: 5, 6, 10, 13, 14, 15, 16, 17, 18.
Date 18/11/2024
Unfoldings and bisimulations of transition systems.
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
Linear time temporal logics of computations
Selected exercises from the lecture notes:
Section 8.3, pp 129-131
Exercises: 28, 29, 30, 31, 32, 33
Submission of Assignment 2: November 13. Assignment 3 to be posted.
Date 20/11/2024
Branching-time 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.4--3.7
For a more detailed exposition see: S. Demri, V. Goranko, M. Lange: Temporal Logics in Computer Science, CUP, 2016, Chapter 7
Giuseppe De Giacomo, slides on Least and Greatest Fixpoints
Branching time temporal logics, Part I
Selected exercises from the lecture notes:
Section 8.4, pp 132-136
Exercises: 36, 37, 41, 43, 53
Date 27/11/2024
Model-checking in CTL. Applications to verification of concurrent systems.
nuXmv: a tool for symbolic model checking
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.4-2.6
M. Huth and M. Ryan, Logic in Computer Science modelling and reasoning about systems, CUP, 2004. 2nd ed. Chapters 3.4--3.7
For a more detailed exposition see:
S. Demri, V. Goranko, M. Lange: Temporal Logics in Computer Science, CUP, 2016, Chapter 7
Branching time temporal logics: full set of slides
Presentation on nuXmv
Selected exercises from the lecture notes (carried over from Lecture 11):
Section 8.4, pp 132-136
Exercises: 36, 37, 41, 43, 53
Date 04/12/2024
Logics for multi-agent systems.
The multi-agent temporal logic ATL.
Lecture notes on Temporal Logics of Computations (provided on Athena), Chapter 7
For 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 multi-player 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. 93--136.
R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM 49:672-713, 2002 Sections 1-3.
Alternating time temporal logics
Selected exercises from the lecture notes :
Section 8.5, pp 137-139
Exercises: 61, 64, 66, 67
Submission of Assignment 3
Date TBA
Feedback on Assignment 3
Concluding remarks and final discussion on the course
Link to departamental course page
Link to course plan (in Swedish)
By appointment
Lecture notes, slides and other reading material will be provided or linked to this page on an ongoing basis.
List of exercises will be provided on a weekly basis, usually taken from the lecture notes and handouts. Students are advised to do as many exercises on each topic as they need to master it. Solutions or hints to some selected exercises will be provided and will be discussed in the discussion time before and during the lectures.
There will be 3 mandatory written assignments during the course, each consisting of a set of exercises. The assignments will be provided about 10-14 days before the submission deadline. Students must do these exercises individually and prepare written reports with their solutions. Strict deadlies for submission of the assignment reports will apply.
The assignments will be checked and corrected by the lecturer and the teaching assistant, then returned to the students for feedback. The average of the assignments grades will form the final grade.
If you have any queries on the information above, talk to me or send me an email.
Mail to V.Goranko