{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:23:08Z","timestamp":1725664988763},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540627180"},{"type":"electronic","value":"9783540684947"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62718-9_7","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:49:40Z","timestamp":1330278580000},"page":"104-129","source":"Crossref","is-referenced-by-count":4,"title":["Replacement can preserve termination"],"prefix":"10.1007","author":[{"given":"Annalisa","family":"Bossi","sequence":"first","affiliation":[]},{"given":"Nicoletta","family":"Cocco","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"7_CR1","volume-title":"Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics","author":"K. R. Apt","year":"1990","unstructured":"K. R. Apt. Introduction to Logic Programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics. Elsevier, Amsterdam and The MIT Press, Cambridge, 1990."},{"key":"7_CR2","unstructured":"K. R. Apt. Declarative programming in Prolog. In D. Miller, editor, Proceedings of the 1993 International Symposium on Logic Programming, pages 12-35. The MIT Press, 1993."},{"issue":"6A","key":"7_CR3","doi-asserted-by":"crossref","first-page":"743","DOI":"10.1007\/BF01213601","volume":"6","author":"K. R. Apt","year":"1994","unstructured":"K. R. Apt and B. Marchiori. Reasoning about Prolog programs: from modes through types to assertions. Formal Aspects of Computing, 6(6A):743\u2013765, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"7_CR4","first-page":"150","volume-title":"Studies in Pure Prolog: termination","author":"K. R. Apt","year":"1990","unstructured":"K. R. Apt and D. Pedreschi. Studies in Pure Prolog: termination. In J.W. Lloyd, editor, Proceedings of the Simposium in Computational Logic, pages 150\u2013176, Berlin, 1990. Springer-Verlag."},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science 526","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-54415-1_50","volume-title":"Proving termination of general Prolog programs","author":"K. R. Apt","year":"1991","unstructured":"K. R. Apt and D. Pedreschi. Proving termination of general Prolog programs. In T. Ito and A. Meyer, editors, Proceedings of the International Conference on Theoretical Aspects of Computer Software, Lecture Notes in Computer Science 526, pages 265\u2013289, Berlin, 1991. Springer-Verlag."},{"key":"7_CR6","volume-title":"Technical Report TRCS-R9238","author":"K. R. Apt","year":"1992","unstructured":"K. R. Apt and Pellegrini. On the occur-check free Prolog programs. Technical Report TRCS-R9238, CWI, Amsterdam, The Netherlands, 1992."},{"key":"7_CR7","volume-title":"PhD thesis","author":"M. Baudinet","year":"1989","unstructured":"M. Baudinet. Logic Programming Semantics: Techniques and Applications. PhD thesis, Stanford University, Stanford, California, 1989."},{"issue":"4","key":"7_CR8","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1145\/1780.1781","volume":"6","author":"R.S. Bird","year":"1984","unstructured":"R.S. Bird. The Promotion and Accumulation Strategies in Transformational Programming. TOPLAS ACM, 6 4):487\u2013504, 1984.","journal-title":"TOPLAS ACM"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science, vol. 352","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/3-540-50940-2_30","volume-title":"TAPSOFT '89","author":"A. Bossi","year":"1989","unstructured":"A. Bossi and N. Cocco. Verifying correctness of logic programs. In J. Diaz and F. Orejas, editors, TAPSOFT '89, Barcelona, Spain, March 1989, (Lecture Notes in Computer Science, vol. 352), pages 96\u2013110. Springer-Verlag, 1989."},{"key":"7_CR10","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/0743-1066(93)90023-A","volume":"16","author":"A. Bossi","year":"1993","unstructured":"A. Bossi and N. Cocco. Basic Transformation Operations which preserve Computed Answer Substitutions of Logic Programs. Journal of Logic Programming, 16:47\u201387, 1993.","journal-title":"Journal of Logic Programming"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"A. Bossi and N. Cocco. Preserving universal termination through unfold\/fold. In G. Levi and M Rodriguez-Artalejo, editors, Proceedings ALP'94, Madrid, Spain, September 1994.","DOI":"10.1007\/3-540-58431-5_19"},{"key":"7_CR12","first-page":"265","volume-title":"volume 649 of Lecture Notes in Computer Science","author":"A. Bossi","year":"1992","unstructured":"A. Bossi, N. Cocco, and S. Etalle. Transforming Normal Programs by Replacement. In A. Pettorossi, editor, Meta Programming in Logic \u2014 Proceedings META '92, volume 649 of Lecture Notes in Computer Science, pages 265\u2013279. Springer-Verlag, Berlin, 1992."},{"issue":"1","key":"7_CR13","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1093\/logcom\/6.1.79","volume":"6","author":"A. Bossi","year":"1996","unstructured":"A. Bossi, N. Cocco, and S. Etalle. Simultaneous Replacement in Normal Programs. Journal of Logic and Computation, 6(1):79\u2013120, 1996.","journal-title":"Journal of Logic and Computation"},{"key":"7_CR14","first-page":"33","volume-title":"volume 1048 of Lecture Notes in Computer Science","author":"A. Bossi","year":"1996","unstructured":"A. Bossi, N. Cocco, and S. Etalle. Transformation of Left Terminating Programs: The Reordering Problem. In M. Proietti, editor, Proceedings LOPSTR'95, volume 1048 of Lecture Notes in Computer Science, pages 33\u201345. Springer-Verlag, Berlin, 1996."},{"key":"7_CR15","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(92)00019-N","volume":"124","author":"A. Bossi","year":"1994","unstructured":"A. Bossi, N. Cocco, and M. Fabris. Norms on terms and their use in proving universal termination of a logic program. Theoretical Computer Science, 124:297\u2013328, 1994.","journal-title":"Theoretical Computer Science"},{"key":"7_CR16","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1016\/0743-1066(87)90010-0","volume":"4","author":"D.R. Brough","year":"1987","unstructured":"D.R. Brough and C.J. Hogger. Compiling Associativity into Logic Programs. Journal of Logic Programming, 4:345\u2013359, 1987.","journal-title":"Journal of Logic Programming"},{"key":"7_CR17","unstructured":"L. Colussi and E. Marchiori. Proving correctness of logic programs using axiomatic semantics. In Proceedings ICLP'91, pages 629\u2013644. MIT Press, 1991."},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"J. Cook and J.P. Gallagher. A transformation system for definite programs based on termination analysis. In G. Levi and M. Rodriguez-Artalejo, editors, LOPSTR'94. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58792-6_4"},{"key":"7_CR19","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0304-3975(88)90099-0","volume":"59","author":"W. Drabent","year":"1988","unstructured":"W. Drabent and J. Maluszynski. Inductive assertion method for logic programs. Theoretical Computer Science, 59:133\u2013155, 1988.","journal-title":"Theoretical Computer Science"},{"key":"7_CR20","unstructured":"U. S. Reddy F. Bronsard, T. K. Lakshman. A framework of directionalities for proving termination of logic programs. In K. R. Apt, editor, Proceedings of the Joint International Conference and Symposium on Logic Programming, pages 321\u2013335. The MIT Press, 1992."},{"key":"7_CR21","unstructured":"P.A. Gardner and J.C. Shepherdson. Unfold\/fold transformations of logic programs. In J-L Lassez and editor G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991."},{"key":"7_CR22","first-page":"413","volume-title":"Preservation of Stronger Equivalence in Unfold\/Fold Logic Programming Transformation","author":"T. Kawamura","year":"1988","unstructured":"T. Kawamura and T. Kanamori. Preservation of Stronger Equivalence in Unfold\/Fold Logic Programming Transformation. In Proc. Int'l Conf. on Fifth Generation Computer Systems, pages 413\u2013422. Institute for New Generation Computer Technology, Tokyo, 1988."},{"key":"7_CR23","first-page":"255","volume-title":"Partial evaluation as a means for inferencing data structures in an applicative language: A theory and implementation in the case of Prolog","author":"H. Komorowski","year":"1982","unstructured":"H. Komorowski. Partial evaluation as a means for inferencing data structures in an applicative language: A theory and implementation in the case of Prolog. In Ninth ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, pages 255\u2013267. ACM, 1982."},{"key":"7_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-83189-8","volume-title":"Foundations of Logic Programming","author":"J. W. Lloyd","year":"1987","unstructured":"J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. Second edition.","edition":"Second edition"},{"key":"7_CR25","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0743-1066(91)90027-M","volume":"11","author":"J. W. Lloyd","year":"1991","unstructured":"J. W. Lloyd and J. C. Shepherdson. Partial Evaluation in Logic Programming. Journal of Logic Programming, 11:217\u2013242, 1991.","journal-title":"Journal of Logic Programming"},{"key":"7_CR26","unstructured":"M.J. Maher. Correctness of a logic program transformation system. IBM Research Report RC13496, T.J. Watson Research Center, 1987."},{"key":"7_CR27","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/BF03037156","volume":"11","author":"K. Marriot","year":"1993","unstructured":"K. Marriot and H. Sondergaard. Difference-list Transformation for Prolog. New Generation Computing, 11:125\u2013177, 1993.","journal-title":"New Generation Computing"},{"key":"7_CR28","unstructured":"N.Jones and A. Mycroft. Stepwise development of operational and denotational semantics for Prolog. In International Symposium on Logic Programming, Atlantic City, NJ, (U.S.A.), pages 289\u2013298, 1984."},{"issue":"20","key":"7_CR29","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1016\/0743-1066(94)90028-0","volume":"19","author":"A. Pettorossi","year":"1994","unstructured":"A. Pettorossi and M. Proietti. Transformation of Logic Programs: Foundations and Techniques. Journal of Logic Programming, 19(20):261\u2013320, 1994.","journal-title":"Journal of Logic Programming"},{"key":"7_CR30","unstructured":"A. Pettorossi and M. Proietti. Transformation of Logic Programs. In J.A. Robinson editors D.M. Gabbay, C.J. Hogger, editor, Handbook of Logic and Artificial Intelligence. Oxford University Press, 1995."},{"key":"7_CR31","volume-title":"volume 446 of Lecture Notes in Artificial Intelligence","author":"L. Pluemer","year":"1990","unstructured":"L. Pluemer. Termination proofs for logic programs, volume 446 of Lecture Notes in Artificial Intelligence. Springer-Verlag, Berlin, 1990."},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"M. Proietti and A. Pettorossi. The synthesis of eureka predicates for developing logic programs. In N. Jones, editor, ESOP'90, (Lecture Notes in Computer Science, Vol. 432), pages 306\u2013325. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52592-0_71"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science, Vol.528","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-54444-5_111","volume-title":"PLILP 91","author":"M. Proietti","year":"1991","unstructured":"M. Proietti and A. Pettorossi. Unfolding, definition, folding, in this order for avoiding unnesessary variables in logic programs. In Maluszynski and M. Wirsing, editors, PLILP 91, Passau, Germany (Lecture Notes in Computer Science, Vol.528), pages 347\u2013358. Springer-Verlag, 1991."},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"M. Proietti and A. Pettorossi. Synthesis of Programs from Unfold\/Fold Proofs. In Y. Deville, editor, LOPSTR'93, pages 141\u2013158, 1994.","DOI":"10.1007\/978-1-4471-3234-9_13"},{"key":"7_CR35","first-page":"175","volume-title":"Lecture Notes in Computer Science, Vol. 463","author":"T. Sato","year":"1990","unstructured":"T. Sato. An equivalence preserving first order unfold\/fold transformation system. In Second Int. Conference on Algebraic and Logic Programming, Nancy, France, October 1990, (Lecture Notes in Computer Science, Vol. 463), pages 175\u2013188. Springer-Verlag, 1990."},{"key":"7_CR36","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/0304-3975(91)90007-O","volume":"86","author":"H. Seki","year":"1991","unstructured":"H. Seki. Unfold\/fold transformation of stratified programs. Journal of Theoretical Computer Science, 86:107\u2013139, 1991.","journal-title":"Journal of Theoretical Computer Science"},{"key":"7_CR37","unstructured":"H. Tamaki and T. Sato. Unfold\/Fold Transformations of Logic Programs. In Sten\u00c5ke T\u00e4rnlund, editor, Proc. Second Int'l Conf. on Logic Programming, pages 127\u2013139, 1984."},{"key":"7_CR38","unstructured":"K. Verschaetse. Static termination analysis for definite Horn clause programs. PhD thesis, Dept. Computer Science, K. U. Leuven, 1992."},{"key":"7_CR39","unstructured":"K. Verschaetse and D. De Schreye. Deriving termination proofs for logic programs, using abstract procedures. In Proc. Eighth Int'l Conf. on Logic Programming, pages 301\u2013315, 1991."},{"key":"7_CR40","unstructured":"J. Zhang and P. W. Grant. An Automatic Difference-list Transformation Algorithm for Prolog. In Proceedings of the European Conference on Artificial Intelligence,ECAI'88, pages 320\u2013325. Pitman, 1988."}],"container-title":["Lecture Notes in Computer Science","Logic Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62718-9_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:14:12Z","timestamp":1605629652000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62718-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540627180","9783540684947"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/3-540-62718-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}