{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T04:20:26Z","timestamp":1648959626109},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540587927","type":"print"},{"value":"9783540491040","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58792-6_1","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:44:35Z","timestamp":1330274675000},"page":"1-16","source":"Crossref","is-referenced-by-count":1,"title":["Logic frameworks for logic programs"],"prefix":"10.1007","author":[{"given":"David A.","family":"Basin","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"1_CR1","unstructured":"David Basin. Isawhelk: Whelk interpreted in Isabelle. Abstract accepted at the 11th International Conference on Logic Programming (ICLP94). Full version available via anonymous ftp to mpi-sb.mpg.de in pub\/papers\/conferences\/Basin-ICLP94.dvi.Z."},{"key":"1_CR2","volume-title":"7th International Workshop on Software Specification and Design","author":"D. Basin","year":"1993","unstructured":"David Basin, Alan Bundy, Ina Kraan, and Sean Matthews. A framework for program development based on schematic proof. In 7th International Workshop on Software Specification and Design, Los Angeles, December 1993. IEEE Computer Society Press."},{"key":"1_CR3","unstructured":"David Basin and Robert Constable. Metalogical frameworks. In G\u00e9rard Huet and Gordon Plotkin, editors, Logical Environments, pages 1\u201329. Cambridge University Press, 1993."},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"David Basin and Sean Matthews. A conservative extension of first order logic and its applications to theorem proving. In 13th Conference of the Foundations of Software Technology and Theoretical Computer Science, pages 151\u2013160, December 1993.","DOI":"10.1007\/3-540-57529-4_50"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"A. Bundy. Tutorial notes; reasoning about logic programs. In G. Comyn, N.E. Fuchs, and M.J. Ratcliffe, editors, Logic programming in action, pages 252\u2013277. Springer Verlag, 1992.","DOI":"10.1007\/3-540-55930-2_18"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"A. Bundy, A. Smaill, and G. A. Wiggins. The synthesis of logic programs from inductive proofs. In J. Lloyd, editor, Computational Logic, pages 135\u2013149. Springer-Verlag, 1990. Esprit Basic Research Series. Also available from Edinburgh as DAI Re search Paper 501.","DOI":"10.1007\/978-3-642-76274-1_8"},{"issue":"1","key":"1_CR7","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. Journal of the Association for Computing Machinery, 24(1):44\u201367, 1977.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"1_CR8","unstructured":"Wei Ngan Chin. Automatic Methods for Program Transformation. Ph. D. thesis, Imperial College Department of Computer Science, March 1990."},{"key":"1_CR9","unstructured":"K. L. Clark and S-\u00e5. T\u00c4rnlund. A first order theory of data and programs. In B. Gilchrist, editor, Information Processing, pages 939\u2013944. IFIP, 1977."},{"key":"1_CR10","unstructured":"K.L. Clark. Predicate logic as a computational formalism. Technical Report TOC 79\/59, Imperial College, 1979."},{"key":"1_CR11","unstructured":"K.L. Clark and S. Sickel. Predicate Logic: a calculus for deriving programs. In R. Reddy, editor, Proceedings of IJCAI-77, pages 419\u2013420. IJCAI, 1977."},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Pierre Flener and Yves Deville. Towards stepwise, schema-guided synthesis of logic programs. In T. Clement and K.-K. Lau, editors, Logic Program Synthesis and Transformation, pages 46\u201364. Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4471-3494-7_4"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Michael J. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Cordell Green. Application of theorem proving to problem solving. In Proceedings of the IJCAI-69, pages 219\u2013239, 1969.","DOI":"10.21236\/ADA459656"},{"issue":"1","key":"1_CR15","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143\u2013184, January 1993.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"1_CR16","unstructured":"P. Hill and J. Lloyd. The G\u00f6del Report. Technical Report TR-91-02, Department of Computer Science, University of Bristol, March 1991. Revised in September 1991."},{"issue":"2","key":"1_CR17","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1145\/322248.322258","volume":"28","author":"C.J. Hogger","year":"1981","unstructured":"C.J. Hogger. Derivation of logic programs. JACM, 28(2):372\u2013392, April 1981.","journal-title":"JACM"},{"key":"1_CR18","unstructured":"L. Kott. About a transformation system: A theoretical study. In Proceedings of the 3rd International Symposium on Programming, pages 232\u2013247, Paris, 1978."},{"key":"1_CR19","unstructured":"Robert A. Kowalski. Predicate logic as a programming language. In IFIP-74. North-Holland, 1974."},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Ina Kraan, David Basin, and Alan Bundy. Logic program synthesis via proof planning. In Proceedings of LoPSTr-92. Springer Verlag, 1992.","DOI":"10.1007\/978-1-4471-3560-9_1"},{"key":"1_CR21","unstructured":"Ina Kraan, David Basin, and Alan Bundy. Middle-out reasoning for logic program synthesis. In 10th International Conference on Logic Programming (ICLP93), pages 441\u2013455, Budapest Hungary, 1993."},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"M.J. Maher. Equivalences of logic programs. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming. Morgan Kaufmann, 1987.","DOI":"10.1016\/B978-0-934613-40-8.50020-8"},{"key":"1_CR23","unstructured":"Sean Matthews, Alan Smaill, and David Basin. Experience with FS 0 as a framework theory. In G\u00e9rard Huet and Gordon Plotkin, editors, Logical Environments, pages 61\u201382. Cambridge University Press, 1993."},{"key":"1_CR24","unstructured":"Lawrence C. Paulson. Set theory for verification: I. From foundations to functions. Journal of Automated Reasoning. In press; draft available as Report 271, University of Cambridge Computer Laboratory."},{"key":"1_CR25","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L. C. Paulson","year":"1989","unstructured":"Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363\u2013397, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR26","volume-title":"Technical Report 280","author":"L. C. Paulson","year":"1993","unstructured":"Lawrence C. Paulson. Introduction to Isabelle. Technical Report 280, Cambridge University Computer Laboratory, Cambridge, January 1993."},{"key":"1_CR27","volume-title":"Technical Report 286","author":"L. C. Paulson","year":"1993","unstructured":"Lawrence C. Paulson. Isabelle's object-logics. Technical Report 286, Cambridge University Computer Laboratory, Cambridge, February 1993."},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Logic programming in the LF logical framework. In Logical Frameworks, pages 149\u2013181. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.008"},{"key":"1_CR29","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0304-3975(92)90287-P","volume":"105","author":"T. Sato","year":"1992","unstructured":"Taisuke Sato. Equivalence-preserving first-order unfold\/fold transformation systems. Theoretical Computer Science, 105:57\u201384, 1992.","journal-title":"Theoretical Computer Science"},{"key":"1_CR30","unstructured":"H. Tamaki and T. Sato. Unfold\/fold transformations of logic programs. In Proceedings of 2nd ICLP, 1984."},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Mattias Waldau. Formal validation of transformation schemata. In T. Clement and K.-K. Lau, editors, Logic Program Synthesis and Transformation, pages 97\u2013110. Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4471-3494-7_8"},{"key":"1_CR32","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/0004-3702(80)90015-6","volume":"13","author":"R. W. Weyhrauch","year":"1980","unstructured":"Richard W. Weyhrauch. Prolegomena to a theory of formal reasoning. Artificial Intelligence, 13:133\u2013170, 1980.","journal-title":"Artificial Intelligence"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Geraint A. Wiggins. Synthesis and transformation of logic programs in the Whelk proof development system. In K. R. Apt, editor, Proceedings of JICSLP-92, 1992.","DOI":"10.1007\/978-1-4471-3494-7_3"}],"container-title":["Logic Program Synthesis and Transformation \u2014 Meta-Programming in Logic","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58792-6_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:24:06Z","timestamp":1605648246000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58792-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540587927","9783540491040"],"references-count":33,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-58792-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1994]]}}}