This page is maintained by Valentin Goranko. Last update: 25/09/2017, 11.00


Logic in Computer Science and Artificial Intelligence (Autumn 2017)

Lecturer: Valentin Goranko

Teaching assistant: Anders Lundstedt

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

Week

Date Main Topics Course notes and readings

Additional readings

Slides Selected exercises Solutions to selected exercises

Assignments and deadlines

36/01

04.09

(NB: no lecture on 07.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 Mondo) Sections 1.1-1.2

Alternatively: Sections 1.1-1.2 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

Provided on Mondo:

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.

 

 

Provided on Mondo.

 
38/02 18.09

Revision on propositional logic:

-- Propositional tableaux.

-- Propositional logical equivalence and negation normal form.

-- Conjunctive and disjunctive normal forms (CNF and DNF).

-- Propositional Resolution.

Lecture Notes on Classical Logic, Ch.2: 1.3, 2.3, 2.5

Alternatively:

Sections 1.3, 2.3, 2.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. 4. Open Course Project, University of Amsterdam

See more references below

Provided on Mondo:

Propositional tableaux

Propositional logical equivalence and negation normal form

Normal forms (CNF and DNF). Propositional Resolution.

 

 

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 Mondo

 

39/03 25.09

 

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

First-order terms and formulae.

Formal semantics of FOL.

Translations between FOL and natural language.

 

 

Lecture Notes on Classical Logic, Sections 3.1, 3.2, 3.3.1-3.3.3

Alternatively:

Sections 3.1, 3.2, 3.3.1-3.3.3 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

See more references below

To be provided on Mondo:

First-order structures and languages

Semantics of FOL.

 

 

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.

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;

 

To be provided on Mondo

 

 

40/04 02.10

Satisfiability, validity, and logical consequence in FOL

Syntax and grammar of FOL.

Logical deduction and deductive systems for FOL: basic concepts.

 

 

Lecture Notes on Classical Logic, Sections 3.3.4-3.3.6, 3.4.1-3.4.5.

Alternatively:

Sections 3.3.4-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

To be provided on Mondo:

Satisfiability, validity, and logical consequence in FOL

Syntax and grammar of FOL.

 

 

TBA

 

 

To be provided on Mondo

 
41/05 09.10

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

To be provided on Mondo:

Semantic tableaux for first-order logic.

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

Prenex normal forms, Skolemization, clausal forms.

 

TBA

To be provided on Mondo

Assignment 1 to be posted on Mondo
41/06

12.10

(NB: this lecture has been moved from Week 42 to 12.10, 13.00-16.00)

Resolution rule for first-order logic.

Term unification.

Resolution with unification in first-order 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

Alternatively:

Sections 4.5, 5.4 from the book Logic as a Tool (available from the SU library)

 

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 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 on Mondo:

Resolution with unification in first-order logic.

Resolution-based Automated Reasoning

Introduction to Logic programming and Prolog (Anders' slides)

TBA

To be provided on Mondo

 

43/07 23.10

Introduction to logical methods for program verification.

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

Practical exercises on Prolog and on Floyd-Hoare logic

The first 2 chapters from: Learn Prolog Now!

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

 

 

 

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

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, in the Lecture notes folder)

 

To be provided on Mondo:

Introduction to Floyd-Hoare logic

TBA

 

 

 

Assignment 1 submission

 

44 / 8 30.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. 99-218, Sections 1,2,4 (To be 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

 

 

To be provided on Mondo:

Introduction to PDL.

TBA

 

 

 

Assignment 2 to be posted on Mondo
45/09 06.11

Transition systems and computations.

Modal logic for transition systems.

Lecture notes on Temporal Logics of Computations (To be provided on Mondo) Chapters 1-4

M. Huth and M. Ryan, Logic in Computer Science modelling and reasoning about systems, CUP, 2004. 2nd ed. Chapter 3.1

 

To be provided on Mondo:

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

TBA

 

 
46/10 13.11

Linear time temporal logics of computations. LTL.

SPIN: tool for LTL model checking.

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

Linear time temporal logics of computations.

Presentation on SPIN

 

TBA

 

Assignment 2 submission
47/11 20.11

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

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

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

 

To be To be provided on Mondo:

Branching time temporal logics

 

 

 

TBA

 

 

Assignment 3 to be posted on Mondo
48/12

 

27.11

 

 

Logics for multi-agent systems. Alternating time temporal logic.

Lecture notes on Temporal Logics of Computations (To be provided on Mondo) Chapter 7

 

To be provided on Mondo:

Alternating time temporal logics

Exam info

TBA

 

 
49/13 04.12 Capita selecta and general revision           Assignment 3 submission
51 19.12 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 provided on Mondo or linked to this page on an ongoing basis.

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