Logic and Proof

Lecturer: Dr L.C. Paulson (lcp@cl.cam.ac.uk)

No. of lectures: 12  

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. Skolemization. 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. Skolemization. The world's smallest theorem prover?

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.