Supervisor: Alan Bundy, 502716, bundy@dai

Subject Areas: Automated Reasoning/Theorem Proving,

Project Suitable for the Following Degrees: MSC in AI, AI-CS4, AI-Math4, AI-Psych4,

Principal goal of the project: Build a system which summarises mathematical proofs in English. The system will use proof planning to construct the summaries.

Description:

When mathematicians explain proofs to each other they can draw on a shared language of common proof patterns. This enables them to summarise the proof using only the overall shape and the departures from the standard patterns. Most automated reasoning systems do not support such ways of explaining proofs. Normally, it is only possible to explain the proof in terms of the lowest level logical steps. This leads to long, detailed and hard to understand explanations.

The proof planning technique should be adaptable to provide the kind of proof summaries described above. A proof plan is the computational representation of a common pattern of proof. Proof plans have been used by our Clam planner to guide the search for a proof, mainly in the domain of mathematical induction. Critics analyse any failure to apply a proof plan to a conjecture and suggest patches.

It seems possible to exploit this by explaining a proof in terms of (a) the underlying proof plan and (b) any departures from it. Typical proof summaries might be:

• "The proof is by one-step structural induction on x. Both the base case and the step case require a nested one-step structural induction on y."
• "The proof is by two-step structural induction on x. However, to enable the step case to be completed, the conjecture must first be generalised by introducing a second universal variable y. y is appended to x on the LHS and x is appended to y on the RHS."
• "The proof requires an unusual induction in which x takes the values 0, 1 and any prime number in the base cases and is a product of natural numbers in the step case."

The grammar required is quite limited and so the text may be generated from small pieces of canned text and a specialised grammar. The construction process will be informed by the final proof plan, the use of critics during the proof and the history of the proof construction process. An optional extension would be the facility to vary the amount of detail in the proof. This corresponds, for instance, to unpacking the proof plan to reveal some of the lower level details.

Resources Required: Access to the CLAM proof planner.

Degree of Difficulty: The project is moderately difficult because it requires a combination of knowledge about both automated reasoning, especially proof planning, and natural language generation. It is fairly open ended so could be extended for a strong student or restricted for a weak student.

Background Needed: Attendance at the automated reasoning and techniques in natural language processing modules.

References:

• Bundy, A. A Science of Reasoning, in `Computational Logic: Essays in Honor of Alan Robinson', eds Lassez J-L & Plotkin, G., MIT Press, pp 178-198, 1991.
• Ireland, A., and Bundy, A. Productive Use of Failure in Inductive Proof, in the special issue of JAR on Automated Mathematical Induction, Vol. 16, No. 1-2, pp 79-111, ed Zhang, H., March 1996.