Abstract
Termination is well-known to be one of the important aspects of program correctness. Logic programming provides a framework with a strong theoretical basis for tackling this problem. However, due to the declarative formulation of programs, the danger of non-termination may increase. As a result, termination analysis received considerable attention in logic programming. Recently, the study of termination of numerical programs led to the emerging of the adorning technique [7]. This technique implements the well-known “divide et impera” strategy by distinguishing between different subsets of values for variables, and deriving termination proofs based on these subsets. In this paper we generalise this technique and discuss its applicability to the domain of terms (the Herbrand domain).
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
Similar content being viewed by others
References
Bruynooghe, M., Codish, M., Genaim, S., Vanhoof, W.: Reuse of results in termination analysis of typed logic programs. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 477–492. Springer, Heidelberg (2002)
Bruynooghe, M., De Schreye, D., Martens, B.: A general criterion for avoiding infinite unfolding during partial deduction. New Generation Computing 11(1), 47–79 (1992)
Dershowitz, N., Hoot, C.: Topics in termination. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690, pp. 198–212. Springer, Heidelberg (1993)
Leuschel, M.: The ecce partial deduction system. In: G. Puebla, editor, Proceedings of the ILPS 1997 Workshop on Tools and Environments for (Constraint) Logic Programming, Universidad Politécnica de Madrid, Tech. Rep. CLIP7/97.1, Port Jefferson, USA (October 1997)
Leuschel, M., Martens, B., Sagonas, K.: Preserving termination of tabled logic programs while unfolding. In: Fuchs, N.E. (ed.) LOPSTR 1997. LNCS, vol. 1463, pp. 189–205. Springer, Heidelberg (1998)
Sahlin, D.: Mixtus: An automatic partial evaluator for full Prolog. New Generation Computing 12(1), 7–51 (1993)
Serebrenik, A., De Schreye, D.: Inference of termination conditions for numerical loops in Prolog. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 654–668. Springer, Heidelberg (2001)
Winsborough, W.: Multiple specialization using minimal-function graph semantics. Journal of Logic Programming 13(2/3), 259–290 (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Serebrenik, A., De Schreye, D. (2004). Proving Termination with Adornments. In: Bruynooghe, M. (eds) Logic Based Program Synthesis and Transformation. LOPSTR 2003. Lecture Notes in Computer Science, vol 3018. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25938-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-25938-1_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22174-6
Online ISBN: 978-3-540-25938-1
eBook Packages: Springer Book Archive