Course co-ordinator(s): Prof Fairouz Kamareddine (Edinburgh).
- To give an introduction to and an appreciation of the basic principles and techniques of logic and proof fundamental to Computer Science.
- Introduce the λ-calculus, how computable functions are represented in the λ-calculus, basic theoretical properties of the λ-calculus, and the relevance of the λ-calculus to computer science.
Course Description: Link to Official Course Descriptor.
- Logic & proof: propositional calculus – truth tables, predicate calculus, inference rules, soundness, completeness, validity, satisfiability, reasoning and calculating with propositions.
- Lambda calculus: syntax, notation, bound & free variables and α-conversion and substitution, reduction and computation, representing computable functions, theoretical properties.
Learning Outcomes: Subject Mastery
Understanding, Knowledge and Cognitive Skills Scholarship, Enquiry and Research (Research-Informed Learning)
- To demonstrate an understanding of the principles of propositional and predicate calculus.
- To foresee the role of argument in logical reasoning.
- Practice in formulating and proving arguments using formal logic
- Knowledge of lambda calculus
- Understanding of different variable techniques (de Bruijn indices, combinator variables)
- Understanding of variable binding and capture-free substitution
- Knowledge of how to represent computations in the λ-calculus
Learning Outcomes: Personal Abilities
Industrial, Commercial & Professional Practice Autonomy, Accountability & Working with Others Communication, Numeracy & ICT
- To be able to formulate statements as well formed formulae in propositional and predicate calculus.
- To be able to express arguments/problems in propositional and predicate calculus.
- To be able to construct formal proofs of logical arguments.
- To be able to think about the meaning of programs mathematically
Assessment: Examination: (weighting – 70%) Coursework: (weighting – 30%)
Re-assessment: Examination: (weighting – 100%)
SCQF Level: 9.