{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:36Z","timestamp":1761611076444,"version":"3.41.0"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[1999,10,1]],"date-time":"1999-10-01T00:00:00Z","timestamp":938736000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,10,1]],"date-time":"1999-10-01T00:00:00Z","timestamp":938736000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Automated Software Engineering"],"published-print":{"date-parts":[[1999,10]]},"DOI":"10.1023\/a:1008763422061","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T16:37:32Z","timestamp":1040575052000},"page":"329-356","source":"Crossref","is-referenced-by-count":12,"title":["Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm"],"prefix":"10.1007","volume":"6","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Smaill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian","family":"Green","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"237817_CR1","doi-asserted-by":"crossref","unstructured":"Basin, D. 1994. Logic frameworks for logic programs. In 4th International Workshop on Logic Program Synthesis and Transformation, (LOPSTR'94), number 883 in LNCS, Springer-Verlag.","DOI":"10.1007\/3-540-58792-6_1"},{"issue":"1\u20132","key":"237817_CR2","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00244462","volume":"16","author":"B. Basin","year":"1996","unstructured":"Basin, B. and Walsh, T. 1996. A calculus for and termination of rippling. Journal of Automated Reasoning, 16(1\u20132): 147-180.","journal-title":"Journal of Automated Reasoning"},{"key":"237817_CR3","unstructured":"Biundo, S. 1988. Automated synthesis of recursive algorithms as a theorem proving tool. In Y. Kodratoff, editor, Eighth European Conference on Artificial Intelligence, pp. 553-558, Pitman."},{"issue":"2","key":"237817_CR4","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BF00881856","volume":"14","author":"A. Bouhoula","year":"1995","unstructured":"Bouhoula, A. and Rusinowitch, M. 1995. Implicit induction in conditional theories. Journal of Automated Reasoning, 14(2):189-235.","journal-title":"Journal of Automated Reasoning"},{"key":"237817_CR5","unstructured":"Boyer, R.S. and Moore, J.S. A Computational Logic. ACM monograph series, Academic Press."},{"key":"237817_CR6","unstructured":"Bundy, A., Smaill, A., and Hesketh, J. 1990. Turning eureka steps into calculations in automatic program synthesis. In S.L.H. Clarke, editor, Proceedings of UK IT 90, pp. 221-226, IEE. Also available from Edinburgh as DAI Research Paper 448."},{"key":"237817_CR7","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/BF00249016","volume":"7","author":"A. Bundy","year":"1991","unstructured":"Bundy, A., van Harmelen, F., Hesketh J., and Smaill, A. 1991. Experiments with proof plans for induction. Journal of Automated Reasoning, 7:303-324. Earlier version available from Edinburgh as DAI Research Paper No 413.","journal-title":"Journal of Automated Reasoning"},{"key":"237817_CR8","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., and Smaill, A. 1993. Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62:185-253. Also available from Edinburgh as DAI Research Paper No. 567.","journal-title":"Artificial Intelligence"},{"key":"237817_CR9","volume-title":"Interactive Program Derivation","author":"M. Coen","year":"1992","unstructured":"Coen, M. 1992. Interactive Program Derivation. Ph.D. thesis, University of Cambridge, Cambridge, England."},{"key":"237817_CR10","unstructured":"Constable, R.L., Allen, S.F., Bromley, H.M. et al. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall."},{"key":"237817_CR11","first-page":"45","volume-title":"Formal Techniques in Artificial Intelligence: A Sourcebook","author":"R.L. Constable","year":"1990","unstructured":"Constable, R.L. and Howe, D.J. 1990. Implementing metamathematics as an approach to automatic theorem proving. In R.B. Banerji, editor, Formal Techniques in Artificial Intelligence: A Sourcebook, Amsterdam, North Holland, pp. 45-76."},{"key":"237817_CR12","series-title":"Formal Methods and Semantics","first-page":"200","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N. and Jouannaud, J.-P. 1990. Rewriting systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics. pp. 200-213, Elsevier: Amsterdam."},{"key":"237817_CR13","unstructured":"Dowek, G., Felty, A., Herbelin, H., Huet, G., Paulin, C., and Werner, B. 1991. The Coq proof assistant user's guide, version 5.6. Technical Report 134, INRIA."},{"key":"237817_CR14","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0743-1066(84)90020-7","volume":"1","author":"L.-H. Eriksson","year":"1984","unstructured":"Eriksson, L.-H. 1984. Synthesis of a unification algorithm in a logic programming calculus. Journal of Logic Programming, 1:3-18.","journal-title":"Journal of Logic Programming"},{"key":"237817_CR15","unstructured":"Gallagher, J.K. 1993. The Use of Proof Plans in Tactic Synthesis. Ph.D. thesis, University of Edinburgh."},{"key":"237817_CR16","doi-asserted-by":"crossref","unstructured":"Green, C. 1969. Application of theorem proving to problem solving. In IJCAI-69, pp. 219-239.","DOI":"10.21236\/ADA459656"},{"key":"237817_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Programming","author":"D. Gries","year":"1981","unstructured":"Gries, D. 1981. The Science of Programming. New York: Springer-Verlag."},{"key":"237817_CR18","unstructured":"Hanson, \u00c5. and T\u00e4rnlund, S.-A. 1979. A natural programming calculus. In Proc. 6th IJCAI, International Joint Conference on Artificial Intelligence, Tokyo, pp. 348-355."},{"key":"237817_CR19","unstructured":"Howard, W.A. 1980. 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, Academic Press, pp. 479-490."},{"key":"237817_CR20","unstructured":"IJCAI-69, Washington, D.C., USA, 1969."},{"issue":"1\u20132","key":"237817_CR21","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A. Ireland","year":"1996","unstructured":"Ireland, A. and Bundy, A. 1996. Productive use of failure in inductive proof. Journal of Automated Reasoning, 16(1\u20132):79-111. Also available as DAI Research Paper No 716, Dept. of Artificial Intelligence, Edinburgh.","journal-title":"Journal of Automated Reasoning"},{"key":"237817_CR22","doi-asserted-by":"crossref","unstructured":"Kraan, I., Basin, D., and Bundy, A. 1993. Logic program synthesis via proof planning. In K.K. Lau and T. Clement, editors, Logic Program Synthesis and Transformation. Springer-Verlag, pp. 1-14. Also available as Max-Planck-Institut f\u00fcr Informatik Report MPI-I-92-244 and Edinburgh DAI Research Report 603.","DOI":"10.1007\/978-1-4471-3560-9_1"},{"key":"237817_CR23","doi-asserted-by":"crossref","unstructured":"Lowe, H. 1994. Proof planning: A methodology for developing AI systems involving design. Artificial Intelligence for Engineering Design, Analysis and Manufacturing, 8(4). Special Issue on Research Methodology.","DOI":"10.1017\/S0890060400000986"},{"issue":"1","key":"237817_CR24","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Manna, Z. and Waldinger, R.J. 1980. A deductive approach to program synthesis. Journal of Transactions on Programming Languages and Systems, 2(1):90-121.","journal-title":"Journal of Transactions on Programming Languages and Systems"},{"key":"237817_CR25","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/0167-6423(81)90004-6","volume":"1","author":"Z. Manna","year":"1981","unstructured":"Manna, Z. and Waldinger, R.J. 1981. Deductive synthesis of the unification algorithm. Science of Computer Programming, 1:5-48.","journal-title":"Science of Computer Programming"},{"key":"237817_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0743-1066(89)90008-3","volume":"7","author":"D. Nardi","year":"1989","unstructured":"Nardi, D. 1989. Formal synthesis of a unification algorithm by the deductive-tableau method. Journal of Logic Programming, 7:1-43.","journal-title":"Journal of Logic Programming"},{"key":"237817_CR27","doi-asserted-by":"crossref","first-page":"605","DOI":"10.1007\/BF01941137","volume":"28","author":"B. Nordstr\u00f6m","year":"1988","unstructured":"Nordstr\u00f6m, B. 1988. Terminating general recursion. BIT, 28:605-619.","journal-title":"BIT"},{"key":"237817_CR28","unstructured":"Nordstr\u00f6m, K., Petersson B., and Smith, J. 1990. Programming in Martin-L\u00f6f Type Theory. Oxford University Press."},{"key":"237817_CR29","doi-asserted-by":"crossref","unstructured":"Paulin-Mohring, C. 1989. Extracting F\n\n                    \u03c9\n                  's programs from proofs in the calculus of constructions. ACM Proc. POPL.","DOI":"10.1145\/75277.75285"},{"key":"237817_CR30","unstructured":"Paulson, L.C. 1984. Verifying the unification algorithm in LCF. Report 50, Computer Laboratory, University of Cambridge."},{"key":"237817_CR31","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1016\/S0747-7171(86)80002-5","volume":"2","author":"L.C. Paulson","year":"1986","unstructured":"Paulson, L.C. 1986. Constructing recursion operators in intuitionistic type theory. Journal of Symbolic Computation, 2:325-355.","journal-title":"Journal of Symbolic Computation"},{"key":"237817_CR32","volume-title":"D\u00e9veloppement d'Algorithmes dans le Calcul des Constructions","author":"J. Rouyer","year":"1994","unstructured":"Rouyer, J. 1994. D\u00e9veloppement d'Algorithmes dans le Calcul des Constructions. Ph.D. thesis, Institut National Polytechnique de Lorraine, Nancy, France."},{"key":"237817_CR33","unstructured":"Saaman, E.H. and Malcolm, G.R. 1987. Well-founded recursion in type theory. Technical Report CS 8710, Department of Mathematics and Computing Science, University of Groningen."},{"key":"237817_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/BFb0105417","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96","author":"K. Slind","year":"1996","unstructured":"Slind, K. 1996. Function definition in higher-order logic. In Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, Vol. 1275 of Lecture Notes in Computer Science, pp. 381-399, Turku, Finland, Springer-Verlag."},{"key":"237817_CR35","doi-asserted-by":"crossref","unstructured":"Stickel, M., Waldinger, R., Lowry, M., Pressburger, T. and Underwood, I. 1994. Deductive composition of astronomical software from subroutine libraries. In Alan Bundy, editor, 12th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Nancy, France, Vol. 814, Springer-Verlag, pp. 341-355.","DOI":"10.1007\/3-540-58156-1_24"},{"key":"237817_CR36","unstructured":"Tyugu, E. 1991. Declarative programming in a type theory. In B. Moller, editor, Constructing Programs from Specifications, North-Holland, pp. 451-472."},{"key":"237817_CR37","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/BF00871707","volume":"1","author":"E. Tyugu","year":"1994","unstructured":"Tyugu, E. 1994. Using classes as specifications for automatic construction of programs in the NUT system. Automated Software Engineering, 1:315-334.","journal-title":"Automated Software Engineering"},{"key":"237817_CR38","unstructured":"Waldinger, R.J. and Lee, R.C. 1969. PROW: A step toward automatic program writing. In IJCAI-69, pp. 241-252."},{"key":"237817_CR39","first-page":"351","volume-title":"Proceedings of JICSLP-92","author":"G.A. Wiggins","year":"1992","unstructured":"Wiggins, G.A. 1992. Synthesis and transformation of logic programs in the Whelk proof development system. In K.R. Apt, editor, Proceedings of JICSLP-92, Cambridge, MA: MIT Press, pp. 351-358."},{"key":"237817_CR40","unstructured":"Yoshida, T., Bundy, A., Green, I., Walsh, T., and Basin, D. 1994. Coloured rippling: An extension of a theorem proving heuristic. In A.G. Cohn, editor, Proceedings of ECAI-94, John Wiley, pp. 85-89."},{"key":"237817_CR41","unstructured":"Zhang, H. 1992. Implementing contextual rewriting. In Micha\u00ebl Rusinowitch and Jean-Luc R\u00e9my, editors, Conditional Term Rewriting Systems. Third International Workshop, LNCS 656, Pont-\u00e1-Mousson, France, July 8\u201310, Springer-Verlag, pp. 363-377."}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008763422061.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008763422061\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008763422061.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:12:49Z","timestamp":1748070769000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008763422061"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,10]]},"references-count":41,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1999,10]]}},"alternative-id":["237817"],"URL":"https:\/\/doi.org\/10.1023\/a:1008763422061","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"type":"print","value":"0928-8910"},{"type":"electronic","value":"1573-7535"}],"subject":[],"published":{"date-parts":[[1999,10]]}}}