CS143-15 Logic and Automata
Introductory description
This module introduces students to formal methods for describing and analysing the behaviour of computational systems.
Module aims
To introduce students to basic connections between mathematical logic, formal languages, automata theory and verification by model checking. Students will also learn and practise proof techniques for reasoning about the limits of various computational models, including concepts such as the pumping lemma and diagonalisation.
Outline syllabus
This is an indicative module outline only to give an indication of the sort of topics that may be covered. Actual sessions held may differ.
Propositional logic and predicate logic, proofs, semantics, regular languages, finite automata, non-determinism, regular expressions, pumping lemma, closure properties, Turing-recognisable languages, Turing machines, decidability, reducibility.
Learning outcomes
By the end of the module, students should be able to:
- Construct and reason about proofs in a variety of logics.
- Apply logic to specify and verify computing systems.
- Specify formal languages and translate between various forms of formal language descriptions.
- Argue that given formal languages are (or are not) regular.
- Understand basic connections between expressive power of some logics and computational models.
Indicative reading list
(a) W. Thomas. Languages, Automata and Logic, Handbook of Formal Languages, volume 3, Springer-Verlag, 1997.
(b) M. Sipser, Introduction to the theory of computation, Cengage Learning, 2013.
(c) J. E. Hopcroft; R. Motwani; J. D. Ullman, Introduction to automata theory, languages, and computation, Pearson, 2014.
(d) B. Khoussainov and A. Nerode, Automata Theory and its Applications. Progress in Computer Science and Applied Logic, Volume 21. Birkhauser, 2001.
(e) M. Fitting, First-order logic and automated theorem proving, Springer-Verlag, 1996.
Subject specific skills
- Formal reasoning about computer systems, languages and proofs. Theory and practice relating to reliability of systems form a vital part of computer science.
- Formally describing, reasoning about and comparing various computational models. Applied in the study of complexity of computational problems.
Transferable skills
Critical Thinking, problem-solving, ability to define problems, design solutions and conduct mathematically rigorous analysis of possible solutions .
Study time
| Type | Required |
|---|---|
| Lectures | 30 sessions of 1 hour (20%) |
| Seminars | 9 sessions of 1 hour (6%) |
| Private study | 109 hours (73%) |
| Assessment | 2 hours (1%) |
| Total | 150 hours |
Private study description
Inclusive of preparation for seminars, background reading, coursework assignment and revision.
Costs
No further costs have been identified for this module.
You do not need to pass all assessment components to pass the module.
Assessment group D
| Weighting | Study time | Eligible for self-certification | |
|---|---|---|---|
| Programming Assignment | 20% | Yes (extension) | |
|
Programming Assignment This assessment is eligible for self-certification (extension). |
|||
| In-person Examination | 80% | 2 hours | No |
|
Final Examination (written)
|
|||
Assessment group R
| Weighting | Study time | Eligible for self-certification | |
|---|---|---|---|
| In-person Examination - Resit | 100% | No | |
|
Resit Examination
|
|||
Feedback on assessment
Marks, feedback on Tabula.
Courses
This module is Core for:
-
UCSA-G500 Undergraduate Computer Science
- Year 1 of G500 Computer Science
- Year 1 of G500 Computer Science
- Year 1 of G500 Computer Science
-
UCSA-G503 Undergraduate Computer Science MEng
- Year 1 of G500 Computer Science
- Year 1 of G500 Computer Science
- Year 1 of G503 Computer Science MEng
- Year 1 of G503 Computer Science MEng
- Year 1 of UCSA-I1N1 Undergraduate Computer Science with Business Studies