Abstract
Proving the termination of algorithms is one of the challenges in program verification.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Avenhaus, J. (1995). Reduktionssysteme. Springer.
Baader, E and Nipkow, T. (1998). Term Rewriting and All That. Cambridge University Press.
Boyer, R. and Moore, J. S. (1979). A Computational Logic. Academic Press, Boston.
Brauburger, J. (1997). Automatic Termination Analysis for Partial Functions using Polynomial Orderings. In Proceedings of the 4th International Static Analysis Symposium (SAS ’87), Paris, France,LNCS 1302, pages 330–344. Springer.
Brauburger, J. (1999). Automatic Termination Analysis for Functional and Imperative Programs. Doctoral Dissertation TU Darmstadt, Infix, St. Augustin, Germany.
Dershowitz, N. and Manna, Z. (1979). Proving termination with multiset orderings. CACM, 22 (8): 465–476.
Feferman, S. (1991). Proofs of termination and the “91” function. In Lifschitz, V., editor, Artificial Intelligence and Mathematical Theory of Computation, pages 47–63. Academic Press, Boston.
Gallier, J. H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper and Row, New York.
Gardner, M. (1983). Wheels, Lifes and other Mathematical Amusements. W. H. Freeman and Company, New York.
Giesl, J. (1995). Automatisierung von Terminierungsbeweisenfir rekursiv definierteAlgorithmen, volume 96 of DISKI. Doctoral Dissertation TU Darmstadt, Infix, St. Augustin, Germany.
Giesl, J. (1997). Termination of Nested and Mutually Recursive Algorithms. Journal of Automated Reasoning, 19: 1–29.
Giesl, J., Walther, C., and Brauburger, J. (1998). Termination Analysis for Functional Programs. In Bibel, W. and Schmitt, R, editors, Automated Deduction —A Basis for Applications,volume 3, pages 135–164. Kluwer Academic Publishers.
Knuth, D. (1991). Textbook examples of recursion. In Lifschitz, V., editor, Artificial Intelligence and Mathematical Theory of Computation, pages 207–229. Academic Press, Boston.
Manna, Z. (1974). Mathematical Theory of Computation. McGraw-Hill.
McAllester and Arkoudas (1996). Walther Recursion. In Proceedings of the 13th International Conference on Automated Deduction (CADE-13), New Brunswick, USA, LNAI 1104, pages 643–657.
Springer. Moore, J. S. (1979). A Mechanical Proof of the Termination of Takeuchi’s Function. Information Processing Letters, pages 176–181.
Newman, M. A. H. (1942). On theories with a combinatorical definition of ‘equivalence’. Annals of Mathematics, 43 (2): 223–243.
Panitz, S. (1997). Generierung statischer Programminformation zur Kompilierung verzögert ausgewerteter funktionaler Programmiersprachen. Doctoral Dissertation, Johann Wolfgang Goethe-Universität, Frankfurt am Main, Germany.
Panitz, S. and Schmidt-Schauß, M. (1997). TEA: Automatically Proving Termination of Programs in a Non-Strict Higher-Order Functional Language. In Proceedings of the 4th International Static Analysis Symposium (SAS ’87), Paris, France,LNCS 1302, pages 345–360. Springer.
Sengler, C. (1996). Termination of Algorithms over Non-freely Generated Data Types. In Proceedings of the 13th International Conference on Automated Deduction (CADE-13), New Brunswick, USA,LNAI 1104, pages 121–136. Springer.
Sengler, C. (1997). Induction on Non-Freely Generated Data Types, volume 160 of DISKI. Doctoral Dissertation, Infix, St. Augustin, Germany.
Walther, C. (1994a). Mathematical Induction. In Gabbay, D., Hogger, C., and Robinson, J., editors, Handbook of Logic in Artificial Intelligence and Logic Programming,volume 2. Oxford University Press.
Walther, C. (1994b). On proving the Termination of Algorithms by Machine. Artificial Intelligence, 71 (1): 101–157.
Walther, C. (1998). Recursion, Induction, Verfication. Course Notes, TU Darmstadt.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Walther, C. (2000). Criteria for Termination. In: Hölldobler, S. (eds) Intellectics and Computational Logic. Applied Logic Series, vol 19. Springer, Dordrecht. https://doi.org/10.1007/978-94-015-9383-0_22
Download citation
DOI: https://doi.org/10.1007/978-94-015-9383-0_22
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5438-8
Online ISBN: 978-94-015-9383-0
eBook Packages: Springer Book Archive