No CrossRef data available.
Article contents
Non-termination analysis of logic programs with integer arithmetics
Published online by Cambridge University Press: 06 July 2011
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.
In the past years, analyzers have been introduced to detect classes of non-terminating queries for definite logic programs. Although these non-termination analyzers have shown to be rather precise, their applicability on real-life Prolog programs is limited because most Prolog programs use non-logical features. As a first step towards the analysis of Prolog programs, this paper presents a non-termination condition for Logic Programs containing integer arithmetics. The analyzer is based on our non-termination analyzer presented at International Logic Programming Conference (ICLP) 2009. The analysis starts from a class of queries and infers a subclass of non-terminating ones. In first phase, we ignore the outcome (success or failure) of the arithmetic operations, assuming success of all arithmetic calls. In second phase, we characterize successful arithmetic calls as a constraint problem, the solution of which determines the non-terminating queries.
Information
- Type
- Regular Papers
- Information
- Theory and Practice of Logic Programming , Volume 11 , Special Issue 4-5: 27th International Conference on Logic Programming , July 2011 , pp. 521 - 536
- Copyright
- Copyright © Cambridge University Press 2011
References
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
En, N. and Srensson, N. 2003. An extensible sat-solver. In SAT, Giunchiglia, E. and Tacchella, A., Eds. Lecture Notes in Computer Science (LNCS), vol. 2919. Springer, New York, 502–518.Google Scholar
Giesl, J., Schneider-kamp, P. and Thiemann, R. 2006. Aprove 1.2: Automatic termination proofs in the dependency pair framework. In Third International Joint Conference on Automated Reasoning (IJCAR 06). Springer-Verlag, Berlin, Germany, 281–286.CrossRefGoogle Scholar
Lloyd, J. W. 1987. Foundations of Logic Programming, 2nd ed. Springer, New York.CrossRefGoogle Scholar
Nguyen, M. T., De Schreye, D., Giesl, J. and Schneider-Kamp, P. 2011. Polytool: Polynomial interpretations as a basis for termination analysis of logic programs. Theory and Practice of Logic Programming, 11 (1), 33–63.CrossRefGoogle Scholar
Payet, É. and Mesnard, F. 2006. Nontermination inference of logic programs. ACM Transactions on Programming Languages and Systems 28 (2), 256–289.CrossRefGoogle Scholar
Serebrenik, A. and De Schreye, D. 2001. Inference of termination conditions for numerical loops in prolog. In International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Nieuwenhuis, R. and Voronkov, A., Eds. Lecture Notes in Computer Science (LNCS), vol. 2250. Springer, New York, 654–668.Google Scholar
Shen, Y.-D., De Schreye, D. and Voets, D. 2009. Termination prediction for general logic programs. Theory and Practice of Logic Programming 9 (6), 751–780.CrossRefGoogle Scholar
Shen, Y., You, J., Yuan, L., Shen, S. S. P. and Yang, Q. 2003. A dynamic approach to characterizing termination of general logic programs. Transactions on Computational Logic 4 (4), 417–430.CrossRefGoogle Scholar
Voets, D. and De Schreye, D. 2009. A new approach to non-termination analysis of logic programs. In International Logic Programming Conference (ICLP), Hill, P. M. and Warren, D. S., Eds. Lecture Notes in Computer Science (LNCS), vol. 5649. Springer, New York, 220–234.Google Scholar
Voets, D. and De Schreye, D. 2010. Non-termination analysis of logic programs using types. In Proceedings of Logic Program Synthesis and Transformation (LOPSTR). Alpuente, M., Ed. Lecture Notes in Computer Science (LNCS), vol. 6564. Springer, New York, 133–148.Google Scholar
You have
Access
- 6
- Cited by