OXFORD UNIVERSITY COMPUTING LABORATORY
MSc in Computation courses
Theorem Proving and Algebra
Optional course, 16 lectures in Michaelmas Term
Professor J A Goguen and Dr G Malcolm
Aims
This course of lectures treats algebraic proof techniques and their
application to various problems in Computer Science. Exercises use the OBJ3 system for mechanical proofs in areas ranging
from group theory to VLSI.
Synopsis
The following is an outline. Signature, algebra, equation and theory;
homomorphism, initial (or word, or term) algebra, substitution;
equational deduction, variety and completeness; term rewriting,
interpretation and equivalence of theories, the theorem of constants;
quotient algebras and rewriting modulo equations; induction;
conditional equations; second order universal quantifiers.
There is also an introduction to the OBJ system, and applications to
group theory, abstract data types (including various number systems,
lists and stacks), propositional calculus and digital hardware. There
is a draft textbook, currently about two-thirds finished.
Reading
- Joseph Goguen, Theorem Proving and Algebra, draft textbook - in
preparation
- Joseph Goguen, Proving and Rewriting
- Joseph Goguen, OBJ as a Theorem Prover
- Joseph Goguen, Jose Meseguer & Timothy Winkler, Introducining
OBJ3
- Bergestra, Jan, J Heering & Paul Klint, Algebraic
Specification, ACM Press 1989
- Bledsoe, W W & Donald Loveland (eds), Automatied Theorem
Proving: After 25 Years, (A.M.S. 1984) Volume 29 of Contemporary
Mathematics Series
- Boyer, Robert S & J Strother Moore, A Computational Logic,
ACM 1979
- Chang, Chin-Liang & Richard Char-Tung Lee, Symbolic Logic and
Mechanical Theorem Proving, Academic Press, 1973
- Cohn, Paul M, Universal Algebra, Reidel 1981
- Dershowitz, Nachum & Jean-Pierre Jouannaud, Rewriting Systems
- Ehrig, Hartmut & Bernard Mahr, Fundamentals of Algebraic
Specification, Springer-Verlag 1985
- Klop, Jan Willem, Term Rewriting Systems: A Tutorial
- Andrew Stevens, Joseph Goguen and Keith Hobley, Mechanised Theorem
Proving with 2OBJ: A Tutorial Introduction
Practicals
www@comlab.ox.ac.uk