Current postgraduate taught students
COMP60332: Automated Reasoning and Verification (2012-2013)
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 and verification tools.
The course aims at providing an understanding of propositional logic, first-order logic and clause logic, giving an introduction to theoretical concepts and results that form the basis of current automated reasoning systems based on DPLL and resolution, and discussin verification as an important application domain.
|Programme outcome||Unit learning outcomes||Assessment|
|A1 A2 B3||Have knowledge and understanding of the syntax and semantics of classical propositional and first-order logic as well as clause logic.|
|A1 A2 B3||Have understanding of the propositional reasoning based on DPLL.|
|B2 C3||Be able to use the SAT solver, MiniSAT, and apply it to solve reasoning problems.|
|A1 A2 B3||Have an understanding of advanced techniques of resolution theorem proving and be able to use them.|
|B2 C3||Be able to use the SPASS resolution prover and apply it to solve reasoning problems.|
|A1 A2 B3||Have an understanding of issues relating to verification and gain experience in using automated reasoning for verification purposes.|
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 (4)
- the language of first-order logic
- normal forms, clauses, optimised normal forms
Semantics of first-order logic (3)
- Herbrand models
- concepts and results of soundness and completeness
- orderings, model building
Resolution theorem proving (4)
- unifiers, unification algorithm
- basic first-order resolution, ordering and selection refinements
- redundancy elimination, distributed reasoning as application
- Using SPASS
- hardware verification
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
Title: Logic for Computer Scientists
Author: Schoning, Uwe
Publisher: Birkhauser Verlag AG
Title: Essence of logic
Author: Kelly, John
Publisher: Pearson Education Limited