Module 19342 (2006)
Syllabus page 2006/2007
06-19342
Logic for Computer Science
Level 2/I
Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus
The Module Description is a strict subset of this Syllabus Page. (The University module description has not yet been checked against the School's.)
Relevant Links
For more information visit
http://www.cs.bham.ac.uk/~ard.
Outline
The module presents the proof theory and the model theory of the propositional calculus, the predicate calculus and a Floyd-Hoare logic.
Aims
The aims of this module are to:
- present the proof theory and the model theory of first-order logic with identity
- present the proof theory and the model theory of a Floyd-Hoare logic
Learning Outcomes
| On successful completion of this module, the student should be able to: | Assessed by: | |
| 1 | understand the syntax, semantics, and proof theory of propositional logic, and perform proofs | Examination, Exercises |
| 2 | understand the syntax, semantics, and proof theory of predicate logic, and perform proofs | Examination, Exercises |
| 3 | understand basic notions of the Hoare calculus | Examination, Exercises |
Restrictions, Prerequisites and Corequisites
Restrictions:
None
Prerequisites:
None
Co-requisites:
None
Teaching
Teaching Methods:
2 lectures and 1 exercise class per week.
Contact Hours:
Assessment
- Sessional: 1.5 hr examination (80%), continuous assessment (20%).
- Supplementary (where allowed): By examination only.
Recommended Books
| Title | Author(s) | Publisher, Date |
| Z: An Introduction to Formal Methods (second edition) | Antoni Diller | Wiley , 1994 |
| Logic: A Foundation for Computer Science | Volker Sperschneider and Grigorios Antoniou | Addison-Wesley , 1991 |
| Programming: The Derivation of Algorithms | Anne Kaldewaij | Prentice Hall , 1990 |
| Logic for Information Technology | Antony Galton | Wiley , 1990 |
| Proofs and Refutations | Imre Lakatos | Cambridge University Press , 1976 |
Detailed Syllabus
- Nature of logic
- Propositional calculus:
- syntax
- proof theory
- model theory
- soundness, completeness and decidability
- Predicate calculus with identity:
- syntax
- proof theory
- model theory
- soundness, completeness and undecidability
- Floyd-Hoare logic:
- syntax
- proof theory
- model theory
Last updated: 28 Jun 2006
Source file: /internal/modules/COMSCI/2006/xml/19342.xml
Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus