{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T19:51:44Z","timestamp":1672516304157},"reference-count":42,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2010,2,25]],"date-time":"2010-02-25T00:00:00Z","timestamp":1267056000000},"content-version":"unspecified","delay-in-days":0,"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":[[2011,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Our goal is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, we show how to adapt termination analysis techniques based on polynomial interpretations\u2014very well known in the context of term rewrite systems\u2014to obtain new (nontransformational) termination analysis techniques for definite logic programs (LPs). This leads to an approach that can be seen as a direct generalization of the traditional techniques in termination analysis of LPs, where linear norms and level mappings are used. Our extension generalizes these to arbitrary polynomials. We extend a number of standard concepts and results on termination analysis to the context of polynomial interpretations. We also propose a constraint-based approach for automatically generating polynomial interpretations that satisfy the termination conditions. Based on this approach, we implemented a new tool, called <jats:monospace>Polytool<\/jats:monospace>, for automatic termination analysis of LPs.<\/jats:p>","DOI":"10.1017\/s1471068410000025","type":"journal-article","created":{"date-parts":[[2010,2,25]],"date-time":"2010-02-25T09:51:42Z","timestamp":1267091502000},"page":"33-63","source":"Crossref","is-referenced-by-count":7,"title":["<tt>Polytool<\/tt>: Polynomial interpretations as a basis for termination analysis of logic programs"],"prefix":"10.1017","volume":"11","author":[{"given":"MANH THANG","family":"NGUYEN","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"DANNY","family":"DE SCHREYE","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00dcRGEN","family":"GIESL","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"PETER","family":"SCHNEIDER-KAMP","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2010,2,25]]},"reference":[{"key":"S1471068410000025_ref15","first-page":"340","volume-title":"Proc. SAT \u201907","author":"Fuhs","year":"2007"},{"key":"S1471068410000025_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/1216374.1216378"},{"key":"S1471068410000025_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.10.004"},{"key":"S1471068410000025_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/3540539816_66"},{"key":"S1471068410000025_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"S1471068410000025_ref35","first-page":"270","volume-title":"Proc. RTA \u201900","author":"Ohlebusch","year":"2000"},{"key":"S1471068410000025_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-9022-x"},{"key":"S1471068410000025_ref17","first-page":"280","volume-title":"Proc. ICLP \u201905","author":"Gallagher","year":"2005"},{"key":"S1471068410000025_ref27","first-page":"63","volume-title":"Proc. ICLP \u201997","author":"Lindenstrauss","year":"1997"},{"key":"S1471068410000025_ref1","first-page":"493","volume-title":"Handbook of Theoretical Computer Science","author":"Apt","year":"1990"},{"key":"S1471068410000025_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9057-7"},{"key":"S1471068410000025_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/330643.330645"},{"key":"S1471068410000025_ref13","unstructured":"Dershowitz N. , Lindenstrauss N. and Sagiv Y. 1997. What norms are useful for logic programs? In Proc. WST \u201997. Transparencies available from URL: http:\/\/www.cs.huji.ac.il\/~naomil\/."},{"key":"S1471068410000025_ref32","first-page":"311","volume-title":"Proc. ICLP \u201905","author":"Nguyen","year":"2005"},{"key":"S1471068410000025_ref12","first-page":"16","volume-title":"Proc. French Spring School in Theoretical Computer Science","author":"Dershowitz","year":"1995"},{"key":"S1471068410000025_ref5","first-page":"254","volume-title":"Proc. CADE \u201998","author":"Brauburger","year":"1998"},{"key":"S1471068410000025_ref36","volume-title":"Proc. LOPSTR \u201909","author":"Schneider-Kamp"},{"key":"S1471068410000025_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(00)00006-6"},{"key":"S1471068410000025_ref10","first-page":"420","volume-title":"Proc. ILPS \u201993","author":"Decorte","year":"1993"},{"key":"S1471068410000025_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(99)00006-0"},{"key":"S1471068410000025_ref34","first-page":"8","volume-title":"Proc. LOPSTR \u201907","author":"Nguyen","year":"2008"},{"key":"S1471068410000025_ref26","unstructured":"Lindenstrauss N. 2000. TermiLog: Termination analyzer for logic programs. URL: http:\/\/www.cs.huji.ac.il\/~naomil\/termilog.php."},{"key":"S1471068410000025_ref18","first-page":"281","volume-title":"Proc. IJCAR \u201906","author":"Giesl","year":"2006"},{"key":"S1471068410000025_ref7","first-page":"35","volume-title":"Proc. SAS \u201905","author":"Bruynooghe","year":"2005"},{"key":"S1471068410000025_ref20","first-page":"443","volume-title":"Proc. CADE \u201907","author":"Giesl","year":"2007"},{"key":"S1471068410000025_ref16","unstructured":"Fuhs C. , Giesl J. , Middeldorp A. , Schneider-Kamp P. , Thiemann R. and Zankl H. 2008. Maximal termination. In Proc. RTA \u201908, 110\u2013125."},{"key":"S1471068410000025_ref25","volume-title":"On Proving Term Rewriting Systems are Noetherian","author":"Lankford","year":"1979"},{"key":"S1471068410000025_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25951-0_14"},{"key":"S1471068410000025_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-83189-8"},{"key":"S1471068410000025_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90032-X"},{"key":"S1471068410000025_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068404002017"},{"key":"S1471068410000025_ref31","unstructured":"Nguyen M. T. 2009 Termination Analysis: Crossing Paradigm Borders. Ph.D. thesis, Department of Computer Science, K. U. Leuven, Belgium."},{"key":"S1471068410000025_ref33","first-page":"210","volume-title":"Proc. LOPSTR \u201906","author":"Nguyen","year":"2007"},{"key":"S1471068410000025_ref23","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005983105493"},{"key":"S1471068410000025_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/1614431.1614433"},{"key":"S1471068410000025_ref38","doi-asserted-by":"crossref","unstructured":"Serebrenik A. 2003. Termination Analysis of Logic Programs. Ph.D. thesis, Department of Computer Science, K. U. Leuven, Belgium. URL: http:\/\/www.cs.kuleuven.ac.be\/publicaties\/doctoraten\/cw\/CW2003_02.abs.html.","DOI":"10.1007\/978-3-540-24599-5_45"},{"key":"S1471068410000025_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45628-7_9"},{"key":"S1471068410000025_ref39","unstructured":"Serebrenik A. and De Schreye D. 2003. Hasta-La-Vista: Termination analyser for logic programs. In Proc. WLPE \u201903. Eds. Mesnard F. and Serebrenik A. , 60\u201374."},{"key":"S1471068410000025_ref40","first-page":"18","volume-title":"Proc. FSTTCS \u201992","author":"Steinbach","year":"1992"},{"key":"S1471068410000025_ref41","unstructured":"Taboch C. , Genaim S. and Codish M. 2002. TerminWeb: Semantics-based termination analyser for logic programs. URL: http:\/\/www.cs.bgu.ac.il\/~mcodish\/TerminWeb."},{"key":"S1471068410000025_ref42","first-page":"301","volume-title":"Proc. ICLP \u201991","author":"Verschaetse","year":"1991"},{"key":"S1471068410000025_ref3","first-page":"294","volume-title":"Proc. CADE \u201909","author":"Borralleras","year":"2009"}],"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\/S1471068410000025","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T20:08:42Z","timestamp":1556395722000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068410000025\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,2,25]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["S1471068410000025"],"URL":"https:\/\/doi.org\/10.1017\/s1471068410000025","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,2,25]]}}}