Proof Checking Using Experience
Edmund Furse
Checking Mathematics proofs is a complex task which needs experience. Yet most AI approaches to proof checking tend to use general methods rather than knowledge rich approaches. The program MU, Mathematics Understander, reads mathematics texts expressed in the Formal Expression Language (FEL), and provides explanations of the proof steps. MU has successfully checked proofs in group theory and classical analysis, and appears to be the state of the art in the complexity of the mathematical material it can check. To achieve this performance MU needs to use a large quantity of mathematical knowledge, all of which is learned from the reading of texts, it being impractical to hand program such knowledge. Of particular importance is that in checking proofs in order to avoid a combinatorial explosion it is necessary to be able to limit the search. This is achieved by use of the Contextual Memory System (CMS) which ensures that important results are easy to access, and unimportant results more difficult. It is further argued that for a machine to be able to check complex proofs it is necessary that its knowledge is organised in a form so that the relative importance of results is used for retrieval purposes, and that this is only gained through experience.

Furse E., (1993), Proof Checking using Experience, Technical Report no. CS-93-5, Department of Computer Studies, University of Glamorgan.

List of Papers