{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T09:46:29Z","timestamp":1780566389410,"version":"3.54.1"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2009,10,1]],"date-time":"2009-10-01T00:00:00Z","timestamp":1254355200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["GI 274\/5-2"],"award-info":[{"award-number":["GI 274\/5-2"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2009,10]]},"abstract":"<jats:p>\n            There are two kinds of approaches for termination analysis of logic programs: \u201ctransformational\u201d and \u201cdirect\u201d ones. Direct approaches prove termination directly on the basis of the logic program. Transformational approaches transform a logic program into a Term Rewrite System (TRS) and then analyze termination of the resulting TRS instead. Thus, transformational approaches make all methods previously developed for TRSs available for logic programs as well. However, the applicability of most existing transformations is quite restricted, as they can only be used for certain subclasses of logic programs. (Most of them are restricted to\n            <jats:italic>well-moded<\/jats:italic>\n            programs.) In this article we improve these transformations such that they become applicable for\n            <jats:italic>any<\/jats:italic>\n            definite logic program. To simulate the behavior of logic programs by TRSs, we slightly modify the notion of rewriting by permitting infinite terms. We show that our transformation results in TRSs which are indeed suitable for\n            <jats:italic>automated<\/jats:italic>\n            termination analysis. In contrast to most other methods for termination of logic programs, our technique is also sound for logic programming\n            <jats:italic>without occur check<\/jats:italic>\n            , which is typically used in practice. We implemented our approach in the termination prover AProVE and successfully evaluated it on a large collection of examples.\n          <\/jats:p>","DOI":"10.1145\/1614431.1614433","type":"journal-article","created":{"date-parts":[[2009,11,4]],"date-time":"2009-11-04T18:28:31Z","timestamp":1257359311000},"page":"1-52","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Automated termination proofs for logic programs by term rewriting"],"prefix":"10.1145","volume":"11","author":[{"given":"Peter","family":"Schneider-Kamp","sequence":"first","affiliation":[{"name":"University of Southern Denmark, Odense M, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexander","family":"Serebrenik","sequence":"additional","affiliation":[{"name":"Eindhoven University of Technology, Eindhoven, The Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[{"name":"University of Innsbruck, Innsbruck, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2009,11,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'93)","volume":"761","author":"Aguzzi G.","unstructured":"Aguzzi , G. and Modigliani , U . 1993. Proving termination of logic programs by transforming them into equivalent term rewriting systems . In Proceedings of the Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'93) . Lecture Notes in Computer Science , vol. 761 . Springer, 114--124. Aguzzi, G. and Modigliani, U. 1993. Proving termination of logic programs by transforming them into equivalent term rewriting systems. In Proceedings of the Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'93). Lecture Notes in Computer Science, vol. 761. Springer, 114--124."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the Symposium on Mathematical Foundations of Computer Science (MFCS'93)","volume":"711","author":"Apt K. R.","unstructured":"Apt , K. R. and Etalle , S . 1993. On the unification free Prolog programs . In Proceedings of the Symposium on Mathematical Foundations of Computer Science (MFCS'93) . Lecture Notes in Computer Science , vol. 711 . Springer, 1--19. Apt, K. R. and Etalle, S. 1993. On the unification free Prolog programs. In Proceedings of the Symposium on Mathematical Foundations of Computer Science (MFCS'93). Lecture Notes in Computer Science, vol. 711. Springer, 1--19."},{"key":"e_1_2_1_3_1","volume-title":"From Logic Programming to Prolog","author":"Apt K. R.","unstructured":"Apt , K. R. 1997. From Logic Programming to Prolog . Prentice Hall , London . Apt, K. R. 1997. From Logic Programming to Prolog. Prentice Hall, London."},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the International Workshop on Logic-Based Program Synthesis and Transformation (LOPSTR'95)","volume":"1048","author":"Arts T.","unstructured":"Arts , T. and Zantema , H . 1995. Termination of logic programs using semantic unification . In Proceedings of the International Workshop on Logic-Based Program Synthesis and Transformation (LOPSTR'95) . Lecture Notes in Computer Science , vol. 1048 . Springer, 219--233. Arts, T. and Zantema, H. 1995. Termination of logic programs using semantic unification. In Proceedings of the International Workshop on Logic-Based Program Synthesis and Transformation (LOPSTR'95). Lecture Notes in Computer Science, vol. 1048. Springer, 219--233."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press.   Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press.","DOI":"10.1017\/CBO9781139172752"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the European Symposium on Programming (ESOP'92)","volume":"582","author":"Bossi A.","unstructured":"Bossi , A. , Cocco , N. , and Fabris , M . 1992. Typed norms . In Proceedings of the European Symposium on Programming (ESOP'92) . Lecture Notes in Computer Science , vol. 582 . Springer, 73--92. Bossi, A., Cocco, N., and Fabris, M. 1992. Typed norms. In Proceedings of the European Symposium on Programming (ESOP'92). Lecture Notes in Computer Science, vol. 582. Springer, 73--92."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the International Static Analysis Symposium (SAS'96)","volume":"1145","author":"Bruynooghe M.","unstructured":"Bruynooghe , M. , Demoen , B. , Boulanger , D. , Denecker , M. , and Mulkers , A . 1996. A freeness and sharing analysis of logic programs based on a pre-interpretation . In Proceedings of the International Static Analysis Symposium (SAS'96) . Lecture Notes in Computer Science , vol. 1145 . Springer, 128--142. Bruynooghe, M., Demoen, B., Boulanger, D., Denecker, M., and Mulkers, A. 1996. A freeness and sharing analysis of logic programs based on a pre-interpretation. In Proceedings of the International Static Analysis Symposium (SAS'96). Lecture Notes in Computer Science, vol. 1145. Springer, 128--142."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_5"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1216374.1216378"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the International Static Analysis Symposium (SAS'98)","volume":"1503","author":"Charatonik W.","unstructured":"Charatonik , W. and Podelski , A . 1998. Directional type inference for logic programs . In Proceedings of the International Static Analysis Symposium (SAS'98) . Lecture Notes in Computer Science , vol. 1503 . Springer, 278--294. Charatonik, W. and Podelski, A. 1998. Directional type inference for logic programs. In Proceedings of the International Static Analysis Symposium (SAS'98). Lecture Notes in Computer Science, vol. 1503. Springer, 278--294."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(99)00006-0"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562931_25"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_16"},{"key":"e_1_2_1_15_1","unstructured":"Codish M. 2007. Collection of benchmarks. http:\/\/lvs.cs.bgu.ac.il\/~mcodish\/suexec\/terminweb\/bin\/terminweb.cgi?command=examples.  Codish M. 2007. Collection of benchmarks. http:\/\/lvs.cs.bgu.ac.il\/~mcodish\/suexec\/terminweb\/bin\/terminweb.cgi?command=examples."},{"key":"e_1_2_1_16_1","volume-title":"Academic","author":"Colmerauer A.","unstructured":"Colmerauer , A. 1982. Prolog and infinite trees . In Logic Programming, K. L. Clark and S. Tarnlund, Eds. Academic Press , Oxford, UK . Colmerauer, A. 1982. Prolog and infinite trees. In Logic Programming, K. L. Clark and S. Tarnlund, Eds. Academic Press, Oxford, UK."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10026-2"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90027-2"},{"key":"e_1_2_1_19_1","volume-title":"Eds. Lecture Notes in Computer Science","volume":"2407","author":"De Schreye D.","unstructured":"De Schreye , D. and Serebrenik , A . 2002. Acceptability with general orderings. In Computational Logic: Logic Programming and Beyond. Essays in Honour of Robert A. Kowalski, Part I, A. C. Kakas and F. Sadri , Eds. Lecture Notes in Computer Science , vol. 2407 . Springer, 187--210. De Schreye, D. and Serebrenik, A. 2002. Acceptability with general orderings. In Computational Logic: Logic Programming and Beyond. Essays in Honour of Robert A. Kowalski, Part I, A. C. Kakas and F. Sadri, Eds. Lecture Notes in Computer Science, vol. 2407. Springer, 187--210."},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the International Logic Programming Symposium (ILPS'93)","author":"Decorte S.","unstructured":"Decorte , S. , De Schreye , D. , and Fabris , M . 1993. Automatic inference of norms: A missing link in automatic termination analysis . In Proceedings of the International Logic Programming Symposium (ILPS'93) . MIT Press, Boston, 420--436. Decorte, S., De Schreye, D., and Fabris, M. 1993. Automatic inference of norms: A missing link in automatic termination analysis. In Proceedings of the International Logic Programming Symposium (ILPS'93). MIT Press, Boston, 420--436."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80022-6"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_47"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the International Sympsium on Practical Aspects of Declarative Languages (PADL'02)","volume":"2257","author":"Gallagher J. P.","unstructured":"Gallagher , J. P. and Puebla , G . 2002. Abstract interpretation over non-deterministic finite tree automata for set-based analysis of logic programs . In Proceedings of the International Sympsium on Practical Aspects of Declarative Languages (PADL'02) . Lecture Notes in Computer Science , vol. 2257 . Springer, 243--261. Gallagher, J. P. and Puebla, G. 2002. Abstract interpretation over non-deterministic finite tree automata for set-based analysis of logic programs. In Proceedings of the International Sympsium on Practical Aspects of Declarative Languages (PADL'02). Lecture Notes in Computer Science, vol. 2257. Springer, 243--261."},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the International Workshop on Conditional and Typed Rewriting Systems (CTRS '92)","volume":"656","author":"Ganzinger H.","unstructured":"Ganzinger , H. and Waldmann , U . 1993. Termination proofs of well-moded logic programs via conditional rewrite systems . In Proceedings of the International Workshop on Conditional and Typed Rewriting Systems (CTRS '92) . Lecture Notes in Computer Science , vol. 656 . Springer, 430--437. Ganzinger, H. and Waldmann, U. 1993. Termination proofs of well-moded logic programs via conditional rewrite systems. In Proceedings of the International Workshop on Conditional and Typed Rewriting Systems (CTRS '92). Lecture Notes in Computer Science, vol. 656. Springer, 430--437."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00200-004-0162-8"},{"key":"e_1_2_1_26_1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Proceedings of the International Conference on Logic Programming Artificial Intelligence and Reasoning (LPAR'04)","author":"Giesl J.","unstructured":"Giesl , J. , Thiemann , R. , and Schneider-Kamp , P. 2005. The dependency pair framework: Combining techniques for automated termination proofs . In Proceedings of the International Conference on Logic Programming Artificial Intelligence and Reasoning (LPAR'04) . Lecture Notes in Artificial Intelligence , vol. 3452 . Springer , 301--331. Giesl, J., Thiemann, R., and Schneider-Kamp, P. 2005. The dependency pair framework: Combining techniques for automated termination proofs. In Proceedings of the International Conference on Logic Programming Artificial Intelligence and Reasoning (LPAR'04). Lecture Notes in Artificial Intelligence, vol. 3452. Springer, 301--331."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_24"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_23"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9057-7"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.10.004"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90032-X"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(97)00028-9"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571168"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the International Conference on Logic Programming (ICLP'03)","volume":"2916","author":"Lagoon V.","unstructured":"Lagoon , V. , Mesnard , F. , and Stuckey , P. J . 2003. Termination analysis with types is more accurate . In Proceedings of the International Conference on Logic Programming (ICLP'03) . Lecture Notes in Computer Science , vol. 2916 . Springer, 254--268. Lagoon, V., Mesnard, F., and Stuckey, P. J. 2003. Termination analysis with types is more accurate. In Proceedings of the International Conference on Logic Programming (ICLP'03). Lecture Notes in Computer Science, vol. 2916. Springer, 254--268."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567078"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the International Workshop on Logic-Based Program Synthesis and Transformation (LOPSTR'96)","volume":"1207","author":"Leuschel M.","unstructured":"Leuschel , M. and S\u00f8rensen , M. H . 1996. Redundant argument filtering of logic programs . In Proceedings of the International Workshop on Logic-Based Program Synthesis and Transformation (LOPSTR'96) . Lecture Notes in Computer Science , vol. 1207 . Springer, 83--103. Leuschel, M. and S\u00f8rensen, M. H. 1996. Redundant argument filtering of logic programs. In Proceedings of the International Workshop on Logic-Based Program Synthesis and Transformation (LOPSTR'96). Lecture Notes in Computer Science, vol. 1207. Springer, 83--103."},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the International Conference on Computer Aided Verification (CAV'97)","volume":"1254","author":"Lindenstrauss N.","unstructured":"Lindenstrauss , N. , Sagiv , Y. , and Serebrenik , A . 1997. TermiLog: A system for checking termination of queries to logic programs . In Proceedings of the International Conference on Computer Aided Verification (CAV'97) . Lecture Notes in Computer Science , vol. 1254 . Springer, 444--447. Lindenstrauss, N., Sagiv, Y., and Serebrenik, A. 1997. TermiLog: A system for checking termination of queries to logic programs. In Proceedings of the International Conference on Computer Aided Verification (CAV'97). Lecture Notes in Computer Science, vol. 1254. Springer, 444--447."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/351268.351293"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the International Conference on Rewriting Techniques and Applications (RTA'07)","volume":"4533","author":"Marche C.","unstructured":"Marche , C. and Zantema , H . 2007. The termination competition . In Proceedings of the International Conference on Rewriting Techniques and Applications (RTA'07) . Lecture Notes in Computet Science , vol. 4533 . Springer, 303--313. Marche, C. and Zantema, H. 2007. The termination competition. In Proceedings of the International Conference on Rewriting Techniques and Applications (RTA'07). Lecture Notes in Computet Science, vol. 4533. Springer, 303--313."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/647707.734817"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/646057.678339"},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'96)","volume":"1207","author":"Martin J.","unstructured":"Martin , J. , King , A. , and Soper , P . 1996. Typed norms for typed logic programs . In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'96) . Lecture Notes in Computer Science , vol. 1207 . Springer, 224--238. Martin, J., King, A., and Soper, P. 1996. Typed norms for typed logic programs. In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'96). Lecture Notes in Computer Science, vol. 1207. Springer, 224--238."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/635499.635503"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068404002017"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068407003122"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562931_24"},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the 8th International Workshop on Termination (WST'06)","author":"Nguyen M. T.","unstructured":"Nguyen , M. T. , Bruynooghe , M. , De Schreye , D. , and Leuschel , M . 2006. Program specialisation as a pre-processing step for termination analysis . In Proceedings of the 8th International Workshop on Termination (WST'06) . 7--11. http:\/\/www.easychair.org\/FLoC-06\/WST-preproceedings.pdf. Nguyen, M. T., Bruynooghe, M., De Schreye, D., and Leuschel, M. 2006. Program specialisation as a pre-processing step for termination analysis. In Proceedings of the 8th International Workshop on Termination (WST'06). 7--11. http:\/\/www.easychair.org\/FLoC-06\/WST-preproceedings.pdf."},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06)","volume":"4407","author":"Nguyen M. T.","unstructured":"Nguyen , M. T. and De Schreye, D. 2007. Polytool: Proving termination automatically based on polynomial interpretations . In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06) . Lecture Notes in Computer Science , vol. 4407 . Springer, 210--218. Nguyen, M. T. and De Schreye, D. 2007. Polytool: Proving termination automatically based on polynomial interpretations. In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06). Lecture Notes in Computer Science, vol. 4407. Springer, 210--218."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78769-3_2"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.5555\/647199.718692"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002000100064"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1119479.1119481"},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the International Conference on Logic Programming (ICLP'97)","author":"van Raamsdonk F.","year":"1997","unstructured":"van Raamsdonk , F. 1997 . Translating logic programs into conditional rewriting systems . In Proceedings of the International Conference on Logic Programming (ICLP'97) . MIT Press, Boston, 168--182. van Raamsdonk, F. 1997. Translating logic programs into conditional rewriting systems. In Proceedings of the International Conference on Logic Programming (ICLP'97). MIT Press, Boston, 168--182."},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06)","volume":"4407","author":"Schneider-Kamp P.","unstructured":"Schneider-Kamp , P. , Giesl , J. , Serebrenik , A. , and Thiemann , R . 2007. Automated termination analysis for logic programs by term rewriting . In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06) . Lecture Notes in Computer Science , vol. 4407 . Springer, 177--193. Schneider-Kamp, P., Giesl, J., Serebrenik, A., and Thiemann, R. 2007. Automated termination analysis for logic programs by term rewriting. In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06). Lecture Notes in Computer Science, vol. 4407. Springer, 177--193."},{"key":"e_1_2_1_56_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'03)","author":"Serebrenik A.","unstructured":"Serebrenik , A. and De Schreye , D. 2003. Proving termination with adornments . In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'03) . Lecture Notes in Computer Science , vol. 3018 . Springer , 108--109. Serebrenik, A. and De Schreye, D. 2003. Proving termination with adornments. In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'03). Lecture Notes in Computer Science, vol. 3018. Springer, 108--109."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068404002042"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068404002248"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-6546-z"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27775-0_4"},{"key":"e_1_2_1_61_1","volume-title":"Proceedings of the International Workshop on Termination (WST'04)","author":"Tamary L.","year":"2004","unstructured":"Tamary , L. and Codish , M . 2004. Abstract partial evaluation for termination analysis . In Proceedings of the International Workshop on Termination (WST'04) 47--50. http:\/\/aib.informatik.rwth-aachen.de\/ 2004 \/2004-07.pdf. Tamary, L. and Codish, M. 2004. Abstract partial evaluation for termination analysis. In Proceedings of the International Workshop on Termination (WST'04) 47--50. http:\/\/aib.informatik.rwth-aachen.de\/2004\/2004-07.pdf."},{"key":"e_1_2_1_62_1","unstructured":"TPDB. 2007. The termination problem data base 4.0. http:\/\/www.lri.fr\/~marche\/tpdb\/.  TPDB. 2007. The termination problem data base 4.0. http:\/\/www.lri.fr\/~marche\/tpdb\/."},{"key":"e_1_2_1_63_1","volume-title":"Proceedings of the International Static Analysis Symposium (SAS '02)","volume":"2477","author":"Vaucheret C.","unstructured":"Vaucheret , C. and Bueno , F . 2002. More precise yet efficient type inference for logic programs . In Proceedings of the International Static Analysis Symposium (SAS '02) . Lecture Notes in Computer Science , vol. 2477 . Springer, 102--116. Vaucheret, C. and Bueno, F. 2002. More precise yet efficient type inference for logic programs. In Proceedings of the International Static Analysis Symposium (SAS '02). Lecture Notes in Computer Science, vol. 2477. Springer, 102--116."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(94)90063-9"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.5555\/2428096.2428100"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1614431.1614433","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1614431.1614433","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:18:06Z","timestamp":1750249086000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1614431.1614433"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,10]]},"references-count":64,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,10]]}},"alternative-id":["10.1145\/1614431.1614433"],"URL":"https:\/\/doi.org\/10.1145\/1614431.1614433","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,10]]},"assertion":[{"value":"2008-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-11-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}