{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:06:30Z","timestamp":1725663990340},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540568049"},{"type":"electronic","value":"9783540477501"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56804-2_44","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:40:53Z","timestamp":1330256453000},"page":"476-485","source":"Crossref","is-referenced-by-count":2,"title":["Constructive matching methodology: Formally creative or Intelligent inductive theorem proving?"],"prefix":"10.1007","author":[{"given":"Marta","family":"Fra\u0148ov\u00e1","sequence":"first","affiliation":[]},{"given":"Yves","family":"Kodratoff","sequence":"additional","affiliation":[]},{"given":"Martine","family":"Gross","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"44_CR1","unstructured":"R. S. Boyer, J S. Moore: A Computational Logic; Academic Press, 1979."},{"key":"44_CR2","doi-asserted-by":"crossref","unstructured":"R. S. Boyer, Y. Yu: Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor; in: CADE 11 Proc, Springer, 1992, 416\u2013430.","DOI":"10.1007\/3-540-55602-8_181"},{"issue":"no.3","key":"44_CR3","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/BF00244273","volume":"1","author":"R. L. Constable","year":"1985","unstructured":"R. L. Constable, T.B. Knoblock, J.L. Bates: Writing Programs that construct Proofs; Journal of Automated Reasoning, vol. 1, no. 3, 1985, 285\u2013326.","journal-title":"Journal of Automated Reasoning"},{"key":"44_CR4","unstructured":"M. Franova, A. Galton: Failure Analysis in Constructive Matching Methodology: A Step Towards Autonomous Program Synthesizing Systems; in: R. Trappl, (ed): Cybernetics and System Research '92; 1553\u20131560."},{"key":"44_CR5","unstructured":"M. Franova, Y. Kodratoff, M. Gross: Constructive matching methodology: an extension and an application to a planning problem; forthcoming, 1993."},{"key":"44_CR6","unstructured":"an extended version of this paper; forthcoming, 1993."},{"key":"44_CR7","unstructured":"M. Franova, Y. Kodratoff: Practical Problems in the Automatization of Inductive Theorem Proving; Rapport de Recherche No.752, L.R.I., 1992."},{"key":"44_CR8","unstructured":"M. Franova, Y. Kodratoff: How to Clear a Block with Constructive Matching methodology; in: Proc. IJCAI'91; Morgan Kaufmann, 1991, 232\u2013337."},{"key":"44_CR9","unstructured":"M. Franova, Y. Kodratoff: Predicate Synthesis from Formal Specifications; in: B. Neumann, (ed.): ECAI 92 proceedings, John Wiley & Sons Ltd., 1992, 87\u201391."},{"key":"44_CR10","unstructured":"M. Franova, Y. Kodratoff: Predicate Synthesis from Formal Specifications: Using Mathematical Induction for Finding the Preconditions of Theorems; to appear in proceedings of NIL'92, available as Rapport de Recherche No.781, L.R.I., 1992."},{"key":"44_CR11","unstructured":"M. Franova, Y. Kodratoff: Simplifying Implications in Inductive Theorem Proving: Why and How?; Rapport de Recherche No.788, L.R.I., 1992."},{"key":"44_CR12","unstructured":"M. Franova, L. Popelinsky: Constructing formal specifications of predicates; forthcoming, 1993."},{"key":"44_CR13","unstructured":"M. Franova: Program Synthesis and Constructive proofs Obtained by Beth's tableaux; in: R. Trappl, (ed): Cybernetics and System Research 2; 1984, 715\u2013720."},{"key":"44_CR14","unstructured":"M. Franova: CM-strategy; A Methodology for Inductive Theorem Proving or Constructive Well-Generalized Proofs; in Proc. IJCAI'85, 1214\u20131220."},{"key":"44_CR15","unstructured":"M. Franova: Fundamentals of a new methodology for Program Synthesis from Formal Specifications: CM-construction of atomic formulae; Thesis, 1988."},{"key":"44_CR16","unstructured":"M. Franova: Precomas 0.3 User Guide; Rap. de Rech. No.524, L.R.I., 1989."},{"key":"44_CR17","unstructured":"M. Franova: A constructive proof for prime factorization theorem: A result of putting it together in constructive matching methodology; R.R. No.780, L.R.I., 1992."},{"key":"44_CR18","unstructured":"Franova: PRECOMAS: An Implementation of CM; Proc. of ISSAC'90, 16\u201323."},{"key":"44_CR19","unstructured":"M. Franova: Generating induction hypotheses by Constructive Matching methodology for ITP and PS revisited; Rapport de Recherche No.647, L.R.I., 1991."},{"key":"44_CR20","unstructured":"H. Kirchner: Preuves par Compl\u00e9tion; Thesis, 21 June, 1985."},{"issue":"No.1","key":"44_CR21","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 Trans. on Prog. Languages and Systems, Vol. 2., No.1, January, 1980, 90\u2013121.","journal-title":"ACM Trans. on Prog. Languages and Systems"},{"key":"44_CR22","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/BF00247434","volume":"3","author":"Z. Manna","year":"1987","unstructured":"Z. Manna, R. Waldinger: How to Clear a Block: A Theory of Plans; Journal of Automated Reasoning 3, 1987, 343\u2013377.","journal-title":"Journal of Automated Reasoning"},{"key":"44_CR23","unstructured":"G. Polya: How to solve it; 1957."},{"key":"44_CR24","unstructured":"T. Skolem: The foundations of elementary mathematic established by means of the recursive mode of thought, without the use of apparent variables ranging over infinite domains; in: J. van Heijenoort: From Frege to Godel; 1967, 302\u2013334."}],"container-title":["Lecture Notes in Computer Science","Methodologies for Intelligent Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56804-2_44.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T00:56:19Z","timestamp":1619571379000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56804-2_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540568049","9783540477501"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-56804-2_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}