%0 Book Section %9 OS CH : Chapitres d'ouvrages scientifiques %A Bengeloune, I. %T Induction and synthesis by simplification %B CARI'96 : actes du 3ème colloque africain sur la recherche en informatique = CARI'96 : proceedings of the 3rd African conference on research in computer science %C Paris %D 1996 %E Moukeli, P. %L fdi:010008764 %G ENG %I ORSTOM %@ 2-7099-1333-X %K INDUCTION ; ALGORITHME ; SYNTHESE ; AUTOMATISATION ; INTELLIGENCE ARTIFICIELLE %P 545-559 %U https://www.documentation.ird.fr/hor/fdi:010008764 %> https://horizon.documentation.ird.fr/exl-doc/pleins_textes/pleins_textes_6/colloques2/010008764.pdf %W Horizon (IRD) %X Les formules existentielles jouent un rôle important dans le domaine de la synthèse déductive de programmes. Nous présentons une méthode permettant la construction (automatique) de preuves de validité de formules existentielles dans le modèle initial d'un ensemble d'équations. Cette méthode est basée sur une notion de "cover set" et de système de réécriture ordonné. Nous proposons également un algorithme de synthèse de définitions récursives de fonction de Skolem pour une formule existentielle à partir de sa preuve de validité. (Résumé d'auteur) %S Colloques et Séminaires %B CARI'96 : Colloque Africain sur la Recherche en Informatique = CARI'96 : African Conference on Research in Computer Science %8 1996/10/09-16 %$ 122INTAR