Proposer: Alan Bundy, 50-2716, bundy@ed.ac.uk

Suggested Supervisors: Alan Bundy

Principal goal of the project: To synthesise decision procedures and/or normalisers for mathematical (sub-)theories.

Description:

One approach to solving the combinatorial explosion in automated reasoning is to use decision procedures. A decision procedure is given a formula in a decidable theory and returns its truth value. When the decision procedure is also efficient then this solution avoids the combinatorial explosion. Unfortunately, few interesting theories are decidable. But even undecidable theories often have decidable sub-theories. Then, one or more decision procedures can make a big contribution to proof search by taking care of many minor sub-goals.

Many efficient decision procedures are known and have been efficiently encoded and used in practical theorem provers, eg PVS. However, we frequently encounter new theories in practical applications of automated reasoning. Consider, for instance, verification of software. The programs to be verified define new functions. These definitions constitute a new theory, for which we are unlikely to have predefined decision procedures.

Many decision procedures have a similar structure. For instance, they work by applying a sequence of normalisers to rewrite the input formulae into a tighter and tighter normal form. At some point it becomes trivial to read off the truth value from this formulae, eg because it contains no variables and can be evaluated. Many normalisers also have a family resemblance. For instance, they may start by using definitions to remove certain functions. They may then stratify the formula into layers, so all occurrences of each function are clustered together. Then each layer may be normalised separately. Conjunctive normal form and polynomial normal form are examples of this pattern.

The rewrite rules which implement each stage of these processes have a syntactic form which can be automatically recognised. So the project is to automatically recognise the potential for normalisers/decision procedures from among the definitions, axioms, theorems etc of a theory and then put it together. Essentially, we provide a proof plan for a normaliser/decision procedure and the program will instantiate it with the rewrite rules available. The essential ideas behind this are described in more detail in the paper and note below.

Resources Required: Access to the Clam proof planner.

Degree of Difficulty: This is a challenging project, but it can be made more or less difficult according to the ability of the student. For instance, the provision of proof plans for normalisers/decision procedures depends on the ingenuity of the student in spotting common patterns and representing them. The scope and power of the system will depend on the generality with which this is done. Also there are opportunities for optional extensions, eg conjecturing then proving lemmas which fill gaps in a partial normaliser.

Background Needed: Knowledge of automated theorem proving.

References:

• The Use of Proof Plans for Normalisation, Bundy, A., Essays in Honor of Woody Bledsoe, ed Boyer, R.S., Kluwer, pp149-166,. Also available as DAI Research Paper No. 513.
• Automatic generation of normal forms, Bundy, A., Blue Book Note 1138, 1997.