06-02316 Logic (SEM1A6)
|Dr Manfred Kerber||
10 credits, Semester 2
On completion of this course, the student should be able to:
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.
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.
|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|
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.
|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|
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
Maintained by M.Kerber@cs.bham.ac.uk
School of Computer Science
The University of Birmingham
Last update 29 March 2000