COMP60332 Automated Reasoning and Verification syllabus 2019-2020
Automated reasoning plays an important role in computer science and practical areas of computing such as software and hardware verification, program analysis, security, semantic web and AI. For example, in web and agent technologies logical and automated reasoning methods are used for the intelligent processing of large ontologies, for decision making based on knowledge bases of structured data, and for formal specification and verification of web services. Another application of automated reasoning is in software and hardware verification, in particular, automated reasoning tools are successfully used in large software and hardware companies such as Intel and Microsoft. An important part of the systems development process concerns reasoning about the behaviour of systems in order to verify the correctness of the behaviour. The main motivation of the course is the study and development of general and efficient techniques, which form the basis of state-of-the-art automated reasoning systems and verification tools.
The course aims at providing an understanding of propositional reasoning and first-order reasoning, giving an introduction to theoretical concepts and results that form the basis of current automated reasoning systems based on DPLL and resolution, and discussing verification as an important application domain.
The following lists the topics to be covered in the course. The teaching days will contain a mixture of lectures, examples classes, supervised laboratories and self-study. The number of lectures for each topic are given in brackets.
* Introduction (1)
* Orderings, multi-sets (1)
* Propositional reasoning
+ Language of propositional logic, semantics, truth tables (1)
+ Satisfiability, validity, equivalence, decidability (1)
+ Normal forms, CNF, clauses, optimised normalisation (1)
+ Propositional resolution (1)
+ DPLL and SAT-solving with backjumping, lemma learning (2)
+ Logical modelling (1)
* General first-order reasoning
+ Language of first-order logic, semantics (2)
+ Normal forms, clauses (1)
+ Herbrand interpretations (1)
+ Soundness, literal & clause orderings, saturation (1)
+ Model construction (1)
+ Unication for general resolution (1)
+ Basic general resolution, ordering & selection refinements (2)
+ Redundancy elimination (1)
+ Using SPASS (lab)
+ LTL (1)
+ bounded model checking (1)
Lecturers will be interspersed with example classes and labs on teaching days
Example classes will take place on teaching days
Labs will take place on teaching days
Exercise classes; assessment and feedback on written assignments.
- Assessment written exam (2 hours)
- Lectures (24 hours)
- Practical classes & workshops (16 hours)
- Analytical skills
- Problem solving
- Written communication
On successful completion of this unit, a student will be able to:
- A basic understanding of the computational needs of modern biology.
- Develop an understanding of the problems inherent in communicating with scientists from a different discipline.
- Develop the ability to reflect upon and synthesize a range of computational techniques to develop effective problem solving strategies in an unfamiliar problem domain.
- Develop the ability to communicate these strategies to non-specialists.
|Essence of logic||Kelly, John||0133963756||Pearson Education Limited||1997||✖|
|Mathematical logic for Computer Science (3rd edition)||Ben-Ari, Mordechai||9781447141280||Springer||2012||✖|
|First-order logic and automated theorem proving (2nd edition)||Fitting, Melvin||0387945938||Springer||1995||✖|
|Logic for Computer Scientists||Schoning, Uwe||9780817647629||Birkhauser Verlag AG||2008||✖|
Course unit materials
Links to course unit teaching materials can be found on the School of Computer Science website for current students.