Bengeloune I. (1996). Induction and synthesis by simplification. In :
Moukeli P. (ed.). 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. Paris : ORSTOM, p. 545-559. (Colloques et Séminaires). CARI'96 : Colloque Africain sur la Recherche en Informatique = CARI'96 : African Conference on Research in Computer Science, 3., Libreville (GAB), 1996/10/09-16. ISBN 2-7099-1333-X. ISSN 0767-2896.
Titre du document
Induction and synthesis by simplification
Année de publication
1996
Type de document
Partie d'ouvrage
Auteurs
Bengeloune I.
In
Moukeli P. (ed.), 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
Source
Paris : ORSTOM, 1996,
p. 545-559 (Colloques et Séminaires). ISBN 2-7099-1333-X ISSN 0767-2896
Colloque
CARI'96 : Colloque Africain sur la Recherche en Informatique = CARI'96 : African Conference on Research in Computer Science, 3., Libreville (GAB), 1996/10/09-16
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)
