Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

LPAR

1999

Springer

1999

Springer

Abstract. 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: ﬁrstly, 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.

Related Content

Added |
04 Aug 2010 |

Updated |
04 Aug 2010 |

Type |
Conference |

Year |
1999 |

Where |
LPAR |

Authors |
Jeremy Gow, Alan Bundy, Ian Green |

Comments (0)