CS 5209 - Foundation in Logic and Artificial Intelligence, Semester 2 2009-2010

News

Slides 11 are out, see below. Also note the updated assessment section at the bottom.

Brief Description

The module aims to cover both classical and non-classical logics focusing on their deductive and algorithmic aspects. It introduces mathematical logic as a means for specifying, verifying and reasoning about computer programs. Its emphasis, in contrast to other similar logic modules, is on how logic can be used to represent computational problems, how these representations can be proved correct and how they can be executed on a computer. Topics covered include classical logic theories, logic programming, and an introduction program specfication and verification. Propositional calculus, predicate calculus, and temporal logic are fully covered with emphasis on their specification, verification, deductive and algorithmic aspects.

Textbook

The textbook for the module is: 
Logic in Computer Science
Michael Huth and Mark Ryan
2nd Edition
Cambridge University Press
See publisher's webpage on the book

Material

The module material (slides, covered book chapters) is accessible in the following table.

Lecture Date Subject Slides Notes
01 14/1 Introduction and Propositional Calculus (Part 1) Slides 01 in color
Slides 01 in B/W 		Sections 1.1 and 1.2
02 20/8 Propositional Calculus (Part 2)
Automated Theorem Proving 		Slides 02 in color and B/W
 Sections 1.3, 1.4, 1.5, 1.6.1
03 28/1 SAT solving; inductive definitions Slides 03 in color and B/W
Slides 03b in color
and B/W
 -
04 4/2 Automated Theorem Proving Coq proof script demonstrated during lecture
Coq library needed for proof script 		Coq for Windows
Coq for UNIX (sources)
05 11/2 Predicate Logic Slides 05 in color and B/W
 Sections 2.1, 2.2, 2.3, 2.4, 2.5
06 25/2 Predicate Logic II Slides 06 in PDF and Powerpoint
 Coq proof script demonstrated during lecture
07 4/3 Program Verification I Slides 07 in color
Slides 07 in B/W 		Chapter 4
08 11/3 Program Verification II Slides 08 Part I in color
Slides 08 Part I in B/W
Slides 08 Part II in PDF
Slides 08 in PPTX
 Chapter 4
09 18/3 Separation Logic Slides 09 in PDF
Slides 09 in PPTX
 -
10 25/3 Modal Logic I Slides 10 in color
Slides 10 in B/W
 Sections 5.1, 5.2, 5.3
11 1/4 Modal Logic II Slides 11 in color
Slides 11 in B/W
 Sections 5.4, 5.5
12 8/4 The lambda calculus Slides 12
 -

Assignments

Two assignments are distributed online on this web site. Submission as indicated in the assignments.

Assignment Date handed out Time due Assignment Solution
Assignment 1
Coq library needed for homework
Coq script (to be completed for homework) 		8/2 25/2, 5:30pm not yet available
Assignment 2 (Coq part):
Coq script (to be completed for homework)
Coq library (v2.0) needed for homework 		25/3 7/4, 10:00pm not yet available
Assignment 2 (paper part):
Assignment 2
 30/3 8/4, 5:00pm not yet available

More Module Information

Lectures
Lectures are taking place in COM1/212 on Thursdays from 6:30 to 8:15 pm.
The first lecture is on Thursday, January 14, 2010.
Workload
2-0-0-2-6
Explanation: A-B-C-D-E
A: no. of lecture hours per week
B: no. of tutorial hours per week
C: no. of lab hours per week
D: no. of hours for projects, assignments, fieldwork etc per week
E: no. of hours for preparatory work by a student per week
Assessment
Final exam: 70% (approx.)
Assignments: 30% (approx.); each of the two assignments counts for about 15%
Final Exam
29/4, morning, 2 hours, open book. The exam will be held in the labs, and there will be Coq proof components in the exam.
Instructors

Martin Henz and Aquinas Hobor