{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,14]],"date-time":"2024-05-14T00:06:12Z","timestamp":1715645172467},"reference-count":16,"publisher":"Cambridge University Press (CUP)","issue":"4-5","license":[{"start":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T00:00:00Z","timestamp":1380067200000},"content-version":"unspecified","delay-in-days":86,"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":[[2013,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A large body of work has been dedicated to termination analysis of logic programs but relatively little has been done to analyze <jats:italic>non<\/jats:italic>-termination. In our opinion, <jats:italic>explaining<\/jats:italic> non-termination is a much more important task because it can dramatically improve a user's ability to effectively debug large, complex logic programs without having to abide by punishing syntactic restrictions. Non-termination analysis examines program execution history when the program is suspected to not terminate and informs the programmer about the exact reasons for this behavior. In Liang and Kifer (2013), we studied the problem of non-termination in tabled logic engines with subgoal abstraction, such as XSB, and proposed a suite of algorithms for non-termination analysis, called <jats:monospace>Terminyzer<\/jats:monospace>. These algorithms analyze forest logging traces and output sequences of tabled subgoal calls that are the likely causes of non-terminating cycles. However, this feedback was hard to use in practice: the same subgoal could occur in multiple rule heads and in even more places in rule bodies, so <jats:monospace>Terminyzer<\/jats:monospace> left too much tedious, sometimes combinatorially large amount of work for the user to do manually.<\/jats:p><jats:p>Here we propose a new suite of algorithms, <jats:monospace>Terminyzer+<\/jats:monospace>, which closes this usability gap. <jats:monospace>Terminyzer+<\/jats:monospace> can detect not only sequences of subgoals that cause non-termination, but, importantly, the exact rules where they occur and the rule sequences that get fired in a cyclic manner, thus causing non-termination. This makes <jats:monospace>Terminyzer+<\/jats:monospace> suitable as a back-end for user-friendly graphical interfaces on top of <jats:monospace>Terminyzer+<\/jats:monospace>, which can greatly simplify the debugging process. <jats:monospace>Terminyzer+<\/jats:monospace> back-ends exist for the SILK system as well as for the open-source <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S1471068413000446_inline1\"\/><jats:tex-math>${\\cal F}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula><jats:sc>lora<\/jats:sc>-<jats:italic>2<\/jats:italic> system. A graphical interface has been developed for SILK and is currently underway for <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S1471068413000446_inline1\"\/><jats:tex-math>${\\cal F}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula><jats:sc>lora<\/jats:sc>-<jats:italic>2<\/jats:italic>. We also report experimental studies, which confirm the effectiveness of <jats:monospace>Terminyzer+<\/jats:monospace> on a host of large real-world knowledge bases. All tests used in this paper are available online.<jats:sup>1<\/jats:sup><\/jats:p><jats:p>In addition, we make a step towards automatic remediation of non-terminating programs by proposing an algorithm that heuristically fixes some causes of misbehavior. Furthermore, unlike <jats:monospace>Terminyzer<\/jats:monospace>, <jats:monospace>Terminyzer+<\/jats:monospace> does not require the underlying logic engine to support subgoal abstraction, although it can make use of it.<\/jats:p>","DOI":"10.1017\/s1471068413000446","type":"journal-article","created":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T16:24:58Z","timestamp":1380126298000},"page":"705-719","source":"Crossref","is-referenced-by-count":6,"title":["A practical analysis of non-termination in large logic programs"],"prefix":"10.1017","volume":"13","author":[{"given":"SENLIN","family":"LIANG","sequence":"first","affiliation":[]},{"given":"MICHAEL","family":"KIFER","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2013,9,25]]},"reference":[{"key":"S1471068413000446_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78769-3_2"},{"key":"S1471068413000446_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71410-1_15"},{"key":"S1471068413000446_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000500"},{"key":"S1471068413000446_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000512"},{"key":"S1471068413000446_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25951-0_14"},{"key":"S1471068413000446_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90027-2"},{"key":"S1471068413000446_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210335"},{"key":"S1471068413000446_ref13","doi-asserted-by":"crossref","DOI":"10.1145\/230514.571645","volume-title":"Introduction to the Theory of Computation","author":"Sipser","year":"1996"},{"key":"S1471068413000446_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(93)90039-J"},{"key":"S1471068413000446_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90004-L"},{"key":"S1471068413000446_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/1216374.1216378"},{"key":"S1471068413000446_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000457"},{"key":"S1471068413000446_ref7","volume-title":"Practical Aspects of Declarative Languages","author":"Liang","year":"2013"},{"key":"S1471068413000446_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000165"},{"key":"S1471068413000446_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/371282.371357"},{"key":"S1471068413000446_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000445"}],"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\/S1471068413000446","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,13]],"date-time":"2024-05-13T09:28:44Z","timestamp":1715592524000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068413000446\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7]]},"references-count":16,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2013,7]]}},"alternative-id":["S1471068413000446"],"URL":"https:\/\/doi.org\/10.1017\/s1471068413000446","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7]]}}}