Extensions to the estimation calculus

Abstract

Walther's estimation Cetlculus was designed to prove the termination of functional programs, etnd can also be used to solve the similar problem of proving the well-foundedness of induction rules. However, there are certain features of the goal formulae which axe more common to the problem of induction rule well-foundedness than the problem of termination, eind which the calculus Ccinnot handle. We present a sound extension of the cailculus that is capable of dealing with these features. The extension develops Walther's concept of an argument bounded function in two ways: firstly, so that the function may be bounded below by its cirgument, and secondly, so that a bound may exist between two aiguments of a predicate. Our calculus enables automatic proofs of the well-foundedness of a large class of induction rules not captiued by the original calculus.