Skip to navigation | Skip to main content | Skip to footer
Menu
Menu

COMP60332 Automated Reasoning and Verification syllabus 2017-2018

COMP60332 materials

COMP60332 Automated Reasoning and Verification

Level 6
Credits: 15
Enrolled students: 25

Course leader: Renate Schmidt


Additional staff: view all staff

Assessment methods

  • 50% Written exam
  • 50% Coursework
Timetable
SemesterEventLocationDayTimeGroup
Sem 2 w19,21-22 Lecture 2.15 Fri 09:00 - 17:00 -
Sem 2 w20,23 Lecture 2.15 Fri 09:00 - 16:00 -
Sem 2 w20,23 Lab 2.25B Fri 14:00 - 17:00 -
Themes to which this unit belongs
  • Ontology Engineering and Automated Reasoning
  • Computer Science units for ACSwITM students (semester 2)

Overview

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.

Aims

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.

Syllabus

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)

Teaching methods

Lectures

Lecturers will be interspersed with example classes and labs on teaching days

Examples classes

Example classes will take place on teaching days

Laboratories

Labs will take place on teaching days

Feedback methods

Exercise classes; assessment and feedback on written assignments.

Study hours

Employability skills

  • Analytical skills
  • Problem solving
  • Research
  • Written communication

Learning outcomes

Programme outcomeUnit learning outcomesAssessment
A1 A2 B3Have knowledge and understanding of the syntax and semantics of classical propositional and first-order logic as well as clause logic.
  • Examination
  • Lab assessment
  • Individual coursework
A1 A2 B3Have understanding of the propositional reasoning based on DPLL.
  • Lab assessment
  • Individual coursework
  • Examination
B2 C3Be able to use the SAT solver, MiniSAT, and apply it to solve reasoning problems.
  • Individual coursework
  • Lab assessment
  • Examination
A1 A2 B3Have an understanding of advanced techniques of resolution theorem proving and be able to use them.
  • Individual coursework
  • Examination
  • Lab assessment
B2 C3Be able to use the SPASS resolution prover and apply it to solve reasoning problems.
  • Individual coursework
  • Lab assessment
A1 A2 B3Have an understanding of issues relating to verification and gain experience in using automated reasoning for verification purposes.
  • Examination
  • Lab assessment
  • Individual coursework

Reading list

TitleAuthorISBNPublisherYearCore
Mathematical logic for Computer Science (3rd edition)Ben-Ari, Mordechai9781447141280Springer2012
First-order logic and automated theorem proving (2nd edition)Fitting, Melvin0387945938Springer1995
Essence of logicKelly, John0133963756Pearson Education Limited1997
Logic for Computer ScientistsSchoning, Uwe9780817647629Birkhauser Verlag AG2008

Additional notes

Course unit materials

Links to course unit teaching materials can be found on the School of Computer Science website for current students.