{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,7]],"date-time":"2023-02-07T16:17:07Z","timestamp":1675786627936},"publisher-location":"London","reference-count":19,"publisher":"Springer London","isbn-type":[{"value":"9783540198062","type":"print"},{"value":"9781447135609","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/978-1-4471-3560-9_1","type":"book-chapter","created":{"date-parts":[[2012,12,30]],"date-time":"2012-12-30T06:49:46Z","timestamp":1356850186000},"page":"1-14","source":"Crossref","is-referenced-by-count":19,"title":["Logic Program Synthesis via Proof Planning"],"prefix":"10.1007","author":[{"given":"Ina","family":"Kraan","sequence":"first","affiliation":[]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[]},{"given":"Alan","family":"Bundy","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"1_CR1","first-page":"113","volume":"7","author":"JL Bates","year":"1985","unstructured":"Joseph L. Bates and Robert L. Constable. Proofs as programs. ACM Transactions on Programming Languages and Systems, 7 (1): 113\u2013136, January 1985.","journal-title":"January"},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/0004-3702(80)90050-8","volume":"14","author":"W Bibel","year":"1980","unstructured":"W. Bibel. Syntax-directed, semantics-supported program synthesis. Artificial Intelligence, 14: 243\u2013261, 1980.","journal-title":"Artificial Intelligence"},{"key":"1_CR3","unstructured":"S. Biundo. Automated synthesis of recursive algo rithms as a theorem proving tool. In Y. Kodratoff, editor, Eighth European Conference on Artificial Intelligence, pages 553\u20138. Pitman, 1988."},{"key":"1_CR4","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Academic Press, 1988. Perspectives in Computing, Vol 23."},{"key":"1_CR5","first-page":"349","volume-title":"9th Conference on.Automated Deduction, pages 111-120","author":"A Bundy","year":"1988","unstructured":"A. Bundy. The use of explicit plans to guide inductive proofs. In R. Lusk and R. Overbeek, editors, 9th Conference on.Automated Deduction, pages 111\u2013120. Springer-Verlag, 1988. Longer version available from Edinburgh as DAI Research Paper No. 349."},{"key":"1_CR6","first-page":"419","volume-title":"Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, pages 359-365","author":"A Bundy","year":"1989","unstructured":"A. Bundy, F. van Harmelen, J. Hesketh, A. Smaill, and A. Stevens. A rational reconstruction and extension of recursion analysis. In N.S. Sridharan, editor, Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, pages 359\u2013365. Morgan Kauf-mann, 1989. Also available from Edinburgh as DAI Research Paper 419."},{"key":"1_CR7","unstructured":"Bundy et al 90a] A. Bundy, A. Smaill, and J. Hesketh. Turning eureka steps into calculations in automatic program synthesis. In S.L.H. Clarke, editor,Proceedings of UK IT 90,pages 221\u20136, 1990. Also available from Edinburgh as DAI Research Paper 448."},{"key":"1_CR8","first-page":"501","volume-title":"Computational Logic) pages 135-149","author":"A Bundy","year":"1990","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 Research Paper 501."},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 647\u2013648. Springer-Verlag, 1990. Lecture Notes in Artificial Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 507.","DOI":"10.1007\/3-540-52885-7_123"},{"key":"1_CR10","series-title":"Prentice Hall","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"RL Constable","year":"1986","unstructured":"R.L. Constable, S.F. Allen, H.M. Bromley, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986."},{"key":"1_CR11","volume-title":"Addision-wesley","author":"Y Deville","year":"1990","unstructured":"Y. Deville. Logic Programming. Systematic Program Development. International Series in Logic Programming. Addision-Wesley, 1990."},{"key":"1_CR12","first-page":"685","volume-title":"Proceedings of Eighth International Conference on Logic Programming","author":"L Fribourg","year":"1990","unstructured":"L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In Proceedings of Eighth International Conference on Logic Programming, pages 685\u2013699. MIT Press, June 1990."},{"key":"1_CR13","volume-title":"Revised in","author":"P Hill","year":"1991","unstructured":"P. Hill and J. Lloyd. The Godei Report. Technical Report TR-91\u201302, Department of Computer Science,University of Bristol, March 1991. Revised in September 1991."},{"issue":"2","key":"1_CR14","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1145\/322248.322258","volume":"28","author":"CJ Hogger","year":"1981","unstructured":"C.J. Hogger. Derivation of logic programs. J ACM, 28 (2): 372\u2013392, April 1981.","journal-title":"J Acm"},{"key":"1_CR15","volume-title":"J.p. Seldin and J.R. Hindley, editors, To H.B. Curry; Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479-490. Academic Press","author":"WA Howard","year":"1980","unstructured":"W.A. Howard. The formulae-as-types notion of construction. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry; Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479\u2013490. Academic Press, 1980."},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Per Martin-Lof. Constructive mathematics and computer programming. In 6th International Congress for Logic, Methodology and Philosophy of Science, pages 153\u2013175, Hanover, August 1979. Published by North Holland, Amsterdam. 1982.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"1_CR17","unstructured":"Wiggins 92]"},{"key":"1_CR18","volume-title":"K. R. Apt, editor, Proceedings of JICSLP-92","author":"GA Wiggins","year":"1992","unstructured":"G. A. Wiggins. Synthesis and transformation of logic programs in the Whelk proof development system. In K. R. Apt, editor, Proceedings of JICSLP-92, 1992."},{"key":"1_CR19","first-page":"27","volume-title":"Proceedings of Lopstr-91","author":"GA Wiggins","year":"1991","unstructured":"G. A. Wiggins, A. Bundy, H. C. Kraan, and J. Hes-keth. Synthesis and transformation of logic programs through constructive, inductive proof. In K-K. Lau and T. Clement, editors, Proceedings of LoPSTr-91, pages 27\u201345. Springer Verlag, 1991. Workshops in Computing Series."}],"container-title":["Logic Program Synthesis and Transformation","Workshops in Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4471-3560-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,10]],"date-time":"2019-05-10T03:07:02Z","timestamp":1557457622000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-4471-3560-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540198062","9781447135609"],"references-count":19,"URL":"http:\/\/dx.doi.org\/10.1007\/978-1-4471-3560-9_1","relation":{},"ISSN":["1431-1682"],"issn-type":[{"value":"1431-1682","type":"print"}],"published":{"date-parts":[[1993]]}}}