This page is maintained by Valentin Goranko. Last update: 05/12/2016, 11.40 (This page will be updated often, so check it out regularly)


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

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

37/01 12.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 infere

Lecture Notes on Classical Logic, (provided on Mondo) Sections 1.1, 1.2

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:

Revision on propositional logic (as many as needed from the following):

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 19.09

Revision on propositional logic:

-- propositional logical equivalence and negation normal form;

--propositional tableaux.

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

First-order terms and formulae.

Lecture Notes on Classical Logic

Ch.1: 1.3;

Ch.2: 2.3;

Ch.3: 3.1

 

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

See more references below

Provided on Mondo:

Propositional logical equivalence and negation normal form

Propositional tableaux

First-order structures and languages

 

 

From the lecture notes: (Do as many exercises from each group as needed)

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. 3.1.4, p.97-98, 3+4a,e,h; 6, 7a,f,j,m, 10, 11.

 

 

 

Provided on Mondo.

 

39/03 26.09

Formal semantics of FOL.

Translations between FOL and natural language.

Satisfiability, validity, and logical consequence in FOL

 

Lecture Notes on Classical Logic, Sections 3.2, 3.3.1-3.3.3, 3.4.1-3.4.3

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

W. Hodges, Elementary Predicate Logic, Sections 14-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

Provided on Mondo:

Semantics of FOL.

Satisfiability, validity, and logical consequence in 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.

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;

Ex. 3.4.9, p.138-142. Own selection from: 1a,c,e,g,i,k,m,o; 6a,c,e; 7f; 8a,c,e,gi,k; 16; 18a,c,e (only the formalisation and semantic argument) 19a,d

 

Provided on Mondo

 

 

40/04 03.10

Syntax and grammar of FOL.

Logical deduction and deductive systems for FOL: basic concepts.

Semantic tableaux for first-order logic.

Conjunctive and disjunctive normal forms (CNF and DNF). Propositional Resolution.

 

Lecture Notes on Classical Logic, Sections 3.3.4-3.3.6, 3.4.3-3.4.5, 4.2, 2.5

 

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

Provided on Mondo:

Syntax and grammar of FOL.

Semantic tableaux for first-order logic.

Normal forms (CNF and DNF). Propositional Resolution.

 

Ex. 3.3.7, p.118-122. Selection from: 11a,c,e,g,i; 13a,c,f,g,h,j;

Ex. 4.2.4, p.158-162: 1c; 2a,e,g; 4c,d,h,l.

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

Assignment 1 posted on Mondo
41/05 10.10

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

Prenex normal forms, Skolemization, clausal forms.

 

Lecture Notes on Classical Logic, Sections 2.5, 3.4.5-3.4.7, 4.4

 

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

Provided on Mondo:

Propositional Resolution.

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

Prenex normal forms, Skolemization, clausal forms.

 

Ex. 3.4.9, p.138-142. 12a,c,h; 13, 14a,c,e,g,i; 15b,d,f,h;

Ex. 4.4.4, p.173. Ex. 2,4,6,10.

 

Provided on Mondo

 
42/06

17.10

NB: this lecture is moved to 12.10

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

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

 

Provided on Mondo:

Resolution with unification in first-order logic.

Resolution-based Automated Reasoning

Introduction to Logic programming and Prolog (Anders' slides)

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

 

Provided on Mondo

Assignment 1 submission deadline: October 20

43/07 24.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)

 

Provided on Mondo:

Introduction to Floyd-Hoare logic

Provided on Mondo:

Exercises on Prolog

Exercises on Floyd-Hoare logic

 

 

 

 

Assignment 2 posted on Mondo

44 / 8 31.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 (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

 

 

Provided on Mondo:

Introduction to PDL.

Provided on Mondo:

Exercises on PDL and selected answers

 

 

 

 
45/09 09.11

Transition systems and computations.

Modal logic for transition systems.

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

 

Provided on Mondo:

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.

 

Assignment 2 submission deadline: November 10
46/10 16.11

Linear time temporal logics of computations. LTL.

SPIN: tool for LTL model checking.

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

Linear time temporal logics of computations.

Presentation on SPIN

 

Selected exercises from the lecture notes:

Section 8.3, pp 129-131

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

 

Assignment 3 posted on Mondo
47/11 23.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 (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 provided on Mondo:

Branching time temporal logics

 

 

 

Selected exercises from the lecture notes:

Section 8.4, pp 132-136

Exercises: 36, 37, 30, 41, 43, 53

 

 

 
49/12

05.12

NB change of date and venue

 

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

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

 

Provided on Mondo:

Alternating time temporal logics

Exam info

Selected exercises from the lecture notes:

Section 8.5, pp 137-139

Exercises: 61, 64, 66, 67

 

Assignment 3 submission deadline
49 09.12 Exam

 

Class sessions time-table (note changes for the last 4 lectures)

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