COMP60121: Automated Reasoning (2009-2010)

Announcements

• 7 Jan 2010:
  There will be a revision session on Renate's part of the course on Thursday, 14 January at 14:00-15:00 in Room 2.15.
• 9 Dec 2009:
  There are two typos in the exercise sheets for week 5 (to be handed out on 10 Dec):
  • Assessed Coursework, p. 10, Q. 5(ii): C and D denote non-empty clauses which do not have any first-order variables in common (insert a 'not').
  • Unassessed Exercises, p. 8, Q. 4: ?? should be 2.
• 25 Nov 2009:
  Lectures of Part II on "Advanced Topics" start at 2pm on Thursday, 26 November 2009.

Course description

Follow this link for the course unit description, giving details about the aims and learning outcomes of the course, reading material, assessment, and the syllabus.

• Link to ACS Syllabus

Lecturers

• Renate Schmidt
• Andrei Voronkov

Locations and times

• Times: 9:00-17:00 on Thursdays, 12 November - 10 December.
• Venues: Lectures and exercise classes will be in Room 2.19, unless otherwise stated. The labs will be in the MSc lab (2.25a & 2.25b).

Coursework

Handing in your work

Please hand in your written coursework as a hard copy to the Student Support Office, Room LF21.

Slides

• Slides of introductory talk: PDF.
• Updated slides for Part II:
  • Week 3: PDF (4 pages on one)
  • Week 4: PDF (4 pages on one)
  • Week 5: PDF (4 pages on one)

Other resources

• SPASS Website
• SPASS Tutorial
• MSPASS Website

Pre-requisites

Familiarity with propositional logic (also known as classical logic or Boolean logic).

Knowledge of first-order logic and some logic programming experience would be some advantage, but is not essential.

To refresh your knowledge on propositional logic, and also first-order logic, we recommend

• Kelly, J. The Essence of Logic. Pearson.
• Almost any introductory level textbook on Automated Reasoning, Artificial Intelligence, KR&R, Logic, foundations of CS.

To refresh your knowledge on sets, relations and function we recommend

• Chapter 5.2 in Cormen, T. H. and Leiserson, C. E. and Rivest, R. L. (1992), Introduction to Algorithms. The MIT Electrical Engineering and Computer Science Series, MIT Press.
• Chapter 1.1 and 1.3 of "Interactive Real Analysis". This website includes interactive exercises with answers.
• Any book on the mathematical foundations of CS or discrete mathematics.

Reading material

The course does not follow a specific book: copies of the slides are made available.

Recommended reading material is listed in the course unit description in the ACS Syllabus. Further references may be given during lectures.

There is no need to buy a book. All books are available in the Resources Centre Library or the main library.

Assessment

60% coursework, 40% exam