Automated Reasoning and Verification
|Unit level:||Level 6|
|Teaching period(s):||Semester 2|
|Offered by||School of Computer Science|
|Available as a free choice unit?:||Y
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.
Automated reasoning has a wide range of applications fromproving mathematical theorems automatically to verification of hardware and software. For example, major software and hardware industries such as Microsoft and Intel intensively use automated reasoning methods in verification of their products.
This course introduces automated reasoning methods for propositional and first-order logic. The course develops theoretical foundations of automated reasoning with focus on efficiency and applications.
Teaching and learning methods
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
Learning outcomes are detailed on the COMP60332 course unit syllabus page on the School of Computer Science's website for current students.
- Analytical skills
- Problem solving
- Written communication
- Written exam - 50%
- Written assignment (inc essay) - 50%
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)
COMP60332 reading list can be found on the School of Computer Science website for current students.
Exercise classes; assessment and feedback on written assignments.
- Assessment written exam - 2 hours
- Lectures - 24 hours
- Practical classes & workshops - 16 hours
- Independent study hours - 108 hours