{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:20:40Z","timestamp":1725484840200},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677970"},{"type":"electronic","value":"9783540449577"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44957-4_41","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T05:24:41Z","timestamp":1180675481000},"page":"613-628","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Perfect Model Checking via Unfold\/Fold Transformations"],"prefix":"10.1007","author":[{"given":"Alberto","family":"Pettorossi","sequence":"first","affiliation":[]},{"given":"Maurizio","family":"Proietti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,12,15]]},"reference":[{"issue":"20","key":"41_CR1","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1016\/0743-1066(94)90024-8","volume":"19","author":"K. R. Apt","year":"1994","unstructured":"K. R. Apt and R. N. Bol. Logic programming and negation: A survey. Journal of Logic Programming, 19,20:9\u201371, 1994.","journal-title":"Journal of Logic Programming"},{"key":"41_CR2","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic. Academic Press, New York, 1979."},{"key":"41_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0743-1066(98)10030-4","volume":"40","author":"S. Brass","year":"1999","unstructured":"S. Brass and J. Dix. Semantics of (disjunctive) logic programs based on partial evaluation. Journal of Logic Programming, 40:1\u201346, 1999.","journal-title":"Journal of Logic Programming"},{"issue":"1","key":"41_CR4","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"R. M. Burstall","year":"1977","unstructured":"R. M. Burstall and J. Darlington. A transformation system for developing recursive programs. JACM, 24(1):44\u201367, January 1977.","journal-title":"JACM"},{"key":"41_CR5","doi-asserted-by":"crossref","unstructured":"W. Chen and D. S. Warren. Tabled evaluation with delaying for general logic programs. JACM, 43(1), 1996.","DOI":"10.1145\/227595.227597"},{"key":"41_CR6","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-1-4684-3384-5_11","volume-title":"Logic and Data Bases","author":"K. L. Clark","year":"1978","unstructured":"K. L. Clark. Negation as failure. In H. Gallaire and J. Minker (eds.) Logic and Data Bases, 293\u2013322. Plenum Press, New York, 1978."},{"key":"41_CR7","unstructured":"H. Comon and R. Nieuwenhuis. Induction = I-axiomatization + first-order consistency. Information and Computation. (To appear)."},{"key":"41_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(86)90050-2","volume":"42","author":"B. Courcelle","year":"1986","unstructured":"B. Courcelle. Equivalences and Transformations of Regular Systems-Applications to Recursive Program Schemes and Grammars. Theo. Comp. Sci., 42:1\u2013122, 1986.","journal-title":"Theo. Comp. Sci."},{"key":"41_CR9","doi-asserted-by":"crossref","unstructured":"E. A. Emerson. Temporal and modal logic. In J. van Leuveen (ed.) Handbook of Theoretical Computer Science, volume B, 997\u20131072. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"41_CR10","volume-title":"DAIMI FN-10","author":"J. Engelfriet","year":"1975","unstructured":"J. Engelfriet. Tree Automata and Tree Grammars. DAIMI FN-10, Department of Computer Science, University of Aarhus, Denmark, April 1975."},{"key":"41_CR11","unstructured":"L. Kott. Unfold\/fold program transformation. In M. Nivat and J.C. Reynolds (eds.) Algebraic Methods in Semantics, 411\u2013434. Cambridge University Press, 1985."},{"key":"41_CR12","doi-asserted-by":"crossref","unstructured":"J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1987. 2nd Ed.","DOI":"10.1007\/978-3-642-83189-8"},{"issue":"2&3","key":"41_CR13","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/S0743-1066(99)00029-1","volume":"41","author":"A. Pettorossi","year":"1999","unstructured":"A. Pettorossi and M. Proietti. Synthesis and transformation of logic programs using unfold\/fold proofs. Journal of Logic Programming, 41(2&3):197\u2013230, 1999.","journal-title":"Journal of Logic Programming"},{"issue":"1","key":"41_CR14","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/0304-3975(94)00227-A","volume":"142","author":"M. Proietti","year":"1995","unstructured":"M. Proietti and A. Pettorossi. Unfolding-definition-folding, in this order, for avoiding unnecessary variables in logic programs. Theo. Comp. Sci., 142(1):89\u2013124, 1995.","journal-title":"Theo. Comp. Sci."},{"key":"41_CR15","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF00243002","volume":"5","author":"T. C. Przymusinski","year":"1989","unstructured":"T. C. Przymusinski. On the declarative and procedural semantics of logic programs. Journal of Automated Reasoning, 5:167\u2013205, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"41_CR16","first-page":"1","volume":"141","author":"M. O. Rabin","year":"1969","unstructured":"M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1\u201334, July 1969.","journal-title":"Transactions of the American Mathematical Society"},{"key":"41_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-46419-0_13","volume-title":"Proc. TACAS 2000","author":"A. Roychoudhury","year":"2000","unstructured":"A. Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan, I.V. Ramakrishnan, and S. A. Smolka. Verification of parametrized systems using logic program transformations. In Proc. TACAS 2000, LNCS 1785, 172\u2013187. Springer, 2000."},{"key":"41_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/3-540-63166-6_16","volume-title":"Proc. CAV\u2019 97","author":"Y.S. Ramakrishna","year":"1997","unstructured":"Y.S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In Proc. CAV\u2019 97, LNCS 1254, 143\u2013154. Springer, 1997."},{"key":"41_CR19","doi-asserted-by":"publisher","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. Theo. Comp. Sci., 86:107\u2013139, 1991.","journal-title":"Theo. Comp. Sci."},{"key":"41_CR20","first-page":"127","volume-title":"Proceedings of ICLP\u201984","author":"H. Tamaki","year":"1984","unstructured":"H. Tamaki and T. Sato. Unfold\/fold transformation of logic programs. In Proceedings of ICLP\u201984, 127\u2013138. Uppsala University, Sweden, 1984."}],"container-title":["Lecture Notes in Computer Science","Computational Logic \u2014 CL 2000"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44957-4_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:30:25Z","timestamp":1558272625000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44957-4_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677970","9783540449577"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-44957-4_41","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"15 December 2000","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}