{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:18:46Z","timestamp":1725455926460},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540536864"},{"type":"electronic","value":"9783540469827"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/bfb0018443","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T05:30:30Z","timestamp":1132637430000},"page":"212-226","source":"Crossref","is-referenced-by-count":0,"title":["Constructive matching \u2014 A methodology for inductive theorem proving"],"prefix":"10.1007","author":[{"given":"Marta","family":"Fra\u0148ov\u00e1","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1016\/0304-3975(79)90035-5","volume":"9","author":"R. Aubin","year":"1979","unstructured":"R. Aubin: Mechanizing Structural Induction. Part 2: Strategies; Theoretical Computer Science 9, North-Holland, 1979, 347\u2013362.","journal-title":"Theoretical Computer Science"},{"key":"14_CR2","first-page":"69","volume-title":"Automatic Program Construction Techniques","author":"W. Bibel","year":"1984","unstructured":"W. Bibel, K. M. Hoernig: LOPS \u2014 A System Based on a Strategical Approach to Program Synthesis; in [3], 69\u201391."},{"volume-title":"Automatic Program Construction Techniques","year":"1984","key":"14_CR3","unstructured":"A. Biermann, G. Guiho, Y. Kodratoff (ed): Automatic Program Construction Techniques; Macmillan Publishing Company, London, 1984."},{"key":"14_CR4","first-page":"553","volume-title":"Automated synthesis of recursive algorithms as a theorem proving tool","author":"S. Biundo","year":"1988","unstructured":"S. Biundo: Automated synthesis of recursive algorithms as a theorem proving tool; in [16], 553\u2013558."},{"key":"14_CR5","unstructured":"R. S. Boyer, J S. Moore: A Computational Logic; Academic Press, 1979."},{"key":"14_CR6","unstructured":"A. Bundy, (ed): Proceedings of the Eigth International Joint Conference on Artificial Intelligence; August, Karlsruhe, 1983."},{"key":"14_CR7","first-page":"359","volume-title":"A Rational Reconstruction and Extension of Recursion Analysis","author":"A. Bundy","year":"1989","unstructured":"A. Bundy, F. van Harmelen, J. Hessketh, A. Smail, A. Stevens: A Rational Reconstruction and Extension of Recursion Analysis; in [23], 359\u2013365."},{"key":"14_CR8","unstructured":"N. Dershowitz: Synthesis by Completion; in [13] 208\u2013214."},{"key":"14_CR9","first-page":"137","volume-title":"Fundamentals for a new methodology for inductive theorem proving: CM-construction of atomic formulae","author":"M. Franova","year":"1988","unstructured":"M. Franova: Fundamentals for a new methodology for inductive theorem proving: CM-construction of atomic formulae; in [16], 137\u2013141."},{"key":"14_CR10","volume-title":"Fundamentals of a new methodology for Program Synthesis from Formal Specifications: CM-construction of atomic formulae","author":"M. Franova","year":"1988","unstructured":"M. Franova: Fundamentals of a new methodology for Program Synthesis from Formal Specifications: CM-construction of atomic formulae; Thesis, Universit\u00e9 Paris-Sud, November, Orsay, France, 1988."},{"key":"14_CR11","unstructured":"M. Franova: Explanations in Inductive Theorem Proving; to appear in proceedings of AAAI-90, 1990."},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/3-540-17220-3_19","volume-title":"Rewriting Techniques and Applications; Proceedings","author":"J. H. Gallier","year":"1987","unstructured":"J. H. Gallier, W. Snyder: A General complete E-unification procedure; in [17], 216\u2013228."},{"key":"14_CR13","unstructured":"A. K. Joshi, (ed): Proceedings of the Ninth International Joint Conference on Artificial Intelligence; August, Los Angeles, 1985."},{"key":"14_CR14","unstructured":"Y. Kodratoff, M.Picard: Compl\u00e9tion de syst\u00e8mes de r\u00e9\u00e9criture et synth\u00e8se de programmes \u00e0 partir de leurs sp\u00e9cifications; Bigre No.35, October, 1983."},{"key":"14_CR15","unstructured":"Y. Kodratoff, J. Castaing: Trivializing the proof of trivial theorems; in In 930."},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Y. Kodratoff: Proceedings of the 8th European Conference on Artificial Intelligence; August 1\u20135, Pitman, London, United Kingdom, 1988.","DOI":"10.1016\/B978-0-08-050930-3.50004-X"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Rewriting Techniques and Applications; Proceedings","year":"1987","unstructured":"P. Lescane, (ed): Rewriting Techniques and Applications; Proceedings, Lecture Notes in Computer Science 256, May, Springer-Verlag, Bordeaux, France, 1987."},{"issue":"1","key":"14_CR18","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Z. Manna, R. Waldinger: A Deductive Approach to Program Synthesis; ACM Transactions on Programming Languages and Systems, Vol. 2., No.1, January, 1980, 90\u2013121.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"W. Nutt, P. R\u00e9ty, G. Smolka: Basic Narowing Revisited; J. Symbolic Computation No. 7, 1989, 295\u2013317.","DOI":"10.1016\/S0747-7171(89)80014-8"},{"key":"14_CR20","unstructured":"H. Perdrix: Program synthesis from specifications; ESPRIT'85, Status Report of Continuing Work, North-Holland, 1986, 371\u2013385."},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/3-540-17220-3_20","volume-title":"Rewriting Techniques and Applications","author":"P. R\u00e9ty","year":"1987","unstructured":"P. R\u00e9ty: Improving basic narrowing techniques; in [17], 228\u2013242."},{"issue":"1","key":"14_CR22","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/0004-3702(85)90083-9","volume":"27","author":"D. R. Smith","year":"1985","unstructured":"D. R. Smith: Top-Down Synthesis of Simple Divide and Conquer Algorithm; Artificial Intelligence, vol. 27, no. 1, 1985, 43\u201396.","journal-title":"Artificial Intelligence"},{"key":"14_CR23","unstructured":"N. S. Sridharan: Proceedings of the Eleventh International Joint Conference on Artificial Intelligence; August 20\u201325 1989, Morgan Kaufmann, California, 1989."},{"key":"14_CR24","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. L. Chang","year":"1973","unstructured":"C. L. Chang, R.Ch.T. Lee: Symbolic Logic and Mechanical Theorem Proving; Academic Press, New York, 1973."},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"M. Franova: PRECOMAS \u2014 An Implementation of Constructive Matching Methodology; to appear in proceedings of ISSAC-90, Tokyo, Japon, 1990.","DOI":"10.1145\/96877.96885"}],"container-title":["Lecture Notes in Computer Science","Logics in AI"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0018443","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T02:36:25Z","timestamp":1586572585000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0018443"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540536864","9783540469827"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0018443","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}