{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,8]],"date-time":"2025-01-08T05:31:51Z","timestamp":1736314311331,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540564331"},{"type":"electronic","value":"9783540475576"}],"license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"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":[[1993]]},"DOI":"10.1007\/bfb0030394","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:32:44Z","timestamp":1138203164000},"page":"184-208","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Predicate synthesis from formal specifications: Using mathematical induction for finding the preconditions of theorems"],"prefix":"10.1007","author":[{"given":"Marta","family":"Fra\u0148ov\u00e1","sequence":"first","affiliation":[]},{"given":"Yves","family":"Kodratoff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,21]]},"reference":[{"key":"9_CR1","unstructured":"E. Beth: Les fondements logiques des mathematiques; Paris-Louvain, 1955."},{"key":"9_CR2","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. L. Chang","year":"1973","unstructured":"C. L. Chang, R.Ch.T. Lcc: Symbolic Logic and Mechanical Theorem Proving; Academic Press, New York, 1973."},{"key":"9_CR3","unstructured":"N. Dershowitz: Synthesis by Completion; in: A. K. Joshi, (ed): Proceedings of the Ninth International Joint Conference on Artificial Intelligence; August, Los Angeles, 1985, 208\u2013214."},{"key":"9_CR4","volume-title":"Rapport de Recherche No.646","author":"M. Fra\u0148ov\u00e1","year":"1991","unstructured":"M. Fra\u0148ov\u00e1, Y. Kodratoff: Predicate Synthesis from Formal Specifications or Using Mathematical Induction for finding the preconditions of theorems; Rapport de Recherche No.646, L.R.I., Universit\u00e9 de Paris-Sud, Orsay, France, February, 1991."},{"key":"9_CR5","volume-title":"Rapport de Recherche No.752","author":"M. Fra\u0148ov\u00e1","year":"1992","unstructured":"M. Fra\u0148ov\u00e1, 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":"9_CR6","unstructured":"M. Fra\u0148ov\u00e1, Y. Kodratoff: Predicate Synthesis from Formal Specifications; to appear in the proceedings of ECAI'92, 1992."},{"key":"9_CR7","unstructured":"M. Fra\u0148ov\u00e1: CM \u2014 Strategy \u2014 Driven Deductions for Automatic Programming; in: T. O'Shea, (ed.): ECAI-84: Advances in Artificial Intelligence; North-Holland, 1984, 573\u2013576."},{"key":"9_CR8","volume-title":"Rapport de Recherche No.376","author":"M. Fra\u0148ov\u00e1","year":"1987","unstructured":"M. Fra\u0148ov\u00e1: PRECOMAS Challenge; Rapport de Recherche No.376, L.R.I., Universit\u00e9 de Paris-Sud, Orsay, France, September, 1987."},{"key":"9_CR9","unstructured":"M. Fra\u0148ov\u00e1: 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; August, Los Angeles, 1985, 1214\u20131220."},{"key":"9_CR10","first-page":"559","volume-title":"An Implementation of Program Synthesis from Formal Specifications","author":"M. Fra\u0148ov\u00e1","year":"1988","unstructured":"M. Fra\u0148ov\u00e1: An Implementation of Program Synthesis from Formal Specifications; in: Y. Kodratoff, (ed.): Proceedings of the 8th European Conference on Artificial Intelligence; August 1\u20135, Pitman, London, United Kingdom, 1988, 559\u2013564."},{"key":"9_CR11","first-page":"137","volume-title":"Fundamentals for a new methodology for inductive theorem proving: CM-construction of atomic formulae","author":"M. Fra\u0148ov\u00e1","year":"1988","unstructured":"M. Fra\u0148ov\u00e1: Fundamentals for a new methodology for inductive theorem proving: CM-construction of atomic formulae; in: Y. Kodratoff, (ed.): Proceedings of the 8th European Conference on Artificial Intelligence; August 1\u20135, Pitman, London, United Kingdom, 1988, 137\u2013141."},{"key":"9_CR12","volume-title":"Thesis","author":"M. Fra\u0148ov\u00e1","year":"1988","unstructured":"M. Fra\u0148ov\u00e1: 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":"9_CR13","unstructured":"M. Fra\u0148ov\u00e1: A constructive proof for Prime Factorization Theorem: A result of putting it together in Constructive Matching methodology; forthcoming, 1992."},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"M. Fra\u0148ov\u00e1: Constructive Matching-Explanation Based Methodology for Inductive Theorem Proving; in: J. Dassow, J. Kelemen, (ed.): Aspects and Prospects of Theoretical Computer Science; LNCS 464, Springer-Verlag, 1990, 138\u2013147.","DOI":"10.1007\/3-540-53414-8_36"},{"key":"9_CR15","unstructured":"M. Fra\u0148ov\u00e1: Failure analysis in Constructive Matching methodology; forthcoming, 1993."},{"key":"9_CR16","unstructured":"M. Fra\u0148ov\u00e1: Constructive Matching methodology for Inductive Theorem Proving and Program Synthesis revisited; forthcoming, 1993."},{"key":"9_CR17","series-title":"Rapport de Recherche","volume-title":"A Step Toward Creative Automated Inductive Theorem Proving","author":"M. Fra\u0148ov\u00e1","year":"1991","unstructured":"M. Fra\u0148ov\u00e1: Constructive Matching Methodology. A Step Toward Creative Automated Inductive Theorem Proving; Rapport de Recherche No. 668, L.R.I., Universit\u00e9 de Paris-Sud, Orsay, France, 1991."},{"key":"9_CR18","first-page":"53","volume-title":"Lecture Notes in Computer Science 87","author":"G. Guiho","year":"1980","unstructured":"G. Guiho, Ch. Grosse: Program synthesis from incomplete specifications; in: W. Bibel, R. Kowalski (ed): Proceedings of the 5-th Conference on Automated Deduction; Lecture Notes in Computer Science 87, Springer-Verlag, Les Arcs, France, 1980, 53\u201363."},{"key":"9_CR19","volume-title":"An Introduction to Machine Learning","author":"Y. Kodratoff","year":"1988","unstructured":"Y. Kodratoff: An Introduction to Machine Learning; Pitman, London, 1988."},{"key":"9_CR20","unstructured":"M. Lebowitz: Concept learning in a rich input domain: Generalization-based Memory; in: R. Michalski, Jaime G. Carbonell, Tom M. Mitchel (eds): Machine Learning: An Artificial Intelligence Approach II; Morgan Kaufmann, 1986, 193\u2013214."},{"issue":"No.1","key":"9_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 Transactions on Programming Languages and Systems, Vol. 2., No.1, January, 1980, 90\u2013121.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"9_CR22","first-page":"517","volume-title":"Automatic Program Construction Techniques","author":"R. Michalski","year":"1984","unstructured":"R. Michalski: Inductive Learning as Rule-guidcd Transformation of Symbolic Descriptions: a Theory and Implementation; in: A. Biermann, G. Guiho.Y. Kodratoff (ed): Automatic Program Construction Techniques; Macmillan Publishing Company, London, 1984, 517\u2013522."},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"S. Muggleton, W. Buntine: Machine Invention of First Order Predicates by Inverting Resolution; in Proceedings of the 5th International Conference on Machine Learning, Pitman, 1988, 339\u2013352.","DOI":"10.1016\/B978-0-934613-64-4.50040-2"},{"key":"9_CR24","first-page":"557","volume-title":"Automatic Program Construction Techniques","author":"C. Rouveirol","year":"1984","unstructured":"C. Rouveirol: Postponing Choices when Inverting Resolution; in: A. Biermann, G. Guiho.Y. Kodratoff (ed): Automatic Program Construction Techniques; Macmillan Publishing Company, London, 1984, 557\u2013562."},{"key":"9_CR25","unstructured":"C. Rouveirol, J. F. Puget: A Simple Solution for Inverting Resolution; Proceedings of the 4th European Working session on Learning, Pitman, 1989, 201\u2013211."},{"key":"9_CR26","unstructured":"C. Sammut, R. B. Banerji: Learning Concepts by Asking Questions; in: R. Michalski, Jaime G. Carbonell, Tom M. Mitchel (eds): Machine Learning: An Artificial Intelligence Approach II; Morgan Kaufmann, 1986, 167\u2013192."},{"key":"9_CR27","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1192.001.0001","volume-title":"Algorithmic Programm Debugging","author":"E. Y. Shapiro","year":"1983","unstructured":"E. Y. Shapiro, E. Y. Shapiro: Algorithmic Programm Debugging; MIT Press, Cambridge, MA, 1983."},{"key":"9_CR28","first-page":"302","volume-title":"From Frege to Godel, A source book in mathematical logic, 1879\u20131931","author":"T. Skolem","year":"1967","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, A source book in mathematical logic, 1879\u20131931; Harvard University Press, Cambridge, Massachusets, 1967, 302\u2013334."},{"key":"9_CR29","unstructured":"D. R. Smith: Derived preconditions and their use in program synthesis; in: D. W. Loveland, (ed.): 6th Conference on Automated Deduction; LNCS 138, Springer-Verlag, 1982, 172\u2013193."},{"key":"9_CR30","unstructured":"P. E. Utgoff: Shift of Bias for Inductive Concept Learning; in: R. Michalski, Jaime G. Carbonell, Tom M. Mitchel (eds): Machine Learning: An Artificial Intelligence Approach II; Morgan Kaufmann, 1986, 107\u2013148."},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"C. Vrain: OGUST: A system that Learns Using Domain Properties Expressed as Theorems; in: Y. Kodratoff, R. S. Michalski: Machine Learning An Artificial Intelligence Approach, Volume III; Morgan Kaufmann, 1990, 360\u2013382.","DOI":"10.1016\/B978-0-08-051055-2.50020-1"}],"container-title":["Lecture Notes in Computer Science","Nonmonotonic and Inductive Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0030394","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T11:57:48Z","timestamp":1736251068000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0030394"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540564331","9783540475576"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/bfb0030394","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]},"assertion":[{"value":"21 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}