Current postgraduate taught students
COMP60121: Automated Reasoning (2007-2008)
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.
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).
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 outcomesLearning 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 OutcomesA1, A2, B2, B3, and C3
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: .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: .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: .Normal forms, clauses, resolution.
First-order/predicate logic introduction: .Quantifiers, first order models, validity and satisfiability.
First-order reasoning using unrefined resolution .Normal forms, clauses, Skolemization: elimination of quantifiers, unification, resolution, simplification techniques.
Basics of Advanced Techniques .Well-founded orderings, multi-sets, multi-set orderings, structural transformation, optimisations.
Refutational completeness of propositional resolution .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 .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 .Neuman-Stubblebine key exchange protocol.
Logic Programming: [2, supervised labs].Horn clauses, SLD resolution, Prolog.
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 TextTitle: First-order Logic
Author: Raymond M. Smullyan
Publisher: Dover Publications Inc.
These texts will give a good introduction to logical systems and reasoning methods.
Supplementary TextTitle: Essence of logic
Author: Kelly, John
Publisher: Pearson Education Limited
These texts will give a good introduction to logical systems and reasoning methods and should appeal to students who find Kelly too basic.
Supplementary TextTitle: Logic for Computer Scientists
Author: Schoning, Uwe
Publisher: Birkhauser Verlag AG
These texts will give a good introduction to logical systems and reasoning methods and will appeal to students who find Kelly too basic.