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: 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. Brauburger and J. Giesl. Termination analysis by inductive evaluation. In C. Kirchner and H. Kirchner, editors, 15th International Conference on Automated Deduction, pages 254–269. LNAI 1421, Springer-Verlag, 1998.
The DReaM Group. The Clam proof planner, user manual and programmer manual (version 2.8.1), April 1999. Available from ftp://dream.dai.ed.ac.uk/pub/oyster-clam/manual.ps.gz.
J. Giesl. Automated termination proofs with measure functions. In I. Wachsmuth, C. Rollinger, and W. Brauer, editors, 19th Annual German Conference on Artificial Intelligence, pages 149–160. LNAI 981, Springer-Verlag, 1995.
J. Giesl. Termination analysis for functional programs using term orderings. In 2nd International Static Analysis Symposium. LNCS 983, Springer-Verlag, 1995.
J. Giesl. Termination of nested and mutually recursive algorithms. Journal of Automated Reasoning, 19:1–29, 1997.
J. Giesl, C. Walther, and J. Brauburger. Termination analysis for functional programs. In W. Bibel and P.H. Schmitt, editors, Automated Deduction — A Basis for Applications, Vol III: Applications, volume 10 of Applied Logic Series, chapter 6, pages 135–164. Kluwer Academic, 1998.
David McAllester and Kostas Arkoudas. Walther recursion. In M.A. McRobbie and J.K. Slaney, editors, 13th International Conference on Automated Deduction, pages 643–657. LNAI 1104, Springer Verlag, July 1996.
L.C. Paulson. ML for the Working Programmer. Cambridge University Press, 1991.
C. Sengler. Termination of algorithms over non-freely generated datatypes. In M.A. McRobbie and J.K. Slaney, editors, 13th International Conference on Automated Deduction, pages 121–135. LNAI 1104, Springer Verlag, July 1996.
C. Walther. On proving termination of algorithms by machine. Artificial Intelligence, 71(1):101–157, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gow, J., Bundy, A., Green, I. (1999). Extensions to the Estimation Calculus. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds) Logic for Programming and Automated Reasoning. LPAR 1999. Lecture Notes in Computer Science(), vol 1705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48242-3_16
Download citation
DOI: https://doi.org/10.1007/3-540-48242-3_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66492-5
Online ISBN: 978-3-540-48242-0
eBook Packages: Springer Book Archive