![]() | Computer Science |
| Manfred Kerber | 10 credits in Semester 1 |
| Wednesdays | (Lecture) | 9:00-11:00 | LT 112 Chemical Engineering |
| Thursdays | (Exercise Class) | 9:00-10:00 | LT G28 Mechanical Engineering |
| Title | Author(s) | Publisher | Comments |
| Logic in Computer Science: Modelling and reasoning about systems (2nd Edition) | Michael R A Huth and Mark D Ryan | Cambridge Univ. Press, 2004 | Further Reading |
| Schaum's Outline of Theory and Problems of Logic (2nd Edition) | John Nolt, Dennis Rohatyn, Achille Varzi | McGraw-Hill, 1998 | Further Reading |
| Logic | Wilfried Hodges | Penguin, 1984 | Further Reading |
| Week | Lectures | Exercises |
| 1 | What is logic, motivation, reasoning about programs, informal Hoare triples
Handout: html, ascii, gzipped PostScript, pdf. | gzipped PostScript, pdf |
| 2 | What is a proof, semi-formal reasoning (assignment, composition, if-then-else)
Handout: html, ascii, gzipped PostScript, pdf. | gzipped PostScript, pdf |
| 3 | Formal reasoning (assignment, composition, if-then-else), weakening, motivation for propositional logic
Handout: html, ascii, gzipped PostScript, pdf. | gzipped PostScript, pdf |
| 4 | Propositional logic, syntax, semantics
Handout: html, ascii, gzipped PostScript, pdf. | gzipped PostScript, pdf |
| 5 | Truth tables, consequence relation
Handout: html, ascii, gzipped PostScript, pdf. | gzipped PostScript, pdf |
| 6 | Boole algebra, natural deduction
Handout: html, ascii, gzipped PostScript, pdf. | gzipped PostScript, pdf |
| 7 | Natural deduction
Handout: html, ascii, gzipped PostScript, pdf. | gzipped PostScript, pdf |
| 8 | Derived rules, First-order logic (syntax, encodings)
Handout: html, ascii, gzipped PostScript, pdf. | gzipped PostScript, pdf |
| 9 | First-order logic (semantics, natural deduction)
Handout: html, ascii, gzipped PostScript, pdf. | gzipped PostScript, pdf |
| 10 | Equality, restricted Hoare plus natural deduction
Handout: html, ascii, gzipped PostScript, pdf. | gzipped PostScript, pdf |
| 11 | Hoare logic with while
Handout: html, ascii, gzipped PostScript, pdf. | gzipped PostScript, pdf |
Errata can be found here.
Information about the tutorials
The module is
to 20% continuously assessed, 2% every week in weeks 1 through 10. The
2% are subdivided into 100% of which typically 40%-50% are for easy
exercises, which should give you enough points for a pass mark.
Exercises of medium difficulty can give you another 20%-30% and bring
you in the range of a second class mark. You need to address
successfully all exercises in order to come in the range of a first
class mark. It is necessary that you revise the material and prepare
yourself for the exercise classes in order to successfully work on the
exercises during the Thursdays exercise classes. Exercises will be
handed out at the start of the exercise class and collected at the
end. You are encouraged to collaborate in a small group of two or
three students and and will make a joint submission at the end of each
exercise class which will be evaluated as a team. While you have to
collaborate within your team, collaboration on the exercises between
different teams is not permitted. You can use presence of the tutors
to clarify matters where you've got stuck.
Clearly write your registration numbers on each sheet of your
submission. No registration number - no points. Do not write your
names on your submission. Submissions with names will be marked but
not returned.
Attendance to the exercise classes is compulsary. If you do not attend the exercise classes, in all likelyhood you will fail the examination. If you actively do attend, however, you will be well prepared and should pass the examination
Some hints about learning
Maintained by:
Manfred Kerber,
School of Computer Science,
The University of Birmingham
Last update: 12.12.2005.
The URL of this page is
http://www.cs.bham.ac.uk/~mmk/Teaching/LCS/index.html.