Next: Digital Electronics
Up: Michaelmas Term 1999: Part
Previous: Unix Tools
Lecturer: Dr L.C. Paulson
(lcp@cl.cam.ac.uk)
No. of lectures: 12
This course is a prerequisite for Specification and
Verification I (Part II).
Aims
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 ordered binary decision diagrams (OBDDs) and
modal logic.
Lectures
- 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.
- Ordered binary decision diagrams.
General concepts. Fast canonical form algorithm. Optimisations.
Applications.
- 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. The Davis-Putnam procedure. The resolution rule.
Examples. Refinements.
- Skolem functions and Herbrand's theorem.
Prenex normal form. Skolemisation. Herbrand models and their
properties.
- Unification.
Composition of substitutions. Most general unifiers. A
unification algorithm. Applications and variations.
- Prolog.
Binary resolution. Factorisation. Example of Prolog
execution. Proof by model elimination.
- 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?
Objectives
At the end of the course students should
- be able to manipulate logical formulas and to notice their own errors
- be able to prove logical theorems, either using a formal calculus or by
applying standard laws of Boolean algebra
- be able to construct a small OBDD
- understand the relationships between the various clause methods
(Davis-Putnam, resolution and Prolog)
- be able to describe the contrasting uses of the two main methods for
propositional logic (OBDDs and Davis-Putnam)
- be able to apply the unification algorithm and to describe its uses
- know how to express and prove statements in modal logic
- understand the relationship between the sequent calculus and tableaux
methods
- be able to describe the distinction between clausal and
non-clausal methods
Recommended books
Chang, C-L. & Lee, R.C-T. (1973). Symbolic Logic and Mechanical
Theorem Proving. Academic Press.
Galton, A. (1990). Logic for Information Technology. Wiley.
Reeves, S. & Clarke, M. (1990). Logic for Computer Science.
Addison-Wesley.
Next: Digital Electronics
Up: Michaelmas Term 1999: Part
Previous: Unix Tools
Christine Northeast
Mon Sep 20 10:28:43 BST 1999