Logic & Reasoning (JMC)

Module aims

In this module you will have the opportunity to:
- learn about syntax, semantics and proof systems of first-order logic
- learn how to translate human natural language to formal logic, and vice versa
- apply various semantic methods for proving validity of arguments and logical equivalences
- use logic to reason about program behaviour through the use of pre, post and mid conditions and invariants
- use induction to reason about recursive programs
 

Learning outcomes

Upon successful completion of this module you will be able to:
- Recall the definitions of the classical logics and logical systems
- Read, parse and evaluate logical formulas
- Formalise English text into first-order logic, and vice versa
- Construct proofs using proof systems presented
- Provide suitable pre, post and mid conditions and loop variants and invariants to program fragments
- Use structural induction to reason about the correctness of functional programs
 

Module syllabus

This module covers the following topics:
- Syntax, semantics and proof systems for first-order logic
- Equivalences of formulae
- Soundness and completeness
- Applications of logic and induction to reasoning about programs

 

Teaching methods

The material will be taught through traditional lectures, backed up by formative exercises designed to reinforce the material as it is taught. Some of these exercises will be covered in small-group tutorials, Personal Maths Tutorials (PMTs), which are one-hour tutorials run by academics tutors and Undergraduate Teaching Assistants (UTAs). These tutorials encourage group discussions and group problem solving designed to reinforce your understanding of key topics in logic and program reasoning. Additional exercises will be provided for self-study and revision.

An online service will be used as a discussion forum for the module.

Assessments

There will be an assessed exercise that contributes 20% of the mark for the module. There will be a final written exam, which counts for the remaining 80% of the marks. The formative exercises selected for the PMT tutorials will be assessed by your academic tutor and UTA. This assessment does not count to your final degree mark, but is intended to give you an indication of how you well you are assimilating the material taught and how effectively you can apply that material to solving previously unseen problems.
               
Detailed feedback, both written and verbal, will be given on the formative exercises covered in the PMT tutorials. Feedback will be returned the week after submission. The assessed exercise will be marked and returned to you with feedback that is appropriate to the exercise.

Reading list

Supplementary reading

Module leaders

Dr Dalal Alrajeh
Dr Mark Wheelhouse
Professor Sophia Drossopoulou

View the module reading list (Leganto)