Course pages 2014–15
Logic and Proof
No. of lectures: 12
Suggested hours of supervisions: 3
This course is a prerequisite for the Part II courses Artificial Intelligence II, Hoare Logic, Temporal Logic and Natural Language Processing.
This course will teach logic, especially the predicate calculus. It will present the basic principles and definitions, then describe a variety of different formalisms and algorithms that can be used to solve problems in logic. Putting logic into the context of Computer Science, the course will show how the programming language Prolog arises from the automatic proof method known as resolution. It will introduce topics that are important in mechanical verification, such as binary decision diagrams (BDDs), SAT solvers and modal logic.
- Introduction to logic. Schematic statements. Interpretations and validity. Logical consequence. Inference.
- Propositional logic. Basic syntax and semantics. Equivalences. Normal forms. Tautology checking using CNF.
- The sequent calculus. A simple (Hilbert-style) proof system. Natural deduction systems. Sequent calculus rules. Sample proofs.
- First order logic. Basic syntax. Quantifiers. Semantics (truth definition).
- Formal reasoning in FOL. Free versus bound variables. Substitution. Equivalences for quantifiers. Sequent calculus rules. Examples.
- Clausal proof methods. Clause form. A SAT-solving procedure. The resolution rule. Examples. Refinements.
- Skolem functions, Unification and Herbrand’s theorem. Prenex normal form. Skolemisation. Most general unifiers. A unification algorithm. Herbrand models and their properties.
- Resolution theorem-proving and Prolog. Binary resolution. Factorisation. Example of Prolog execution. Proof by model elimination.
- Satisfiability Modulo Theories. Decision problems and procedures. How SMT solvers work.
- Binary decision diagrams. General concepts. Fast canonical form algorithm. Optimisations. Applications.
- Modal logics. Possible worlds semantics. Truth and validity. A Hilbert-style proof system. Sequent calculus rules.
- Tableaux methods. Simplifying the sequent calculus. Examples. Adding unification. Skolemisation. The world’s smallest theorem prover?
At the end of the course students should
- be able to manipulate logical formulas accurately;
- be able to perform proofs using the presented formal calculi;
- be able to construct a small BDD;
- understand the relationships among the various calculi, e.g. SAT solving, resolution and Prolog;
- understand the concept of a decision procedure and the basic principles of “satisfiability modulo theories”.
- be able to apply the unification algorithm and to describe its uses.
* Huth, M. & Ryan, M. (2004). Logic in computer science: modelling and reasoning about systems. Cambridge University Press (2nd ed.).
Ben-Ari, M. (2001). Mathematical logic for computer science. Springer (2nd ed.).