Project suggestions from Michael Norrish
I am leaving Britain in December 2002. If you are interested in doing
these projects, you will need to find a supervisor who will be here
for the whole year, though I will happily see you through the
Michaelmas term. Joe Hurd has said that
he will be such a supervisor for these projects, so he's a likely
Simple declarative theorem-proving
When specifying systems formally, a significant error-finding benefit
can accrue simply from writing everything down in an expressive logic,
and getting it all to type-check. Actual formal verification of
important properties can almost be relegated to the role of ``nice work
if you can get it''.
The HOL system
currently doesn't allow for this model of work very well. Part of the
reason for this is that script files for HOL inter-mingle ML (which is
the theorem-prover's implementation language) and embedded bits of
logic. We would like to check the logic without having to be able to
parse (and execute) ML as well.
Therefore, the aim of this project is to design a simple file format
in which users could write ``ML-less HOL'', and to then implement at
least two tools for manipulating this format. The first tool would be
the type-checker. It would make sure that the definitions and other
logical material in the file actually made sense at the level of
types. The second tool would do all this and also produce a genuine
HOL theory, using the various facilities already present in HOL.
If this all went well, there would be ample opportunity to extend this
project so that it also included a declarative proof (as opposed to
just definition) element.
Implementing proof kernels
At the core of LCF systems like HOL,
there is a small ``kernel'' that implements the primitive rules of
inference of the logic. There are a number of interesting issues
relating to the design of these kernels. For example
The project would be to explore this design space by
implementing first a very simple-minded kernel, and then testing a
suite of possible optimisations on top of this initial design. This
problem comes with its own test suite, and admits a very explicit and
clear specification, because of its position as part of HOL.
- How to represent free and bound variables?
- Optimising common calculations (such as calculating the set of
Comparison of (arithmetic decision/first order logic) procedures
There are a variety of well-known decision procedures for deciding
logical problems. For first order logic, the PartIB course
Logic and proof describes tableau and resolution methods.
Another method is model elimination. In arithmetic, there is also a
variety of methods, including Cooper's algorithm, the Omega Test,
SUP-INF, loop residue and the like.
FOL procedures solve problems like
(forall x y z. R(x,y) and R(y,z) implies
R(x,z)) and R(a,b) and R(b,c) and
R(c,d) implies R(a,d).
Arithmetic procedures solve problems like
2x > x implies x > 0
there exist x and y such that
2x + y > 7 and x + 2y < 11
A project in this area would involve implementing appropriate
procedures and then comparing their performance. I can provide
documentation and explanations for the arithmetic procedures.
Given an equation involving variables and characters, where variables
can range over strings of any length, and the only operation is string
concatenation, is there any satisfying assignment of strings to
variables to make the two sides of the equation equal?
E.g., given the equation
aXb = aaY
where X and Y are variables, one satisfying
assignment is X = a and Y = b. But X = aa
and Y = ab also works. In fact, there are an infinite number
of unifiers, all of the form X = aZ, Y = Zb, where Z
can be anything at all (including the empty string, as in the first
solution above). There is a horrendously complicated algorithm for
solving these problems. Your task would be to understand it, and then
Michael Norrish <Michael.Norrish@cl.cam.ac.uk>
Last modified: Tue Oct 1 13:52:18 BST 2002