ÐÂÏã¸ÛÁùºÏ²Ê¿ª½±½á¹û

Aims:

The module aims to introduce and familiarise students with logical and mathematical inference. Students learn a number of logical inference methods for classical logics and for non-classical logics.

Intended learning outcomes:

On successful completion of the module, a student will be able to:

1. Understand how axiomatic systems can be used for propositional and predicate logic.
2. Understand the notions of soundness and completeness.
3. Understand how propositional and predicate tableaus work.
4. Have familiarity with other logics, including modal and temporal logics.
5. Analyse algebras of relations.

Indicative content:Ìý

The following are indicative of the topics the module will typically cover:Ìý

Propositional logic, Predicate logic, Modal Logic and Temporal Logic:

• Review of syntax and semantics.
• Deduction and Inference.
• Truth tables.
• Decidability of propositional logic.

Mathematical proofs:

• Proof by contradiction.
• Induction and structured induction.
• Hilbert systems.
• Axioms and inference rules for propositional logic.
• Axioms and inference rules for predicate logic.
• Axioms and inference rules for modal and temporal logics.
• Tableau construction for propositional logic, predicate logic, modal logics.
• Soundness and completeness theorems for first order logic.
• Semi-decidability of first order logic.
• Undecidability of arithmetic.

Algebras of Relations:

• Algebras of binary relations
• Kleene Algebra
• Relation Algebra
• Other Algebras of Relations.

Requisites:

To be eligible to select this module as optional or elective, a student must: ​(1) be registered on a programme and year of study for which it is a formally available; (2) have taken Theory of Computation (COMP0003) and Algorithms (COMP0005); and (3) have some programming experience (as the assessment will require them to implement a program in C).