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

Current postgraduate taught students

COMP60121: Automated Reasoning (2007-2008)

This is an archived syllabus from 2007-2008

Automated Reasoning
Level: 6
Credit rating: 15
Pre-requisites: Propositional Logic (knowledge of predicate logic and some logic programming experience would be some advantage, but not essential).
Co-requisites: No Co-requisites
Lectures: 1 day per week (5 weeks)
Lecturers: Renate Schmidt, Alan Williams
Course lecturers: Renate Schmidt

Alan Williams

Additional staff: view all staff
Timetable
SemesterEventLocationDayTimeGroup
Sem 1 w1-5 Lecture 2.15 Mon 09:00 - 17:00 -
Assessment Breakdown
Exam: 40%
Coursework: 60%
Lab: 0%

Introduction

Logic, the study of reasoning, plays an important role in theoretical computer science and many of the practical areas of computer science such as systems development, computer hardware, data bases, cognitive science, AI and logic programming. For example, in web technologies and agent technologies logical and automated reasoning methods are used for the intelligent processing of large ontologies, decision making based on knowledge bases of structured data, and formal specification and verification of multi-agent systems. An important part of the systems development process concerns reasoning about the behaviour of systems in order to verify the correctness of the behaviour. While these are specific examples of applications of automated reasoning, the focus in this course is on general aspects of logic and automated reasoning which are relevant to many such applications, as well as logic programming. The main motivation of the course is the study and development of general, efficient automated reasoning techniques.

Aims

Broadly, this course unit aims to provide an introduction to classical logic, automated theorem proving and logic programming. It aims to:
provide students with an understanding of classical logic (propositional, first-order and clause logic),
give an introduction to theoretical concepts and results that form the basis of current state-of-the-art theorem provers (and other theorem proving tools)
discuss and study resolution theorem proving methods.
provide an introduction to logic programming.

It is assumed that students will be familiar with classical propositional logic (Boolean logic). Further knowledge of the subject is not assumed, although it would be an advantage for students to have some familiarity with predicate logic (first-order logic) and experience of logic programming, in particular Prolog (it is worth noting that students without such knowledge have not been disadvantaged in the past).

Learning Outcomes

A student completing this course unit should:
have knowledge and understanding of the syntax and semantics of classical propositional and predicate/first-order logic as well as clause logic (A).
have an understanding of the main ingredients of resolution calculi and be able to use them (transformation into clause form, inference rules, unification, orderings, selection) (A and B).
have an understanding of the main theoretical concepts for establishing refutational completeness of resolution calculi (candidate models, reduction of counter-examples) (A).
have an understanding of and be able to use the general concept of redundancy and be able to use it to justify different ways of simplifying and reducing the search space of theorem proving processes (tautology deletion, subsumption deletion, purity deletion, reduction) (A and B).
be able to use the resolution for constructing proofs/refutations (B).
be able to use the SPASS theorem prover and apply it to solve reasoning problems (C)
have an understanding of the relationship between resolution and logic programming (A).
have the competence to write Prolog programs (B and C).

Assessment of Learning outcomes

Learning outcomes (1)-(6), (8), (9) will be assessed by exam. All learning outcomes will be assessed via paper and laboratory exercises set during the Teaching Period of the course unit.

Contribution to Programme Learning Outcomes

A1, A2, B2, B3, and C3

Syllabus

The following lists the topics to be covered in the course. The Teaching Days will contain a mixture of lectures, examples classes and supervised laboratories. The numbers of sessions for each topic are given in brackets. If the topic is to be covered largely in the student?s Own work time or in the labs, then this is also indicated.
The course unit is practicably-based, and so students will spend approximately one third of the total Teaching and Own Work Time undertaking laboratory exercises. This will include producing implementations of the various reasoning methods covered as well as using existing automated reasoning tools.

Introduction and motivation: [1].

Including example problems, problem representation via logic, computer assisted reasoning in mathematics.

Basics of sets and relations [Own].

What is a set, a relation, a function, set operations (intersection, union, etc), properties of binary relations (reflexivity, symmetry, transitivity, etc).

Revision of Propositional logic: [1].

Theory, language, models, validity and satisfiability, proof/inference rules, soundness and completeness, reasoning methods: truth tables, proof by contradiction, semantic tableaux.

Propositional logic reasoning using resolution: [1].

Normal forms, clauses, resolution.

First-order/predicate logic introduction: [1].

Quantifiers, first order models, validity and satisfiability.

First-order reasoning using unrefined resolution [2].

Normal forms, clauses, Skolemization: elimination of quantifiers, unification, resolution, simplification techniques.

Basics of Advanced Techniques [2].

Well-founded orderings, multi-sets, multi-set orderings, structural transformation, optimisations.

Refutational completeness of propositional resolution [3].

Herbrand interpretations, soundness, clause orderings, construction of candidate models, reduction of counter-examples, model existence theorem, refutational completeness, compactness of propositional logic.

Saturation-based framework of resolution calculi [3].

Ordered resolution with selection, lifting, refutational completeness, Craig interpolation, redundancy concept, saturation up to redundancy, practical model of a resolution prover, fairness, refinements of resolution, hyperresolution.

Formalisation of a concrete application [1].

Neuman-Stubblebine key exchange protocol.

Logic Programming: [2, supervised labs].

Horn clauses, SLD resolution, Prolog.

Reading List

There is no single book covering all material, but the following give a good introduction to logical systems and reasoning methods:

A good introduction to logic programming and Prolog is available at: http://staff.science.uva.nl/~ulle/teaching/prolog/prlog.pdf

There are other text books available on the topics covered. Further details will be presented in the taught week.

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

Supplementary Text
Title: First-order Logic
Author: Raymond M. Smullyan
ISBN: 0486683702
Publisher: Dover Publications Inc.
Edition:
Year: 1995
These texts will give a good introduction to logical systems and reasoning methods.


Supplementary Text
Title: Essence of logic
Author: Kelly, John
ISBN: 0133963756
Publisher: Pearson Education Limited
Edition:
Year: 1997
These texts will give a good introduction to logical systems and reasoning methods and should appeal to students who find Kelly too basic.


Supplementary Text
Title: Logic for Computer Scientists
Author: Schoning, Uwe
ISBN: 9780817647629
Publisher: Birkhauser Verlag AG
Edition:
Year: 2008
These texts will give a good introduction to logical systems and reasoning methods and will appeal to students who find Kelly too basic.