Automated Reasoning and Verification

Unit code: COMP60332
Credit Rating: 15
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

Examples classes

Example classes will take place on teaching days


Labs will take place on teaching days

Learning outcomes

Learning outcomes are detailed on the COMP60332 course unit syllabus page on the School of Computer Science's website for current students.

Employability skills

  • Analytical skills
  • Problem solving
  • Research
  • Written communication

Assessment methods

  • 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)

      * Verification

           + LTL (1)

           + bounded model checking (1)

Recommended reading

COMP60332 reading list can be found on the School of Computer Science website for current students.

Feedback methods

Exercise classes; assessment and feedback on written assignments.

Study hours

  • Assessment written exam - 2 hours
  • Lectures - 24 hours
  • Practical classes & workshops - 16 hours
  • Independent study hours - 108 hours

Teaching staff

Renate Schmidt - Unit coordinator

▲ Up to the top