{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,25]],"date-time":"2025-05-25T04:03:24Z","timestamp":1748145804047,"version":"3.41.0"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"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":[[2003,7]]},"DOI":"10.1023\/a:1024448931103","type":"journal-article","created":{"date-parts":[[2003,9,15]],"date-time":"2003-09-15T17:22:37Z","timestamp":1063646557000},"page":"247-269","source":"Crossref","is-referenced-by-count":2,"title":["Predicate Synthesis for Correcting Faulty Conjectures: The Proof Planning Paradigm"],"prefix":"10.1007","volume":"10","author":[{"given":"Ra\u00fal","family":"Monroy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5127976_CR1","doi-asserted-by":"crossref","unstructured":"Armando, A., Smaill, A., and Green, I. 1997. Automatic synthesis of recursive programs: The proof-planning paradigm. In M. Lowry and Y. Ledru, editors, Proceedings of the 12th Conference on Automated Software Engineering. Nevada, USA, Lake Tahoe, pp. 2\u20139.","DOI":"10.1109\/ASE.1997.632818"},{"key":"5127976_CR2","unstructured":"Bird, R. 1998. Introduction to Functional Programming Using Haskell, 2nd edn. Prentice Hall Europe."},{"key":"5127976_CR3","unstructured":"Boyer, R.S. and Moore, J.S. 1979. A Computational Logic. Academic Press. ACM Monograph Series."},{"issue":"11","key":"5127976_CR4","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1145\/219717.219771","volume":"38","author":"I. Bratko","year":"1995","unstructured":"GROUP\/Papers\/cacm.ps.gz.","journal-title":"Communications of the ACM"},{"key":"5127976_CR5","series-title":"Edinburgh as DAI Research Paper","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/BFb0012826","volume-title":"Proceedings of the 9th Conference on Automated Deduction","author":"A. Bundy","year":"1988","unstructured":"Bundy, A. 1988. The use of explicit plans to guide inductive proofs. In R. Lusk and R. Overbeek, editors, Proceedings of the 9th Conference on Automated Deduction. Illinois, USA: Argonne, pp. 111\u2013120, Springer-Verlag. Also available from Edinburgh as DAI Research PaperNo. 349."},{"key":"5127976_CR6","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/BF00120880","volume":"20","author":"A. Bundy","year":"1991","unstructured":"Bundy, A., Grosse, G., and Brna, P. 1991. A recursive techniques editor for prolog. Instructional Science, 20:135\u2013172.","journal-title":"Instructional Science"},{"key":"5127976_CR7","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\u2013253. Also available from Edinburgh as DAI Research Paper No. 567.","journal-title":"Artificial Intelligence"},{"key":"5127976_CR8","unstructured":"Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A., and Stevens, A. 1989. A rational reconstruction and extension of recursion analysis. In N.S. Sridharan, editor, Proceedings of the 11th International Joint Conference on Artificial Intelligence. pp. 359\u2013365, Morgan Kaufmann. Also available from Edinburgh as DAI Research Paper No. 419."},{"key":"5127976_CR9","doi-asserted-by":"crossref","unstructured":"Bundy, A., van Harmelen, F., Horn, C., and Smaill, A. 1990. The oyster-clam system. In M.E. Stickel, editors, Proceedings of the 10th International Conference on Automated Deduction. Springer-Verlag, pp. 647\u2013648. Also available from Edinburgh as DAI Research Paper No. 507.","DOI":"10.1007\/3-540-52885-7_123"},{"key":"5127976_CR10","doi-asserted-by":"crossref","unstructured":"Cantu, F., Bundy, A., Smaill, A., and Basin, D. 1996. Experiments in automating hardware verification using inductive proof planning. In M. Srivas and A. Camilleri, editors, Proceedings of the Formal Methods for Computer-Aided Design Conference. Springer-Verlag, pp. 94\u2013108. Lecture Notes in Computer Science, vol. 1166. Also available from Edinburgh as DAI Research Paper No. 828.","DOI":"10.1007\/BFb0031802"},{"key":"5127976_CR11","doi-asserted-by":"crossref","unstructured":"Flach, P.A. and Kakas, A.C. (eds.). 2000. Abduction and Induction: Essays on Their Relation and Integration, vol. 18 of Applied Logic Series. Kluwer Academic Publishers.","DOI":"10.1007\/978-94-017-0606-3"},{"issue":"1\/2","key":"5127976_CR12","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0004-3702(97)00082-9","volume":"100","author":"I. Frank","year":"1998","unstructured":"Frank, I. and Basin, D. 1998. Search in games with incomplete information: A case study using bridge card play. Artificial Intelligence, 100(1\/2):87\u2013123.","journal-title":"Artificial Intelligence"},{"key":"5127976_CR13","unstructured":"Frank, I., Basin, D., and Bundy, A. 1992. An adaptation of proof-planning to declarer play in bridge. In Proceedings of the 10th European Conference on Artificial Intelligence, ECAI-92. Vienna, Austria, pp. 72\u201376. Also available from Edinburgh as DAI Research Paper No. 575."},{"key":"5127976_CR14","first-page":"87","volume-title":"Proceedings of the 10th European Conference on Artificial Intelligence, ECAI'92","author":"M. Franova","year":"1992","unstructured":"Franova, M. and Kodratoff, Y. 1992. Predicate synthesis from formal specifications. In B. Neumann, editors, Proceedings of the 10th European Conference on Artificial Intelligence, ECAI'92. John Wiley and Sons: Chichester, England, pp. 87\u201391."},{"key":"5127976_CR15","unstructured":"Gordon, M.J.C. and Melham, T.F. (eds.). 1993. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press."},{"key":"5127976_CR16","unstructured":"Hirata, K. 1994. Aclassification of abduction: Abduction for logic programming'. In Proceedings of the Fourteenth International Machine Learning Workshop, ML-14. p. 16. Also in Machine Intelligence 14."},{"key":"5127976_CR17","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\u2013490."},{"key":"5127976_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/BFb0013060","volume-title":"International Conference on Logic Programming and Automated Reasoning-LPAR 92","author":"A. Ireland","year":"1992","unstructured":"Ireland, A. 1992. The use of planning critics in mechanizing inductive proofs. In A. Voronkov, editors, International Conference on Logic Programming and Automated Reasoning-LPAR 92, St. Petersburg. Springer-Verlag, pp. 178\u2013189. Lecture Notes in Artificial Intelligence vol. 624. Also available from Edinburgh as DAI Research Paper No. 592."},{"issue":"1\/2","key":"5127976_CR19","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\/2):79\u2013111. Also available from Edinburgh as DAI Research Paper No. 716.","journal-title":"Journal of Automated Reasoning"},{"key":"5127976_CR20","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.P. Clement editors, Logic Program Synthesis and Transformation. Springer-Verlag, pp. 1\u201314. Also available as Max-Planck-Institut f\u00fcr Informatik Report MPI-I\u201392\u2013244 and Edinburgh DAI Research Report No. 603.","DOI":"10.1007\/978-1-4471-3560-9_1"},{"key":"5127976_CR21","doi-asserted-by":"crossref","unstructured":"Lowe, H. 1991a. Extending the proof plan methodology to computer configuration problems. Artificial Intelligence Applications Journal, 5(3). Also available from Edinburgh as DAI Research Paper No. 537.","DOI":"10.1080\/08839519108927927"},{"key":"5127976_CR22","unstructured":"Lowe, H. 1991b. The use of theorem proving techniques in expert systems for configuration. In J.-C. Rault editors, Proceedings of the Eleventh International Workshop on Expert Systems and their Applications, Avignon. Also available from Edinburgh as DAI Research Paper No. 536."},{"key":"5127976_CR23","first-page":"91","volume-title":"Proceedings of the 15th Conference on Automated Software Engineering","author":"R. Monroy","year":"2000","unstructured":"Monroy, R. 2000. The use of abduction and recursion-editor techniques for the correction of faulty conjectures. In P. Flenner and P. Alexander, editors, Proceedings of the 15th Conference on Automated Software Engineering. Grenoble, France: IEEE Computer Society Press. pp. 91\u201399. Celebrated on September 11\u201315, 2000."},{"key":"5127976_CR24","doi-asserted-by":"crossref","unstructured":"Monroy, R. 2001. Concept formation via proof planning failure. In R. Nieuwenhuis and A. Voronkov, editors, 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Springer-Verlag, pp. 718\u2013731.","DOI":"10.1007\/3-540-45653-8_50"},{"issue":"1","key":"5127976_CR25","first-page":"25","volume":"5","author":"R. Monroy","year":"2001","unstructured":"Monroy, R. and Bundy, A. 2001. On the correction of faulty formulae. Computaci\u00f3n y Sistemas, 5(1):25\u201337.","journal-title":"Computaci\u00f3n y Sistemas"},{"issue":"3","key":"5127976_CR26","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1023\/A:1008770222354","volume":"7","author":"R. Monroy","year":"2000","unstructured":"Monroy, R., Bundy, A., and Green, I. 2000. Planning proofs of equations in CCS. Automated Software Engineering, 7(3):263\u2013304.","journal-title":"Automated Software Engineering"},{"key":"5127976_CR27","series-title":"Edinburgh as DAI Research Paper","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-58216-9_29","volume-title":"Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning, LPAR'94","author":"R. Monroy","year":"1994","unstructured":"Monroy, R., Bundy, A., and Ireland, A. 1994. Proof plans for the correction of false conjectures. In F. Pfenning editors, Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning, LPAR'94. Kiev, Ukraine: Springer-Verlag, pp. 54\u201368. Also available from Edinburgh as DAI Research Paper No. 681."},{"key":"5127976_CR28","unstructured":"Moore, J.S. 1974. Computational logic: Structure sharing and proof of program properties, Part II. Ph.D. thesis, University of Edinburgh. Available from Edinburgh as DCL Memo No. 68 and from Xerox PARC, Palo Alto as CSL 75\u20132."},{"key":"5127976_CR29","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/BF03037089","volume":"8","author":"S. Muggleton","year":"1991","unstructured":"Muggleton, S. 1991. Inductive logic programming. New Generation Computing, 8:295\u2013318.","journal-title":"New Generation Computing"},{"key":"5127976_CR30","first-page":"281","volume-title":"Inductive Logic Programming","author":"S. Muggleton","year":"1992","unstructured":"Muggleton, S. and Feng, C. 1992. Efficient induction of logic programs. In S. Muggleton, editor, Inductive Logic Programming. New York, Academic Press, pp. 281\u2013298."},{"key":"5127976_CR31","unstructured":"Peirce, C.S. 1959. Collected Papers of Charles Sanders Peirce, vol. 2. C. Harston and P. Weiss, editors, Harvard University Press."},{"key":"5127976_CR32","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/3-540-61511-3_70","volume-title":"13th Conference on Automated Deduction","author":"M. Protzen","year":"1996","unstructured":"Protzen, M. 1996. Patching faulty conjectures. In M. McRobbie and J. Slaney, editors, 13th Conference on Automated Deduction, vol. 1104. New Brunswick, NJ, USA, Springer-Verlag, pp. 77\u201391. Lecture Notes in Artificial Intelligence."},{"key":"5127976_CR33","first-page":"239","volume":"5","author":"J.R. Quinlan","year":"1990","unstructured":"Quinlan, J.R. 1990. Learning logical definitions from relations. Machine Learning, 5:239\u2013266.","journal-title":"Machine Learning"},{"issue":"2","key":"5127976_CR34","first-page":"95","volume":"19","author":"B.L. Richards","year":"1995","unstructured":"Richards, B.L. and Mooney, R.J. 1995. Automated refinement of first-order horn-clause domain theories. Machine Learning, 19(2):95\u2013131.","journal-title":"Machine Learning"},{"key":"5127976_CR35","doi-asserted-by":"crossref","unstructured":"Smith, D.R. 1985. The top-down synthesis of divide and conquer algorithms. AI, 27(1).","DOI":"10.1016\/0004-3702(85)90083-9"},{"issue":"1","key":"5127976_CR36","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/0004-3702(94)90063-9","volume":"71","author":"C. Walther","year":"1994","unstructured":"Walther, C. 1994. On proving termination of algorithms by machine. Artificial Intelligence, 71(1):101\u2013157.","journal-title":"Artificial Intelligence"},{"key":"5127976_CR37","doi-asserted-by":"crossref","unstructured":"Whittle, J., Bundy, A., Boulton, R., and Lowe, H. 1999. An ML editor based on proofs-as-programs. In Proceedings of the 14th IEEE International Conference on Automated Software Engineering, ASE'99. Cocoa Beach, Florida, USA, pp. 166\u2013173. Earlier version available as Research Paper No. 939, DAI, University of Edinburgh.","DOI":"10.1109\/ASE.1999.802196"},{"key":"5127976_CR38","unstructured":"Wong, W. and Curzon, P. 1994. A theory of lists for HOL based on higher-order functions. In T. Melham and J. Camilleri, editors, The Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications, University of Malta."}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1024448931103.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1024448931103\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1024448931103.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:26:29Z","timestamp":1748071589000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1024448931103"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,7]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,7]]}},"alternative-id":["5127976"],"URL":"https:\/\/doi.org\/10.1023\/a:1024448931103","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"type":"print","value":"0928-8910"},{"type":"electronic","value":"1573-7535"}],"subject":[],"published":{"date-parts":[[2003,7]]}}}