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 prospect.

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.

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
and
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.

Word unification

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 implement it.
Michael Norrish <Michael.Norrish@cl.cam.ac.uk>
Last modified: Tue Oct 1 13:52:18 BST 2002