{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:11:45Z","timestamp":1725664305508},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540612865"},{"type":"electronic","value":"9783540684404"}],"license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61286-6_179","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:24:37Z","timestamp":1330273477000},"page":"551-560","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automated inductive reasoning as a support of deductive reasoning in a user-independent automation of inductive theorem proving"],"prefix":"10.1007","author":[{"given":"Marta","family":"Franov\u00e1","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"53_CR1","first-page":"17","volume":"971","author":"S. Agerholm","year":"1995","unstructured":"S. Agerholm: Non-Primitive Recursive Function Definitions; in: Higher Order Logic Theorem Proving and Its Applications; LNCS 971, 1995, 17\u201331.","journal-title":"LNCS"},{"key":"53_CR2","doi-asserted-by":"crossref","unstructured":"R. Aubin: Mechanizing Structural Induction. Part 1: Formal System; Theoretical Computer Science 9, North-Holland, 1979, 329\u2013345.","DOI":"10.1016\/0304-3975(79)90034-3"},{"key":"53_CR3","unstructured":"E. Beth: The Foundations of Mathematics; Amsterdam, 1959."},{"key":"53_CR4","unstructured":"R. S. Boyer, J S. Moore: A Computational Logic; Academic Press, 1979."},{"key":"53_CR5","doi-asserted-by":"crossref","unstructured":"P. A. Fejer, D.A. Simovici: Mathematical Foundations of Computer Science, Volume 1: Sets, Relations, and Induction; Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4612-3086-1_2"},{"key":"53_CR6","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; World Scientific, 1992, 1553\u20131560."},{"key":"53_CR7","volume-title":"Rapport de Recherche No.752","author":"M. Franova","year":"1992","unstructured":"M. Franova, Y. Kodratoff: Practical Problems in the Automatization of Inductive Theorem Proving; Rapport de Recherche No.752, L.R.I., Universit\u00e9 de Paris-Sud, Orsay, France, Mai, 1992."},{"key":"53_CR8","unstructured":"M. Franova, Y. Kodratoff: Predicate Synthesis from Formal Specifications; in: B. Neumann, (ed.): ECAI 92, John Wiley & Sons Ltd., 1992, 87\u201391."},{"key":"53_CR9","first-page":"476","volume":"689","author":"M. Franova","year":"1993","unstructured":"M. Franova, Y. Kodratoff, M. Gross: Constructive Matching Methodology: Formally Creative or Intelligent Inductive Theorem Proving?; in: proc. of ISMIS'93, L.N.A.I. 689, 1993, 476\u2013485.","journal-title":"L.N.A.I."},{"key":"53_CR10","unstructured":"M. Franova, L. Popelinsky: Synthesis of Formal Specifications of Predicates; a draft version, Rap. de Recherche No.866, L.R.I., July, 1993."},{"key":"53_CR11","unstructured":"M. Franova: CM-strategy: A Methodology for Inductive Theorem Proving or Constructive Well-Generalized Proofs; in: A. K. Joshi, (ed): Proceedings of the Ninth International Joint Conference on Artificial Intelligence; 1985, 1214\u20131220."},{"key":"53_CR12","unstructured":"M. Franova: Proving Implications in Inductive Theorem Proving; in: R. Trappl, ed.: Cybernetics and Systems'94; World Scientific, 1994, 1777\u20131784."},{"key":"53_CR13","unstructured":"M. Franova: Constructive Matching methodology: a standard way of proving user-independently theorems by induction; Rap.de Recherche No.973, L.R.I., Mai, 1995."},{"key":"53_CR14","unstructured":"M. Franova: A standard proof by Constructive Matching methodology for a theorem formulated by Skolem; Rapport de Recherche No.972, L.R.I., Mai, 1995."},{"key":"53_CR15","unstructured":"M. Franova: A synthesis of a definition recursive with respect to the second argument for the Ackermann-Peter's function \u2014 a puzzle solved by Constructive Matching methodology; Rapport de Recherche No.971, L.R.I., Mai, 1995."},{"key":"53_CR16","unstructured":"M. Franova: A Theory of Constructible Domains \u2014 a formalization of inductively defined systems of objects for a user-independent automation of inductive theorem proving, Part I; Rapport de Recherche No.970, L.R.I., Mai, 1995."},{"key":"53_CR17","unstructured":"M. Franova: Modifying and Justifying Recursive Programs in Inductive Theorem Proving: Why and How, to appear in proc. of European Meeting on Cybernetics and Systems'96."},{"key":"53_CR18","doi-asserted-by":"crossref","unstructured":"D. Hutter: Synthesis of Induction Orderings for Existence Proofs; in: A. Bundy, ed.: Automated Deduction \u2014 CADE-12; LNAI 814, Springer-Verlag, 1994, 29\u201341.","DOI":"10.1007\/3-540-58156-1_3"},{"key":"53_CR19","unstructured":"S. C. Kleene: Introduction to Meta-Mathematics, North-Holland, 1980."},{"key":"53_CR20","doi-asserted-by":"crossref","unstructured":"G. Le Blanc: BMWk Revisited \u2014 Generalization and Formalization of an Algorithm for Detecting Recursive Relations in Term Sequences; in: proc. ECML-94; LNAI 784, Springer-Verlag, 1994, 183\u2013197.","DOI":"10.1007\/3-540-57868-4_58"},{"issue":"No.2","key":"53_CR21","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BF00881916","volume":"15","author":"L. C. Paulson","year":"1995","unstructured":"L. C. Paulson: Set Theory for Verification; Journal of Automated Reasoning Vol. 15, No.2, 1995, 167\u2013215.","journal-title":"Journal of Automated Reasoning"},{"key":"53_CR22","volume-title":"Recursive Functions","author":"R. P\u00e9ter","year":"1967","unstructured":"R. P\u00e9ter: Recursive Functions; Academic Press, New York, 1967."},{"key":"53_CR23","doi-asserted-by":"crossref","unstructured":"Ch. Walther: Argument-Bounded Algorithms as a Basis for Automated Termination Proofs; in proc. of CADE-10, LNAI 449, 602\u2013621.","DOI":"10.1007\/BFb0012861"},{"key":"53_CR24","unstructured":"Ch. Walther: Combining Inductions Axioms by Machine, in proc of IJCAI-93, Morgan Kaufman, 95\u2013101."},{"key":"53_CR25","unstructured":"H. Zhang, D. Kapur, M.S. Krishnamoorthy: A Mechanizable Induction Principle For Equational Specifications; in: E. Lusk, R. Overbeek, (ed): in proc of CADE-9; LNCS 310, 1988, 162\u2013179."}],"container-title":["Lecture Notes in Computer Science","Foundations of Intelligent Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61286-6_179","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:30:24Z","timestamp":1558254624000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61286-6_179"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540612865","9783540684404"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-61286-6_179","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]},"assertion":[{"value":"1 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}