{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:45Z","timestamp":1749182805953,"version":"3.41.0"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1998,10,1]],"date-time":"1998-10-01T00:00:00Z","timestamp":907200000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,10,1]],"date-time":"1998-10-01T00:00:00Z","timestamp":907200000000},"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":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1998,10]]},"DOI":"10.1023\/a:1005903504159","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T00:10:48Z","timestamp":1040515848000},"page":"233-275","source":"Crossref","is-referenced-by-count":0,"title":["Automated Synthesis of Recursive Programs from a \u2200\u2203 Logical Specification"],"prefix":"10.1007","volume":"21","author":[{"given":"Jacques","family":"Chazarain","sequence":"first","affiliation":[]},{"given":"Serge","family":"Muller","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"158834_CR1","doi-asserted-by":"crossref","unstructured":"Bachmair, L.: Proof by consistency in equational theories, in 3rd Symposium on Logic in Computer Science, IEEE, Edinburgh (UK), 1988, pp. 228\u2013233.","DOI":"10.1109\/LICS.1988.5122"},{"key":"158834_CR2","unstructured":"Barras, B., Boutin, S., Cornes, C., Courant, J., Filli\u00e2tre, J.-C., Gim\u00e9nez, E., Herbelin, H., Huet, G., Mu\u00f1oz, C., Murthy, C., Parent, C., Paulin-Mohring, C., Sa\u00efbi, A., and Werner, B.: The Coq proof assistant, reference manual: Version 6.1, Technical Report RT-0203, INRIA, 1996."},{"key":"158834_CR3","unstructured":"Bellegarde, F.: Automating synthesis by completion, in C. Queinnec, V. Viguie Donzeau-Gouge, and P. Weiss (eds), Journ\u00e9es Francophones des Langages Applicatifs, Vol. 13 of Collection didactique, INRIA, January 1995, pp. 177\u2013202."},{"key":"158834_CR4","first-page":"287","volume-title":"Advances in Artificial Intelligence","author":"S. Biundo","year":"1987","unstructured":"Biundo, S.: A synthesis system mechanizing proofs by induction, in B. Du Boulay, D. Hogg, and L. Steels (eds), Advances in Artificial Intelligence, Vol. 2, Elsevier Science Publishers B.V. (North-Holland), 1987, pp. 287\u2013296."},{"key":"158834_CR5","unstructured":"Biundo, S.: Automated synthesis of recursive algorithms as a theorem proving tool, in Y. Kodratoff (ed.), 8th European Conference on Artificial Intelligence, Munich (Germany), August 1988, pp. 553\u2013558."},{"key":"158834_CR6","unstructured":"Bouhoula, A.: Preuves automatiques par r\u00e9currence dans les th\u00e9ories conditionnelles, Ph.D. thesis, Universit\u00e9 de Nancy I, March 1994."},{"issue":"5","key":"158834_CR7","doi-asserted-by":"crossref","first-page":"631","DOI":"10.1093\/logcom\/5.5.631","volume":"5","author":"A. Bouhoula","year":"1995","unstructured":"Bouhoula, A., Kounalis, E., and Rusinowitch, M.: Automated mathematical induction, Journal of Logic and Computation\n5(5) (1995), 631\u2013668.","journal-title":"Journal of Logic and Computation"},{"key":"158834_CR8","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BF00881856","volume":"14","author":"A. Bouhoula","year":"1995","unstructured":"Bouhoula, A. and Rusinowitch, M.: Implicit induction in conditional theories, Journal of Automated Reasoning\n14 (1995), 189\u2013235.","journal-title":"Journal of Automated Reasoning"},{"key":"158834_CR9","volume-title":"A Computational Logic","author":"R. Boyer","year":"1979","unstructured":"Boyer, R. and Moore, J.: A Computational Logic, Academic Press, New York (USA), 1979."},{"key":"158834_CR10","doi-asserted-by":"crossref","unstructured":"Bundy, A., Smaill, A., and Wiggins, G.: The synthesis of logic programs from inductive proofs, in J. Lloyd (ed.), Symposium on Computational Logic, Esprit Basic Research Series, Springer-Verlag, 1990, pp. 135\u2013149.","DOI":"10.1007\/978-3-642-76274-1_8"},{"key":"158834_CR11","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, S., van Harmelen, F., Ireland, A., and Smaill, A.: Rippling: A heuristic for guiding inductive proofs, Artificial Intelligence\n62 (1993), 185\u2013253.","journal-title":"Artificial Intelligence"},{"key":"158834_CR12","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1007\/3-540-52885-7_123","volume-title":"10th Conference on Automated Deduction","author":"A. Bundy","year":"1990","unstructured":"Bundy, A., van Harmelen, F., Horn, C., and Smaill, A.: The Oyster-Clam system, in M. E. Stickel (ed.), 10th Conference on Automated Deduction, LNCS 449, Springer-Verlag, Kaiserslautern (Germany), July 1990, pp. 647\u2013648."},{"issue":"1","key":"158834_CR13","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1093\/comjnl\/12.1.41","volume":"12","author":"R. Burstall","year":"1969","unstructured":"Burstall, R.: Proving properties of programs by structural induction, Computer Journal\n12(1) (1969), 41\u201348.","journal-title":"Computer Journal"},{"issue":"1","key":"158834_CR14","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"R. Burstall","year":"1977","unstructured":"Burstall, R. and Darlington, J.: A transformation system for developing recursive programs, Journal of the ACM\n24(1) (1977), 44\u201367.","journal-title":"Journal of the ACM"},{"key":"158834_CR15","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/3-540-58156-1_9","volume-title":"12th Conference on Automated Deduction","author":"J. Chazarain","year":"1994","unstructured":"Chazarain, J. and Kounalis, E.: Mechanizable inductive proofs for a classs of \u2200 \u2203 formulas, in A. Bundy (ed.), 12th Conference on Automated Deduction, LNCS 814, Springer-Verlag, Nancy (France), 1994, pp. 118\u2013132."},{"key":"158834_CR16","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1007\/3-540-59200-8_76","volume-title":"6th International Conference on Rewriting Techniques and Applications, RTA-95","author":"J. Chazarain","year":"1995","unstructured":"Chazarain, J. and Muller, S.: Lemma: A system for automated synthesis of recursive programs in equational theories, in J. Hsiang (ed.), 6th International Conference on Rewriting Techniques and Applications, RTA-95, LNCS 914, Springer-Verlag, Kaiserslautern (Germany), April 1995, pp. 420\u2013425."},{"key":"158834_CR17","unstructured":"Constable, R. L., Allen, S. F., Bromley, H. M., Cleaveland, W., Cremer, J., Harper, R., Howe, D., Knoblock, T., Mendler, N. P., Panangaden, P., Sasaki, J., and Smith, S.: Implementing Mathematics with the NuPrl Proof Development System, Prentice Hall, 1986."},{"issue":"1","key":"158834_CR18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(81)90014-X","volume":"16","author":"J. Darlington","year":"1981","unstructured":"Darlington, J.: An experimental program transformation and synthesis system, Artificial Intelligence\n16(1) (1981), 1\u201346.","journal-title":"Artificial Intelligence"},{"issue":"2\u20133","key":"158834_CR19","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1016\/S0019-9958(85)80003-6","volume":"65","author":"N. Dershowitz","year":"1985","unstructured":"Dershowitz, N.: Computing with rewrite systems, Information and Control\n65(2\u20133) (1985), 122\u2013157.","journal-title":"Information and Control"},{"key":"158834_CR20","first-page":"208","volume":"1","author":"N. Dershowitz","year":"1985","unstructured":"Dershowitz, N.: Synthesis by completion, in 9th International Joint Conference on Artificial Intelligence, Vol. 1, Los Angeles (USA), 1985, pp. 208\u2013214.","journal-title":"9th International Joint Conference on Artificial Intelligence"},{"issue":"1\u20132","key":"158834_CR21","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N.: Termination of rewriting, Journal of Symbolic Computation\n3(1\u20132) (1987), 69\u2013116.","journal-title":"Journal of Symbolic Computation"},{"issue":"8","key":"158834_CR22","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N. and Manna, Z.: Proving termination with multiset orderings, Communications of the ACM\n22(8) (1979), 465\u2013476.","journal-title":"Communications of the ACM"},{"key":"158834_CR23","first-page":"234","volume-title":"8th National Conference on Artificial Intelligence (AAAI-90)","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N. and Pinchover, E.: Inductive synthesis of equational programs, in 8th National Conference on Artificial Intelligence (AAAI-90), MIT Press, Boston (USA), 1990, pp. 234\u2013239."},{"key":"158834_CR24","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1016\/S0747-7171(06)80002-7","volume":"15","author":"N. Dershowitz","year":"1993","unstructured":"Dershowitz, N. and Reddy, U.: Deductive and inductive synthesis of equational programs, Journal of Symbolic Computation\n15 (1993), 467\u2013494.","journal-title":"Journal of Symbolic Computation"},{"issue":"3","key":"158834_CR25","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/S0747-7171(89)80069-0","volume":"8","author":"L. Fribourg","year":"1989","unstructured":"Fribourg, L.: A strong restriction of the inductive completion procedure, Journal of Symbolic Computation\n8(3) (1989), 253\u2013276.","journal-title":"Journal of Symbolic Computation"},{"key":"158834_CR26","unstructured":"Fribourg, L.: Extracting logic programs from proofs that use extended Prolog execution and induction, in J.-M. Jacquet (ed.), Constructing Logic Programs, Chapter 2, Wiley, 1993, pp. 39\u201366."},{"key":"158834_CR27","first-page":"219","volume-title":"15th Symposium on Principles of Programming Languages","author":"M. Garland","year":"1988","unstructured":"Garland, M. and Guttag, J.: Inductive methods for reasoning about abstract data types, in 15th Symposium on Principles of Programming Languages, ACM, San Diego (USA), 1988, pp. 219\u2013228."},{"key":"158834_CR28","doi-asserted-by":"crossref","unstructured":"Green, C. C.: Application of theorem-proving to problem solving, in 1st International Joint Conference on Artificial Intelligence, Washington, DC (USA), May 1969, pp. 219\u2013239.","DOI":"10.21236\/ADA459656"},{"key":"158834_CR29","series-title":"LNCS","first-page":"310","volume-title":"11th Conference on Automated Deduction","author":"J. Hesketh","year":"1992","unstructured":"Hesketh, J., Bundy, A., and Smaill, A.: Using middle-out reasoning to control the synthesis of tail-recursive programs, in D. Kapur (ed.), 11th Conference on Automated Deduction, LNCS 607, Springer-Verlag, Saratoga Springs, NY, June 1992, pp. 310\u2013324."},{"issue":"2","key":"158834_CR30","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1145\/322248.322258","volume":"28","author":"C. J. Hogger","year":"1981","unstructured":"Hogger, C. J.: Derivation of logic programs, Journal of the ACM\n28(2) (1981), 372\u2013392.","journal-title":"Journal of the ACM"},{"issue":"2","key":"158834_CR31","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"G. Huet","year":"1982","unstructured":"Huet, G. and Hullot, J.-M.: Proofs by induction in equational theories with constructors, Journal of Computer and System Sciences\n25(2) (1982), 239\u2013266.","journal-title":"Journal of Computer and System Sciences"},{"key":"158834_CR32","unstructured":"Hullot, J.-M.: Compilation de formes canoniques dans des th\u00e9ories \u00e9quationnelles, Ph.D. thesis, Universit\u00e9 Paris-Sud, November 1980."},{"key":"158834_CR33","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.-P. and Kounalis, E.: Proofs by induction in equational theories without constructors, in 1st Symposium on Logic in Computer Science, IEEE, June 1986, pp. 358\u2013366. Full paper in Information and Computation 82 (1989).","DOI":"10.1016\/0890-5401(89)90062-X"},{"key":"158834_CR34","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/3-540-16780-3_83","volume-title":"8th Conference on Automated Deduction","author":"D. Kapur","year":"1986","unstructured":"Kapur, D., Narendran, P., and Zhang, H.: Proof by induction using test sets, in J. H. Siekmann (ed.), 8th Conference on Automated Deduction, LNCS 230, Springer-Verlag, Oxford (UK), July 1986, pp. 99\u2013117."},{"key":"158834_CR35","unstructured":"Kounalis, E.: A simplification-based approach to program synthesis, in 10th European Conference on Artificial Intelligence (ECAI 92), Vienna (Austria), August 1992, pp. 82\u201386."},{"key":"158834_CR36","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0304-3975(92)90279-O","volume":"106","author":"E. Kounalis","year":"1992","unstructured":"Kounalis, E.: Testing for the ground (co)-reducibility property in term rewriting systems, Theoretical Computer Science\n106 (1992), 87\u2013117.","journal-title":"Theoretical Computer Science"},{"key":"158834_CR37","first-page":"216","volume":"41","author":"E. Kounalis","year":"1990","unstructured":"Kounalis, E. and Rusinowitch, M.: Mechanizing inductive reasoning, Bulletin of the European Association for Theoretical Computer Science\n41 (1990), 216\u2013226.","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"158834_CR38","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/BF00244461","volume":"16","author":"I. Kraan","year":"1996","unstructured":"Kraan, I., Basin, D., and Bundy, A.: Middle-out reasoning for synthesis and induction, Journal of Automated Reasoning\n16 (1996), 113\u2013145.","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"158834_CR39","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.: A deductive approach to program synthesis, ACM Transactions on Programming Languages and Systems\n2(1) (1980), 90\u2013121.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"8","key":"158834_CR40","doi-asserted-by":"crossref","first-page":"674","DOI":"10.1109\/32.153379","volume":"18","author":"Z. Manna","year":"1992","unstructured":"Manna, Z. and Waldinger, R.: Fundamentals of deductive program synthesis, IEEE Transactions on Software Engineering\n18(8) (1992), 674\u2013704.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"158834_CR41","doi-asserted-by":"crossref","unstructured":"Musser, D.: On proving inductive properties of abstract data types, in 7th Symposium on Principles of Programming Languages, Las Vegas (USA), Association for Computing Machinery, 1980, pp. 154\u2013162.","DOI":"10.1145\/567446.567461"},{"key":"158834_CR42","doi-asserted-by":"crossref","unstructured":"Padawitz, P.: Computing in Horn Clause Theories, EATCS Monographs on Theoretical Computer Science 16, Springer-Verlag, 1988.","DOI":"10.1007\/978-3-642-73824-1"},{"key":"158834_CR43","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1007\/3-540-51081-8_121","volume-title":"3rd International Conference on Rewriting Techniques and Applications","author":"U. Reddy","year":"1989","unstructured":"Reddy, U.: Rewriting techniques for program synthesis, in N. Dershowitz (ed.), 3rd International Conference on Rewriting Techniques and Applications, LNCS 355, Springer-Verlag, Chapel Hill (USA), 1989, pp. 388\u2013403."},{"key":"158834_CR44","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/3-540-52885-7_86","volume-title":"10th Conference on Automated Deduction","author":"U. Reddy","year":"1990","unstructured":"Reddy, U.: Term rewriting induction, in M. E. Stickel (ed.), 10th Conference on Automated Deduction, LNCS 449, Springer-Verlag, Kaiserslautern (Germany), July 1990, pp. 162\u2013177."},{"key":"158834_CR45","series-title":"LNCS","volume-title":"6th Conference on Automated Deduction","author":"D. Smith","year":"1982","unstructured":"Smith, D.: Derived preconditions and their use in program synthesis, in D. W. Loveland (ed.), 6th Conference on Automated Deduction, LNCS 138, Springer-Verlag, New York (USA), 1982."},{"key":"158834_CR46","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1016\/S0747-7171(89)80040-9","volume":"7","author":"J. Traugott","year":"1989","unstructured":"Traugott, J.: Deductive synthesis of sorting programs, Journal of Symbolic Computation\n7 (1989), 533\u2013572.","journal-title":"Journal of Symbolic Computation"},{"key":"158834_CR47","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"602","DOI":"10.1007\/BFb0012861","volume-title":"9th Conference on Automated Deduction","author":"C. Walther","year":"1988","unstructured":"Walther, C.: Argument-bounded algorithms as a basis for automated termination proofs, in E. Lusk and R. Overbeek (eds), 9th Conference on Automated Deduction, LNCS 310, Springer-Verlag, Argonne (USA), May 1988, pp. 602\u2013621."},{"key":"158834_CR48","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/BFb0012831","volume-title":"9th Conference on Automated Deduction","author":"H. Zhang","year":"1988","unstructured":"Zhang, H., Kapur, D., and Krishnamoorthy, M. S.: A mechanizable induction principle for equational specifications, in E. Lusk and R. Overbeek (eds), 9th Conference on Automated Deduction, LNCS 310, Springer-Verlag, Argonne (USA), May 1988, pp. 162\u2013181."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005903504159.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005903504159\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005903504159.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:25:51Z","timestamp":1749122751000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005903504159"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,10]]},"references-count":48,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1998,10]]}},"alternative-id":["158834"],"URL":"https:\/\/doi.org\/10.1023\/a:1005903504159","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1998,10]]}}}