No CrossRef data available.
Article contents
Automated termination analysis for logic programs with cut*
Published online by Cambridge University Press: 09 July 2010
Abstract
Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.
Termination is an important and well-studied property for logic programs. However, almost all approaches for automated termination analysis focus on definite logic programs, whereas real-world Prolog programs typically use the cut operator. We introduce a novel pre-processing method which automatically transforms Prolog programs into logic programs without cuts, where termination of the cut-free program implies termination of the original program. Hence after this pre-processing, any technique for proving termination of definite logic programs can be applied. We implemented this pre-processing in our termination prover AProVE and evaluated it successfully with extensive experiments.
Information
- Type
- Regular Papers
- Information
- Theory and Practice of Logic Programming , Volume 10 , Special Issue 4-6: 26th International Conference on Logic Programming , July 2010 , pp. 365 - 381
- Copyright
- Copyright © Cambridge University Press 2010
References
Andrews, J. H. 2003. The witness properties and the semantics of the Prolog cut. Theory and Practice of Logic Programming 3, 1, 1–59.CrossRefGoogle Scholar
Billaud, M. 1990. Simple operational and denotational semantics for Prolog with cut. Theoretical Computer Science 71, 2, 193–208.CrossRefGoogle Scholar
Bruynooghe, M., Codish, M., Gallagher, J. P., Genaim, S., and Vanhoof, W. 2007. Termination analysis of logic programs through combination of type-based norms. ACM Transactions on Programming Languages and Systems 29, 2.CrossRefGoogle Scholar
Codish, M., Lagoon, V., and Stuckey, P. J. 2005. Testing for termination with monotonicity constraints. In Logic Programming, 21st International Conference, ICLP, M. Gabbrielli and G. Gupta, Eds. '05. Lecture Notes in Computer Science, vol. 3668. Springer, Berlin, 326–340.Google Scholar
Cousot, P. and Cousot, R. 1992. Abstract interpretation and application to logic programs. Journal of Logic Programming 13, 2–3, 103–179.CrossRefGoogle Scholar
De Schreye, D. and Decorte, S. 1994. Termination of logic programs: The never-ending story. Journal of Logic Programming 19–20, 199–260.CrossRefGoogle Scholar
de Vink, E. P. 1989. Comparative semantics for Prolog with cut. Science of Computer Programming 13, 1, 237–264.CrossRefGoogle Scholar
Deransart, P., Ed-Dbali, A., and Cervoni, L. 1996. Prolog: The Standard. Springer, New York.CrossRefGoogle Scholar
Filé, G. and Rossi, S. 1993. Static analysis of Prolog with cut. In LPAR '93. LNAI, vol. 698. Springer, Berlin, 134–145.Google Scholar
Giesl, J., Schneider-Kamp, P., and Thiemann, R. 2006. AProVE 1.2: Automatic termination proofs in the dependency pair framework. In Proc. IJCAR '06. LNAI, vol. 4130. Springer, Berlin, 281–286.Google Scholar
Giesl, J., Swiderski, S., Schneider-Kamp, P., and Thiemann, R. 2006. Automated termination analysis for Haskell: From term rewriting to programming languages. In RTA '06. LNCS, vol. 4098. Springer, Berlin, 297–312.Google Scholar
Howe, J. M. and King, A. 2003. Efficient groundness analysis in Prolog. Theory and Practice of Logic Programming 3, 1, 95–124.Google Scholar
Kulas, M. and Beierle, C. 2000. Defining standard Prolog in rewriting logic. In WRLA '00. Electronic Notes in Theoretical Computer Science, vol. 36. Elsevier, the Netherlands, 39–59.Google Scholar
Le Charlier, B., Rossi, S., and Van Hentenryck, P. 1994. An abstract interpretation framework which accurately handles Prolog search-rule and the cut. In ILPS '94. MIT Press, 157–171.Google Scholar
Marchiori, M. 1996. Proving existential termination of normal logic programs. In AMAST '96. Lecture Notes in Computer Science, vol. 1101. Springer, Berlin, 375–390.Google Scholar
Mesnard, F. and Serebrenik, A. 2007. Recurrence with affine level mappings is P-time decidable for CLP(R). Theory and Practice of Logic Programming 8, 1, 111–119.CrossRefGoogle Scholar
Mogensen, T. Æ. 1996. A semantics-based determinacy analysis for Prolog with cut. In Ershov Memorial Conference. Lecture Notes in Computer Science, vol. 1181. Springer, Berlin, 374–385.Google Scholar
Nguyen, M. T., De Schreye, D., Giesl, J., and Schneider-Kamp, P. 2010. Polytool: Polynomial interpretations as a basis for termination analysis of logic programs. Theory and Practice of Logic Programming (to appear).Google Scholar
Schneider-Kamp, P., Giesl, J., Serebrenik, A., and Thiemann, R. 2009. Automated termination proofs for logic programs by term rewriting. ACM Transactions on Computational Logic 11, 1.CrossRefGoogle Scholar
Schneider-Kamp, P., Giesl, J., Serebrenik, A., Ströder, T., and Thiemann, R. 2010. Automated termination analysis for logic programs with cut. Tech. Rep. AIB-2010-10, RWTH Aachen. http://aib.informatik.rwth-aachen.de.Google Scholar
Serebrenik, A. and De Schreye, D. 2005. On termination of meta-programs. Theory and Practice of Logic Programming 5, 3, 355–390.CrossRefGoogle Scholar
Sørensen, M. H. and Glück, R. 1995. An algorithm of generalization in positive supercompilation. In ILPS '95. MIT Press, 465–479.Google Scholar
Spoto, F. 2000. Operational and goal-independent denotational semantics for Prolog with cut. Journal of Logic Programming 42, 1, 1–46.Google Scholar
Spoto, F. and Levi, G. 1998. Abstract interpretation of Prolog programs. In AMAST '98. Lecture Notes in Computer Science, vol. 1548. Springer, Berlin, 455–470.Google Scholar
Ströder, T. 2010. Towards termination analysis of real Prolog programs. Diploma Thesis, RWTH Aachen. http://aprove.informatik.rwth-aachen.de/eval/Cut/.Google Scholar
You have
Access
- 20
- Cited by