Extensions to the Estimation Calculus

Jeremy Gow, Alan Bundy, Ian Green

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationLogic for Programming and Automated Reasoning
Subtitle of host publication6th International Conference, LPAR’99 Tbilisi, Georgia, September 6–10, 1999 Proceedings
EditorsHarald Ganzinger, David McAllester, Andrei Voronkov
PublisherSpringer-Verlag GmbH
Number of pages15
ISBN (Electronic)978-3-540-48242-0
ISBN (Print)978-3-540-66492-5
Publication statusPublished - 1999

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint Dive into the research topics of 'Extensions to the Estimation Calculus'. Together they form a unique fingerprint.

Cite this