Hostname: page-component-745bb68f8f-b6zl4 Total loading time: 0 Render date: 2025-01-09T23:00:08.863Z Has data issue: false hasContentIssue false
  • English
  • Français

Automated termination analysis for logic programs with cut*

Published online by Cambridge University Press:  09 July 2010

PETER SCHNEIDER-KAMP ,
JÜRGEN GIESL ,
THOMAS STRÖDER ,
ALEXANDER SEREBRENIK  and
RENÉ THIEMANN
PETER SCHNEIDER-KAMP
Affiliation:
Department of Mathematics and Computer Science, University of Southern Denmark, Denmark
JÜRGEN GIESL
Affiliation:
LuFG Informatik 2, RWTH Aachen University, Germany
THOMAS STRÖDER
Affiliation:
LuFG Informatik 2, RWTH Aachen University, Germany
ALEXANDER SEREBRENIK
Affiliation:
Department of Mathematics and Computer Science, TU Eindhoven, The Netherlands
RENÉ THIEMANN
Affiliation:
Institute of Computer Science, University of Innsbruck, Austria
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Keywords

automated termination analysiscutdefinite logic programs
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

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

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
Apt, K. R. 1997. From Logic Programming to Prolog. Prentice Hall, London.Google 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