@inproceedings{d229201740784eed8df19575fb62115f,
title = "Extensions to the Estimation Calculus",
abstract = "Walther{\textquoteright}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{\textquoteright}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.",
author = "Jeremy Gow and Alan Bundy and Ian Green",
year = "1999",
doi = "10.1007/3-540-48242-3_16",
language = "English",
isbn = "978-3-540-66492-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag GmbH",
pages = "258--272",
editor = "Harald Ganzinger and David McAllester and Andrei Voronkov",
booktitle = "Logic for Programming and Automated Reasoning",
}