Surmising is sometimes better than proving

The paper defines and tackles the problem of surmising recursive function properties given a finite computation of the function. The problem ls motivated in the framework of software development and correctness proof by level of abstractions, where properties of abstraction modules must be used as lemmas in higher level abstraction proofs. A surmising algorithm is given which is used on generalization, instantiation by symbolic execution, and symbolic execution trace analysis. Examples are given which illustrate the capabilities (and limitations) of the algorithm. The second part of the paper gives a formal basis for a performance evaluation of the algorithm. A class of primitive recursive function 15 characterized in terms of function definition schemata, and a proof is given that in such a case the properties surmised by the algorithm actually hold. Hence, the surmising algorithm can be used as a peculiar theorem prover for the given restricted primitive recursive function class. Finally,the implementation issues are briefly discussed.