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

Current postgraduate taught students

COMP61111: Logical Reasoning and Applications (2011-2012)

This is an archived syllabus from 2011-2012

Logical Reasoning and Applications
Level: 6
Credit rating: 15
Pre-requisites: none
Co-requisites: none
Duration: 6 weeks long; teaching will take place on 1 day per week for 5 weeks
Lectures: Lecturers will be interspersed with example classes and labs on teaching days
Examples classes: Example classes will take place on teaching days
Labs: Labs will take place on teaching days
Lecturers: Konstantin Korovin, Renate Schmidt
Course lecturers: Konstantin Korovin

Renate Schmidt

Additional staff: view all staff
Sem 1 P1 Lecture 2.15 Tue 09:00 - 17:00 -
Assessment Breakdown
Exam: 50%
Coursework: 50%
Lab: 0%

Themes to which this unit belongs
  • Logics and Ontologies


Logic and 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 logic and 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.


The course aims at providing an understanding of propositional, first-order and clause logics, giving an introduction to
theoretical concepts and results that form the basis of current automated reasoning systems based on DPLL and resolution, and discussing important applications of automated reasoning.

Programme outcomeUnit learning outcomesAssessment
G1Have knowledge and understanding of the syntax and semantics of classical propositional and first-order logic as well as clause logic.
  • Lab assessment
  • Individual coursework
  • Examination
G1Have knowledge of basic concepts of logic (soundness, completeness, proofs, decidability, undecidability).
  • Examination
  • Individual coursework
G1Have knowledge of normal forms and transformation algorithms (clausal normal from, optimised transformation, Skolemisation).
  • Examination
  • Lab assessment
  • Individual coursework
G1 G2Have understanding of the propositional reasoning using DPLL (unit propagation, backtracking, backjumping, lemma learning.
  • Examination
  • Individual coursework
  • Lab assessment
G3Be able to use the SAT solver, MiniSAT, and apply it to solve reasoning problems.
  • Individual coursework
  • Lab assessment
G1 G2Have an understanding of advanced techniques of resolution theorem proving and be able to use them (local restrictions of inference, orderings, selection, redundancy elimination.
  • Lab assessment
  • Examination
  • Individual coursework
G1Have an understanding of the main theoretical concepts of soundness and completeness of resolution (Herbrand models, model construction).
  • Examination
  • Individual coursework
G2Be able to use ordered resolution with selection for constructing refutation proofs.
  • Individual coursework
  • Lab assessment
  • Examination
G2Have an understanding of application areas of logical reasoning discussed in class.
  • Lab assessment
  • Individual coursework
  • Examination
G3Be able to use the SPASS resolution prover and apply it to solve reasoning problems.
  • Lab assessment
  • Individual coursework


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 to logics and applications (1)

Orderings, multi-sets, induction (1)

Propositional logic (2)
- syntax, semantics, truth tables
- concepts and results of soundness and completeness, decidability

Transformations to normal forms (1)
- CNF, NNF, clauses

Propositional reasoning methods (4)
- Propositional resolution, resolution rule, factoring rule, proofs
- DPLL & SAT-solving, unit propagation, backtracking, backjumping, lemma learning

First-order logic (3)
- syntax, semantics
- concepts and results of soundness and completeness,
- undecidability and semi-decidability

Resolution theorem proving (6)
- transformation to clausal form: prenex normal form, CNF, Skolemisation, optimisations
- substitutions, unifiers, unification algorithm
- Herbrand models,
- model construction, soundness & refutational completeness
- first-order resolution, ordering and selection refinements

Concrete applications (3)
- logic applications
- security protocol verification
- planning & scheduling

Reading List

There is no single book covering all material, but the following give a good introduction to logical systems and reasoning methods. There are other text books available on the topics covered.

Fitting, Schoning and Voronkov will give a good introduction to logical systems and reasoning methods and should appeal to students who find Kelly too basic.

Notes made available during the course unit to cover the SPASS theorem prover and all of the various topics presented in the course.

Further details will be presented in the course.

Title: First-order logic and automated theorem proving (2nd edition)
Author: Fitting, Melvin
ISBN: 0387945938
Publisher: Springer
Edition: 2nd
Year: 1995

Title: Logic for Computer Scientists
Author: Schoning, Uwe
ISBN: 9780817647629
Publisher: Birkhauser Verlag AG
Year: 2008

Title: Essence of logic
Author: Kelly, John
ISBN: 0133963756
Publisher: Pearson Education Limited
Year: 1997