In this module you will have the opportunity to:
- learn about language and semantics of propositional and first-order logic
- explore the user of logic for modelling rigorously human reasoning
- apply various semantic methods for proving validity of arguments and logical equivalences
- study natural deduction and resolution for constructing correct proofs
- investigate soundness and completeness of natural deduction
- apply first-order logic to program specification
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
- Use logic to prove properties over sets and relations
- Construct proofs using proof systems presented
- Apply induction to construct soundness and completeness proofs
This module covers the following topics in relation to both propositional and first-order logic:
- Informal and formal semantics
- Validity, satisfiability
- Semantic entailment
- Proof systems
- Soundeness and Completeness proofs
- Many-sorted logic
- Applications in program specification
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 weekly 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, discrete mathematics, algorithm design and program reasoning. The remaining exercises are intended for you to use for self-study. Additional exercises will be provided and intended for you to use for self-study and revision. The lectures will introduce the theoretical foundations of logic and show you how logic can be used to formalise and reason about English sentences. Particular emphasis will also be placed on the use of logic as a vehicle for specifying properties (e.g. sets properties and specifications of programs), and on the correctness and validity of proofs.
The Piazza Q&A web service will be used as an open online discussion forum for the module.
There will be an assessed test that contributes 15% of the mark for the module. There will be a final written exam, which counts for the remaining 85% 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. These exercises will be issued approximately every two weeks and feedback will be returned the week after submission. The test exercise will be marked and returned to you; the feedback will mostly be limited to a mark for each question attempted.
Module leadersDr Dalal Alrajeh
Professor Alessandra Russo