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
Mathematical Induction in Otter-Lambda, Journal of Automated Reasoning, vol.5, issue.2, pp.311-344, 2006. ,
DOI : 10.1007/s10817-006-9036-z
Syntax-directed, semantics-supported program synthesis, Artificial Intelligence, vol.14, issue.3, pp.243-261, 1980. ,
DOI : 10.1016/0004-3702(80)90050-8
Automated induction proofs using methods of program synthesis, Computers and Artificial Intelligence, vol.3, issue.6, pp.473-481, 1984. ,
The OYSTER-CLAM system, Proc. 10th International Conference on Automated Deduction, pp.647-648, 1990. ,
DOI : 10.1007/3-540-52885-7_123
Rippling: Meta-level guidance for mathematical reasoning, 2005. ,
DOI : 10.1017/CBO9780511543326
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
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
Oeuvres philosophiques ,
CM-strategy : A methodology for inductive theorem proving or constructive well-generalized proofs, Proc. of the Ninth IJCAI, pp.1214-1220, 1985. ,
Fundamentals of a new methodology for program synthesis from formal specifications: CMconstruction of atomic formulae " ; Thesis, 1988. ,
Precomas 0.3 user guide, Research Report No. L.R.I, vol.524, 1989. ,
Constructive Matching methodology and automatic plan-construction revisited, Research Report No. L.R.I, vol.874, 1993. ,
Créativité Formelle: méthode et pratique conception des systèmes 'informatiques' complexes et brevet épistémologique, Publibook, 2008. ,
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. ,
The role of recursion in and for scientific creativity, Cybernetics and Systems Proc. of the 20th EMCSR, pp.573-578, 2010. ,
On computational creativity: 'inventing' theorem proofs, Proc. 18th ISMIS, LNAI 5722, pp.573-581, 2009. ,
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. ,
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. ,
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
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
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
The foundation of a generic theorem prover, Journal of Automated Reasoning, vol.49, issue.3, pp.363-397, 1989. ,
DOI : 10.1007/BF00248324
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