Top

Logic in Computer Science and Artificial Intelligence

Last update: 18/11/2024, 11.45
Mail to V.Goranko

Lecturer Valentin Goranko

Teaching assistant and SI meetings leader: Mikael Eriksson

Departmental course page (intro level)

Departmental course page (advanced level)

Schedule

Detailed course plan

Current version. Updates will be made frequently.

Lecture 1

Date 11/09/2024

Main Topics

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).

Recommended readings

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)

Supplementary readings

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

The Carnap book

John Slaney, The Logic Notes

See more references below

Slides posted on Athena

Introduction to the course

Revision on basics of propositional logic

Exercises and selected solutions posted on Athena

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.

Assignments and deadlines

Lecture 2

Date 18/09/2024

Main Topics

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.

Recommended readings

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)

Supplementary readings

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

Slides posted on Athena

Basic concepts of logical deductive systems

Propositional tableaux

Propositional Resolution.

Revision on classical first-order logic (FOL): Part I

Exercises and selected solutions posted on Athena

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.

Assignments and deadlines

Lecture 3

Date 25/09/2024

Main Topics

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.

Recommended readings

Lecture Notes on Classical Logic, Sections 3.1, 3.2, 3.3

Alternatively:

Sections 3.1, 3.2. 3.3 from the book Logic as a Tool (available from the SU library)

Supplementary readings

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

Slides posted on Athena

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.

Exercises and selected solutions (posted on Athena)

From the lecture notes:

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.

For additional exercises:

Howard Pospesel and David Marans, Arguments: Deductive Logic Exercises (2nd ed, 1978, Prentice Hall)

Assignments and deadlines

Lecture 4

Date 02/10/2024

Main Topics

Revision on classical first-order logic (FOL):

Satisfiability, validity, and logical consequence in FOL

Syntax and grammar of FOL.

Recommended readings

Lecture Notes on Classical Logic

Sections

3.3, 3.4.1-3.4.5

Alternatively:

Sections

3.3, 3.4.1-3.4.5

from the book Logic as a Tool (available from the SU library)

Supplementary readings

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

Slides (posted on Athena)

Syntax and grammar of FOL.

Satisfiability, validity, and logical consequence in FOL

Exercises and selected solutions (posted on Athena)

From the lecture notes:

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;

Assignments and deadlines

Assignment 1 to be posted.

Lecture 5

Date 07/10/2024

Main Topics

Semantic tableaux for first-order logic.

Logical equivalence in first-order logic. Negating first-order formulae.

Prenex normal forms, Skolemization, clausal forms.

Recommended readings

Lecture Notes on Classical Logic, Sections 3.4.5-3.4.7, 4.1, 4.2, 4.4

Alternatively:

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)

Supplementary readings

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

Slides (posted on Athena)

Semantic tableaux for first-order logic.

Logical equivalence in first-order logic. Negating first-order formulae.

Prenex normal forms. Skolemization, clausal forms.

Exercises and selected solutions (posted on Athena)

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.

Assignments and deadlines

Lecture 6

Date 09/10/2024

Main Topics

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.

Recommended readings

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)

Supplementary readings

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

Robert Kowalski, Computational Logic and Human Thinking: How to be Artificially Intelligent, Nov 2010.

Also, see list of additional readings below

Slides (posted on Athena after the lectures)

Resolution with unification in first-order logic.

Resolution-based Automated Reasoning

Exercises and selected solutions (posted on Athena)

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

Assignments and deadlines

Lecture 7

Date 16/10/2024

Main Topics

Introduction to Logic programming and Prolog.

Introduction to logical methods for program verification.

Floyd-Hoare logic for proving partial correctness of imperative sequential programs.

Recommended readings

The first 2 chapters from: Learn Prolog Now!

Mike Gordon, Background reading on Hoare Logic, Ch.1-2, pp 7-32

Supplementary readings

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.

M. Spivey, An introduction to logic programming through Prolog, Prentice-Hall International, 1995. Revised electronic version. Chapters 1-8

Added:

Vladimir Lifschitz, What Is Answer Set Programming?, AAAI 2008.

Andrew Cropper, Sebastijan Dumancic, Inductive logic programming at 30: a new introduction

Slides (posted on Athena)

Introduction to Floyd-Hoare logic

Introduction to Logic programming and Prolog (John's slides)

Exercises and selected solutions (posted on Athena)

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

Assignments and deadlines

Lecture 8

Date 23/10/2024

Main Topics

Practical introduction to SWI Prolog.

Propositional dynamic logics of programs (PDL).

Recommended readings

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)

Supplementary readings

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

Slides (posted on Athena)

Introduction to PDL

Exercises and selected solutions (posted on Athena)

Exercises on PDL

Solutions to selected exercises on on PDL

Assignments and deadlines

Submission of Assignment 1.

Assignment 2 to be posted.

Lecture 9

Date 28/10/2024

Main Topics

Logic-based model checking: brief intro

Transition systems and computations.

Modal logic for transition systems.

Unfoldings and bisimulations of transition systems.

Recommended readings

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)

Supplementary readings

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

Slides (posted on Athena)

Transition systems and computations. Properties of computations. Basic modal logic for transition systems. Unfoldings and bisimulations.

Exercises and selected solutions (posted on Athena)

Selected exercises from the lecture notes:

Section 8.1-8.2, pp 125-128.

Exercises: 5, 6, 10, 13, 14, 15, 16, 17, 18.

Assignments and deadlines

Lecture 10

Date 18/11/2024

Main Topics

Unfoldings and bisimulations of transition systems.

The linear time temporal logic of computations LTL.

Recommended readings

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

Supplementary readings

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

Slides (posted on Athena)

Linear time temporal logics of computations

Exercises and selected solutions (posted on Athena)

Selected exercises from the lecture notes:

Section 8.3, pp 129-131

Exercises: 28, 29, 30, 31, 32, 33

Assignments and deadlines

Submission of Assignment 2: November 13. Assignment 3 to be posted.

Lecture 11

Date 20/11/2024

Main Topics

Branching-time temporal logics of computations. The computation tree logics CTL and CTL*.

Recommended readings

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

Supplementary readings

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

Slides (posted on Athena)

Branching time temporal logics, Part I

Exercises and selected solutions (posted on Athena)

Selected exercises from the lecture notes:

Section 8.4, pp 132-136

Exercises: 36, 37, 41, 43, 53

Assignments and deadlines

Lecture 12

Date 27/11/2024

Main Topics

Model-checking in CTL. Applications to verification of concurrent systems.

nuXmv: a tool for symbolic model checking

Recommended readings

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

Supplementary readings

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

Slides (posted on Athena)

Branching time temporal logics: full set of slides

Presentation on nuXmv

Exercises and selected solutions (posted on Athena)

Selected exercises from the lecture notes (carried over from Lecture 11):

Section 8.4, pp 132-136

Exercises: 36, 37, 41, 43, 53

Assignments and deadlines

Lecture 13

Date 04/12/2024

Main Topics

Logics for multi-agent systems.

The multi-agent temporal logic ATL.

Recommended readings

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

Supplementary readings

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.

Slides (posted on Athena)

Alternating time temporal logics

Exercises and selected solutions (posted on Athena)

Selected exercises from the lecture notes :

Section 8.5, pp 137-139

Exercises: 61, 64, 66, 67

Assignments and deadlines

Submission of Assignment 3

Lecture 14

Date TBA

Main Topics

Feedback on Assignment 3

Concluding remarks and final discussion on the course

General course details

Schedule time-table

Link to time-table

Departmental course page

Link to departamental course page

Course plan and description

Link to course plan (in Swedish)

Consulting time

By appointment

Lecture notes, handouts, and other reading material

Lecture notes, slides and other reading material will be provided or linked to this page on an ongoing basis.

Exercises

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.

Assignments and reports

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.

Additional readings and exercises

Readings

On Logic

On Logic in AI

On Logic in CS, general

On Logical deduction and Automated reasoning

On Logical methods for program verification

On Temporal logics, general

On Temporal Logics in CS

Logic and fun

To be continued

Queries

If you have any queries on the information above, talk to me or send me an email.

Mail to V.Goranko