Abstract FR:

L'utilisation de l'analogie en déduction automatique a été identifiée comme un facteur important pour l'efficacité des démonstrateurs. Peu d'études ont pourtant été menées sur ce sujet. Nous proposons pour la première fois une approche capable de construire des preuves de théorèmes mais aussi des contre-exemples de formules par analogie. Dans ce but, nous procédons à une abstraction des preuves (ou contre-exemples), assimilée à un processus de généralisation. Les preuves ainsi généralisées sont de meilleures candidates à une preuve par analogie. Une forme de filtrage d'ordre supérieur constitue le noyau de la construction de nouvelles preuves. En cas d'échec, le problème peut être décomposé par abduction et des techniques de parcours de graphes. La théorie, l'implémentation et les expérimentations seront discutées