Poof Analysis: A technique for Concept Formation

We report the discovery of an unexpected connection between the invention of the concept of uniform convergence and the occurs check in the unification algorithm. This discovery suggests the invention of further interesting concepts in analysis and a technique for automated concept formation. Part of this technique has been implemented.
The discovery arose as part of an attempt to understand the role of proof analysis in mathematical reasoning, so as to incorporate it into a computer program. Silver (1986)and Mitchell (1983) have investigated the automatic analysis of model proofs in order to extract and learn knowledge about controlling search,including the knowledge of new concepts. We focus on the analysis and correction of faulty proofs or 'poofs'. Especially where that correction involves the invention of new mathematical concepts.
A classic example of where the analysis of a poof leads to a new concept is the invention, by Weierstrass, Seidel, Cauchy and others, of uniform convergence as a result of an analysis of Cauchy's poof that the limit of a convergentseriesof continuous functions is itself continuous. The correction consists of substituting in the theorem the new concept of 'uniformly convergent' for 'convergent'. We will investigate this example. The bug in Cauchy's poof is a violation of the occurs check. This observation suggests a technique for automatically correcting the proof and this leads to the concept of uniform convergence.The correction technique involves search. Other branches in the searchspacelead to alternative corrections and alternative concepts,one of which seemedinteresting to me and turns out to have been discovered by the mathematician, Ascoli.