06-02316 Logic (SEM1A6)

Dr Manfred Kerber

10 credits, Semester 2

button bar

Aims

Objectives

On completion of this course, the student should be able to:

Prerequisites

None.

Teaching Methods

Two lectures and one exercise class per week, throughout the semester.
Notes on this course are provided, with examples and exercises. The lectures emphasise the key points, explain in detail the concepts, and go through detailed examples.

Assessment

10% continuous: there are assessed exercises each week, which are to be handed in during the exercise class. One percentage point of the module is given each week for a serious attempt at the assessed exercises.
90% written examination.
Re-assessment is by examination (100%) in the summer.

Recommended Books

Title Author(s) Publisher Comments
Logic in Computer Science: Modelling and reasoning about systems Michael R A Huth and Mark D Ryan Cambridge University Press 2000 Key Text
Introduction to Knowledge Base Systems, 2nd Edition Richard A. Frost Collins 1986 Further Reading
Reasoned programming K. Broda, S. Eisenbach, H. Khoshnevisan, S. Vickers Prentice Hall 1994 Further Reading
Program construction and verification Roland C. Backhouse Prentice Hall 1986 Further Reading


Detailed Syllabus and Relevant Links

The following courses are currently planned, modifications possible. Slides and Exercises will be made available as gzipped PostScript files and pdf files after copies have been handed out in the lecture. Before you print anything out, please check whether there are spare copies left in the School library. You can directly preview the files (locally) by something like:
zcat /bham/ftp/pub/authors/M.Kerber/Teaching/Logic/e8.ps.gz | ghostview -
and print them by something like:
zcat /bham/ftp/pub/authors/M.Kerber/Teaching/Logic/e8.ps.gz | lpr -
On a double sided printer you can get eight pages on one sheet, using the psnup command, e.g.
zcat /bham/ftp/pub/authors/M.Kerber/Teaching/Logic/l8.ps.gz | psnup -6 > [print-file] ; lpr-lj5 -P [double-sided printer] [print-file]
Files are also available in pdf-format and can be previewed with the AcrobatReader, which can be downloaded from Adobe's web site for free.

Week Content Preparation
[Huth/Ryan]
Slides Exercises
1 Difference between syntax and semantics. Informal introduction of interpretation of atomic formulae, relationship to data bases, Boolean expressions in programming languages 45-49 l1.ps.gz; l1.pdf e1.ps.gz; e1.pdf
2 Formal semantics for atomic formulae, consequence relation, notion of soundness and completeness 129-131 l2.ps.gz; l2.pdf e2.ps.gz; e2.pdf
3 Conjunction 1-8, 48 l3.ps.gz; l3.pdf e3.ps.gz; e3.pdf
4 Implication, disjunction, natural deduction proofs 9-18 l4.ps.gz; l4.pdf e4.ps.gz; e4.pdf
5 Negation, propositional logic in overview 19-38 l5.ps.gz; l5.pdf e5.ps.gz; e5.pdf
6 Variables, quantification 119-136 l6.ps.gz; l6.pdf e6.ps.gz; e6.pdf
7 Soundness, completeness, undecidability theorems for first-order logic (without proofs) 90-96, 140-147 l7.ps.gz; l7.pdf e7.ps.gz; e7.pdf
8 Limitations of first-order logic, proof by structural induction 51-56 l8.ps.gz; l8.pdf e8.ps.gz; e8.pdf
9 Proof by induction: more examples. Program verification, partial and total correctness; Hoare triples; a simple programming language. 51-56; 216-230 l9.ps.gz; l9.pdf e9.ps.gz; e9.pdf
10 Program verification (Cont'd): rules for composition and assignment. The rule for If-statements. Invariants and the rule for while-loops. 230-252 l10.ps.gz; l10.pdf e10.ps.gz; e10.pdf
11 Revision     no exercise class
12 Revision     e11.ps.gz; e11.pdf

Files with all slides are available as gzipped PostScript (1804kB) and pdf (5687kB).

In the academic year 1999/2000, the lectures takes places:
Mondays 9-10 in Main LT, Arts and
Wednesdays 11-12 in Hills 212.
The tutorials are:
Mondays 12-13 in G31, MechEng.

Model solutions to the exercises are distributed at the end of the tutorial sessions on Mondays, alternatively they are available from the lecturer during his office hours.


If you want to have a look at the 1999 exam paper you can find here a gzipped PostScript and a pdf version. Past papers on all courses of the last years are available in the School library as well. Please be aware that the past exam papers on the logic course were compiled by Mark Ryan and that the course had a different structure at that time.

You can run (under solaris) the TPS system by
setup UMS
tps
For details see the back of worksheet 5.
A logic tutor can be started by
setup Poplog
pop11 +boole

button bar


Maintained by M.Kerber@cs.bham.ac.uk
School of Computer Science
The University of Birmingham

Last update 29 March 2000