This page is maintained by Valentin Goranko. Last update: 16/09/2019, 17.00 CET


FILOGX: Logic in Computer Science and Artificial Intelligence (Autumn 2019)

Lecturer: Valentin Goranko

Teaching assistant: Anders Lundstedt

Tentative course outline and schedule (to be updated before and during the course):

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

The Carnap book

John Slaney, The Logic Notes

See more references below

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.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 (moved to Lecture 2)

Ex.1.2.4, p. 24-26: 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.30-31: 2a,f; 3g,h,j; 4a,e.

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

 

 

Provided on Athena

 

38/03 16.09

Classical first-order logic (FOL): basic consepts. First-order structures and languages.

First-order terms and formulae.

Formal semantics of FOL. Evaluation games.

Translations from FOL to natural language.

Translations from natural language to FOL.

 

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 1-15, in: D.M. Gabbay and F.Guenthner (eds.), Handbook of Philosophical Logic. 2nd edition. Vol. l , 1-129. 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:

First-order structures and languages. First-order terms and formulae. Semantics of FOL. Evaluation games. Translations between FOL and natural language.

 

From the lecture notes:

Ex. 3.1.4, p.97-98, 3+4a,e,h; 6, 7a,f,j,m, 10, 11.

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)

Provided on Athena.

 

 

39/04 26.09

 

Syntax and grammar of FOL.

Satisfiability, validity, and logical consequence in FOL

 

 

 

Lecture Notes on Classical Logic, Sections

3.3.1-3.3.6, 3.4.1-3.4.5.

 

Alternatively:

Sections

3.3.1-3.3.6, 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

 

See more references below

To be provided:

Syntax and grammar of FOL.

Satisfiability, validity, and logical consequence in FOL

 

 

 

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;

 

 

 

 

To be provided

 
40/05 30.09

Logical deduction and deductive systems for FOL: basic concepts.

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 4.2, 3.4.5-3.4.7, 4.4

Alternatively:

Sections 4.2, 3.4.5-3.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

To be provided

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.

To be provided

Assignment 1 to be posted
41/06

07.10

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

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 First-Order 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 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

 

To be provided

 

41/07 10.10

Introduction to logical methods for program verification.

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

Introduction to Logic programming and Prolog. (by Anders Lundstedt)

 

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

Chapter 1 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 256-305 (available on Mondo. Book available from the SU library. Chapters 1 and 3 available electronically from the authors website)

 

 

To be provided:

Introduction to Floyd-Hoare logic

Introduction to Logic programming and Prolog (Anders' slides)

To be provided

Exercises on Floyd-Hoare logic

Exercises on Logic programming and Prolog

 

 

 

To be provided

 

 

42/ 08 14.10

Propositional dynamic logics of programs (PDL).

Practical introduction to Prolog (by Anders Lundstedt)

 

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 (To be provided)

The first 2 chapters from: Learn Prolog Now!

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

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

 

To be provided

Introduction to PDL

 

To be provided

Exercises on PDL

Exercises on Logic programming and Prolog

 

 

 

To be provided

Assignment 1 submission

Assignment 2 to be posted

44/09 28.10

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 (To be provided) 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

 

To be provided:

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.

To be provided

Assignment 2 submission
45/10 04.11

The linear time temporal logic of computations LTL.

Lecture notes on Temporal Logics of Computations (To be provided) 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

 

To be provided:

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

To be provided

 
46/11 11.11

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

 

 

Lecture notes on Temporal Logics of Computations (To be provided) 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

 

 

To be provided

Branching time temporal logics

 

 

 

 

Selected exercises from the lecture notes:

Section 8.4, pp 132-136

Exercises: 36, 37, 41, 43, 53

 

To be provided

Assignment 3 to be posted
47/12

 

18.11

 

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

nuXmv: a tool for symbolic model checking (Anders)

Lecture notes on Temporal Logics of Computations (To be provided) 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

To be provided:

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 132-136

Exercises: 36, 37, 41, 43, 53

To be provided

 
48/13 25.11

Logics for multi-agent systems.

The multi-agent temporal logic ATL

 

Concluding remarks on the course.

Exam info.

Lecture notes on Temporal Logics of Computations (To be provided) 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 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.

 

 

To be provided:

Alternating time temporal logics

Exam info

Selected exercises from the lecture notes:

Section 8.5, pp 137-139

Exercises: 61, 64, 66, 67

To be provided Assignment 3 submission
49/14 02.12

Feedback on Assignment 3

Final discussion and group consultation on the course

 

TBA TBA

Exam

 

 

Class sessions time-table

Link to the departmental course description page

Link to the course plan (in Swedish)

Consulting time: by appointment

Lecture notes, handouts, and other reading material

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

Additional supplementary sources and readings:

Here are some links to general (optional) additional 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.

Exercises, assignments, and reports

Lists of exercises will be To 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 selected exercises will be to be posted on this site weekly and will be discussed before the lectures.

Assignments and reports

There will be 3 mandatory written assignments during the course, each consisting of a set of exercises. Two of the assignments will include practical sections. The assignments will be to be posted on Mondo 2 weeks before the submission deadline. Students must do these exercises individually and prepare written reports with their solutions. Strict dates for submission of the assignment reports will apply. The assignments will be checked and corrected by the lecturer, returned to the students for feedback, and then returned back to the lecturer. These assignments will be taken into account in the final grade.

Exam and final grade

The assessment of the students will be based on a written exam, and the final grade will be assigned as an aggregate of the exam grade and the assignment reports of the student.

Queries

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