The new page for this course is under preparation!
Logic in Computer Science (CS3181)
Quick links:
latest news;
general information;
reading instructions;
schedule;
examination;
latest exercise results;
Dec 13. -
Dec 12.
-
Nov 22. Assignment 7
-
Nov 19. Chapter 9
-
Nov 12. Assignment 6. Results for exercises 3 and 5
-
Nov 9. Sample solutions to assignment 5
-
Nov 6. Chapter 8
-
Nov 4. Deadline for assignment 4 and 5 extended to November 8
-
Oct 18. Chapter 7 and assignment 5
-
Oct 18. Chapter 6, sample solutions to Exercises 1,2,3, new version of Preliminaries (Chapter 2)
-
Oct 11. Assignment 4 and results of Exercises 1,2.
-
Oct 8. Assignment 3.
-
Oct 1. Chapter 5 and assignment 2.
-
Sep 28. Chapter 4 and assignment 1.
The aim of the undergraduate course 'Logic in Computer Science' is to give introduction to logic for computer scientists and show applicability of logic in a number of important areas of computer science.
This is the first time I give this course, so its content and schedule given below may change. I am going to consider (i) propositional logic and satisfiability-checking algorithms; (ii) temporal logic and model checking (iii) foundations of predicate logic and (iv) logic and database query languages.
I expect the material to have an increasing order of difficulty, with propositional logic being the easiest topic, while first-order logic being the most difficult one.
This Web page will contain all up-to-date material on this course. All announcements related to the course will also be posted on the course mailing list. To subscribe to this list, send a message to cs3181-request@cs.man.ac.uk with the subject 'subscribe'.
There will be 24 lectures in total, but some of them may be replaced or complemented by feedback sessions on exercises (see below). The accessment of this course consists of assessed exercises during the course (20%) and an examination (80%). Each accessed exercise has an associated deadline given in the table below. The solutions can be given to me as a lecture or left at my office (2.46). Computer exercises can be written in any of the following languages: ML, Prolog, C++, C, Java, Perl, or Python, and properly documented. Use of ML or Prolog is strongly recommended as being the easiest.
There will be handouts put on the Web after each lecture. If I use slides during a lecture, a copy of the slides will be put on the Web too. I advise to make notes during the lecture, since the material said or presented on the whiteboard may not find its way to either the slides or the handouts. The handouts will be in the form of a draft textbook, and will be continuously updated.
The reading material (or the handouts) will consist of several chapters (starting with number 3) put on the Web as soon as they are ready. I will also make some copies and put them in a box on my office door. The presentation may be sketchy, but all the important notions will be formally defined. In addition to these chapters, there will be a chapter containing the general preliminaries (Chapter 2). For example, it will contain definition and terminology related to binary relations, trees and rewrite rule systems. I especially recommend to read and understand the definitions related to the rewrite rule systems, since they will be used throughout the course to represent algorithms and also for other purposes.
Your comments on the text are appreciated. Comments should be submitted by email to voronkov@cs.man.ac.uk.
The current version of the preliminaries is available here. Don't forget to reload this document from time to time to get the latest version.
For your convenience, I also provide the index for the reading material. The index will change every time a new material has been added.
Note. Assignment 8 is not compulsory, so there is no deadline for it.
I suggest that you try to solve it, since this may help you to cope with the exam.
I did not teach this course before, so there are no past year exams available.
For your convenience, I compiled a document All You Have to Know About the Examination, which contains all the relevant information.
