TY - GEN
T1 - Extensions to the Estimation Calculus
AU - Gow, Jeremy
AU - Bundy, Alan
AU - Green, Ian
PY - 1999
Y1 - 1999
N2 - 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.
AB - 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.
U2 - 10.1007/3-540-48242-3_16
DO - 10.1007/3-540-48242-3_16
M3 - Conference contribution
SN - 978-3-540-66492-5
T3 - Lecture Notes in Computer Science
SP - 258
EP - 272
BT - Logic for Programming and Automated Reasoning
A2 - Ganzinger, Harald
A2 - McAllester, David
A2 - Voronkov, Andrei
PB - Springer-Verlag GmbH
ER -