Module 19342 (2005)

Syllabus page 2005/2006

06-19342
Logic for Computer Science

Level 2/I

Manfred Kerber
10 credits in Semester 1

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.)

Changes and updates

New module for 2005/06.


Relevant Links

For more information see the module web page at http://www.cs.bham.ac.uk/~mmk/Teaching/LCS/index.html.


Outline

Propositional logic, predicate logic (syntax, semantics and natural deduction), application to program proving.


Aims

The aims of this module are to:

  • introduce the main concepts of classical logic, and to appreciate some of its uses in computer science
  • introduce the basics of reasoning about programs

Learning Outcomes

On successful completion of this module, the student should be able to: Assessed by:
1understand the syntax, semantics, and proof theory of propositional logic, and perform natural deduction proofs Examination, Exercises
2understand the syntax, semantics, and proof theory of predicate logic, and perform easy natural deduction proofs Examination, Exercises
3understand 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:

Approx. 35


Assessment

  • Supplementary (where allowed): As the sessional assessment
  • 1.5 hr examination (80%), continuous assessment (20%). Resit by examination only.

Recommended Books

TitleAuthor(s)Publisher, Date
Logic in Computer Science: Modelling and reasoning about systems (2nd Edition)Michael R A Huth and Mark D RyanCambridge Univ. Press, 2004
Schaum's Outline of Theory and Problems of Logic (2nd Edition)John Nolt, Dennis Rohatyn, Achille VarziMcGraw-Hill, 1998
LogicWilfried HodgesPenguin, 1984

Detailed Syllabus

  1. General motivation, syntax, semantics for atomic formulae, consequence relation, notion of soundness and completeness (2 lectures)
  2. Propositional logic (8 lectures)
    • Connectives
    • Syntax, semantics
    • Examples
    • Natural deduction calculus
  3. First-order logic (4 lectures)
    • Syntax, semantics
    • Natural deduction calculus
  4. Equality (2 lectures)
  5. Reasoning about programs (6 lectures)
    • Specification and partial correctness of programs
    • Hoare calculus
    • Examples

Last updated: 22 Oct 2005

Source file: /internal/modules/COMSCI/2005/xml/19342.xml

Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus