{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T17:11:17Z","timestamp":1712250677058},"reference-count":26,"publisher":"Cambridge University Press (CUP)","issue":"4-6","license":[{"start":{"date-parts":[[2010,7,9]],"date-time":"2010-07-09T00:00:00Z","timestamp":1278633600000},"content-version":"unspecified","delay-in-days":8,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2010,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 <jats:monospace>Prolog<\/jats:monospace> programs typically use the <jats:italic>cut<\/jats:italic> operator. We introduce a novel pre-processing method which automatically transforms <jats:monospace>Prolog<\/jats:monospace> 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 <jats:monospace>AProVE<\/jats:monospace> and evaluated it successfully with extensive experiments.<\/jats:p>","DOI":"10.1017\/s1471068410000165","type":"journal-article","created":{"date-parts":[[2010,7,9]],"date-time":"2010-07-09T12:44:40Z","timestamp":1278679480000},"page":"365-381","source":"Crossref","is-referenced-by-count":20,"title":["Automated termination analysis for logic programs with cut"],"prefix":"10.1017","volume":"10","author":[{"given":"PETER","family":"SCHNEIDER-KAMP","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00dcRGEN","family":"GIESL","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"THOMAS","family":"STR\u00d6DER","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ALEXANDER","family":"SEREBRENIK","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"REN\u00c9","family":"THIEMANN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2010,7,9]]},"reference":[{"key":"S1471068410000165_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068402001540"},{"key":"S1471068410000165_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(99)00012-6"},{"key":"S1471068410000165_ref10","first-page":"134","volume-title":"LPAR '93","author":"Fil\u00e9","year":"1993"},{"key":"S1471068410000165_ref25","first-page":"455","volume-title":"AMAST '98","author":"Spoto","year":"1998"},{"key":"S1471068410000165_ref23","first-page":"465","volume-title":"ILPS '95","author":"S\u00f8rensen","year":"1995"},{"key":"S1471068410000165_ref11","first-page":"281","volume-title":"Proc. IJCAR '06","author":"Giesl","year":"2006"},{"key":"S1471068410000165_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61411-8"},{"key":"S1471068410000165_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1614431.1614433"},{"key":"S1471068410000165_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90027-2"},{"key":"S1471068410000165_ref2","volume-title":"From Logic Programming to Prolog","author":"Apt","year":"1997"},{"key":"S1471068410000165_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90072-L"},{"key":"S1471068410000165_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90197-P"},{"key":"S1471068410000165_ref19","doi-asserted-by":"crossref","unstructured":"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).","DOI":"10.1017\/S1471068410000025"},{"key":"S1471068410000165_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1216374.1216378"},{"key":"S1471068410000165_ref18","first-page":"374","volume-title":"Ershov Memorial Conference","author":"Mogensen","year":"1996"},{"key":"S1471068410000165_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90030-7"},{"key":"S1471068410000165_ref14","first-page":"39","volume-title":"WRLA '00","author":"Kulas","year":"2000"},{"key":"S1471068410000165_ref22","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068404002248"},{"key":"S1471068410000165_ref12","first-page":"297","volume-title":"RTA '06","author":"Giesl","year":"2006"},{"key":"S1471068410000165_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068407003122"},{"key":"S1471068410000165_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068402001485"},{"key":"S1471068410000165_ref26","unstructured":"Str\u00f6der T. 2010. Towards termination analysis of real Prolog programs. Diploma Thesis, RWTH Aachen. http:\/\/aprove.informatik.rwth-aachen.de\/eval\/Cut\/."},{"key":"S1471068410000165_ref5","unstructured":"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\u2013340."},{"key":"S1471068410000165_ref15","first-page":"157","volume-title":"ILPS '94","author":"Le Charlier","year":"1994"},{"key":"S1471068410000165_ref21","unstructured":"Schneider-Kamp P. , Giesl J. , Serebrenik A. , Str\u00f6der 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."},{"key":"S1471068410000165_ref16","first-page":"375","volume-title":"AMAST '96","author":"Marchiori","year":"1996"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068410000165","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T19:31:42Z","timestamp":1556479902000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068410000165\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7]]},"references-count":26,"journal-issue":{"issue":"4-6","published-print":{"date-parts":[[2010,7]]}},"alternative-id":["S1471068410000165"],"URL":"https:\/\/doi.org\/10.1017\/s1471068410000165","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,7]]}}}