A. Asperti, C. S. Coen, E. Tassi, and S. Zacchiroli, User Interaction with the Matita Proof Assistant, Journal of Automated Reasoning, vol.11, issue.3, pp.109-139, 2007.
DOI : 10.1007/s10817-007-9070-5

M. Beeson, Mathematical Induction in Otter-Lambda, Journal of Automated Reasoning, vol.5, issue.2, pp.311-344, 2006.
DOI : 10.1007/s10817-006-9036-z

W. Bibel, Syntax-directed, semantics-supported program synthesis, Artificial Intelligence, vol.14, issue.3, pp.243-261, 1980.
DOI : 10.1016/0004-3702(80)90050-8

S. Biundo and F. Zboray, Automated induction proofs using methods of program synthesis, Computers and Artificial Intelligence, vol.3, issue.6, pp.473-481, 1984.

A. Bundy, F. Van-harnelen, C. Horn, and A. Smaill, The OYSTER-CLAM system, Proc. 10th International Conference on Automated Deduction, pp.647-648, 1990.
DOI : 10.1007/3-540-52885-7_123

A. Bundy, D. Basin, D. Hutter, and A. Ireland, Rippling: Meta-level guidance for mathematical reasoning, 2005.
DOI : 10.1017/CBO9780511543326

T. Coquand and G. Huet, Constructions: A higher order proof system for mechanizing mathematics, Proc
DOI : 10.1007/3-540-15983-5_13

URL : https://hal.archives-ouvertes.fr/inria-00076155

N. Dershowitz and U. S. Reddy, Deductive and inductive synthesis of equational programs, Journal of Symbolic Computation, vol.15, issue.5-6, pp.463-466, 1993.
DOI : 10.1016/S0747-7171(06)80002-7

]. R. Descartes, Oeuvres philosophiques

M. Franova, CM-strategy : A methodology for inductive theorem proving or constructive well-generalized proofs, Proc. of the Ninth IJCAI, pp.1214-1220, 1985.

M. Franova, Fundamentals of a new methodology for program synthesis from formal specifications: CMconstruction of atomic formulae " ; Thesis, 1988.

M. Franova, Precomas 0.3 user guide, Research Report No. L.R.I, vol.524, 1989.

M. Franova, Constructive Matching methodology and automatic plan-construction revisited, Research Report No. L.R.I, vol.874, 1993.

M. Franova, Créativité Formelle: méthode et pratique conception des systèmes 'informatiques' complexes et brevet épistémologique, Publibook, 2008.

M. Franova, A construction of a definition recursive with respect to the second variable for the Ackermann's function, Research Report L.R.I, issue.1511, 2009.

M. Franova, The role of recursion in and for scientific creativity, Cybernetics and Systems Proc. of the 20th EMCSR, pp.573-578, 2010.

M. Franova and Y. Kodratoff, On computational creativity: 'inventing' theorem proofs, Proc. 18th ISMIS, LNAI 5722, pp.573-581, 2009.

M. Franova and Y. Kodratoff, Two examples of computational creativity: ILP multiple predicate synthesis and the 'assets' in theorem proving, Advances in Machine Learning II: Dedicated to the Memory of Professor Ryszard S. Michalski, pp.155-174, 2010.

M. Franova and M. Kooli, Recursion manipulation for robotics: Why and how?, Proc. of the Fourteenth Meeting on Cybernetics and Systems Research, Austrian Society for Cybernetic Studies, Austria, pp.836-841, 1998.

D. Kapur, An overview of Rewrite Rule Laboratory (RRL), Computers & Mathematics with Applications, vol.29, issue.2, pp.91-114, 1995.
DOI : 10.1016/0898-1221(94)00218-A

Z. Manna and R. Waldinger, A Deductive Approach to Program Synthesis, ACM Transactions on Programming Languages and Systems, vol.2, issue.1, pp.90-121, 1980.
DOI : 10.1145/357084.357090

C. Paulin-mohring and B. Werner, Synthesis of ML programs in the system Coq, Journal of Symbolic Computation, vol.15, issue.5-6, pp.607-640, 1993.
DOI : 10.1016/S0747-7171(06)80007-6

L. C. Paulson, The foundation of a generic theorem prover, Journal of Automated Reasoning, vol.49, issue.3, pp.363-397, 1989.
DOI : 10.1007/BF00248324

D. R. Smith, Top-down synthesis of divide-and-conquer algorithms, Artificial Intelligence, vol.27, issue.1, pp.43-96, 1985.
DOI : 10.1016/0004-3702(85)90083-9