Walther’s estimation calculus was designed to prove the termination of functional programs, and 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 are more common to the problem of induction rule well-foundedness than the problem of termination, and which the calculus cannot handle. We present a sound extension of the calculus 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 argument, and secondly, so that a bound may exist between two arguments of a predicate. Our calculus enables automatic proofs of the well-foundedness of a large class of induction rules not captured by the original calculus.
|Title of host publication||Logic for Programming and Automated Reasoning|
|Subtitle of host publication||6th International Conference, LPAR’99 Tbilisi, Georgia, September 6–10, 1999 Proceedings|
|Editors||Harald Ganzinger, David McAllester, Andrei Voronkov|
|Number of pages||15|
|Publication status||Published - 1999|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer Berlin / Heidelberg|