Abstract FR:

La demonstration automatique de theoremes peut etre consideree comme une activite de resolution de problemes: atteindre un etat final e#f (la propriete a demontrer) a partir d'un etat initial e#i (les hypotheses du theoreme a demontrer). Les deux principales strategies utilisees en resolution de problemes correspondent respectivement a un raisonnement par synthese (raisonnement en avant) et a un raisonnement par analyse (raisonnement a partir du but). Nous avons realise un systeme (ubl) qui alterne ces deux strategies au cours d'une meme resolution. Les difficultes se situent dans les choix des theoremes a appliquer ou dans les choix des sous-buts a poser. Faire de bons choix est crucial dans des domaines ou il existe un grand nombre d'applications differentes des operateurs a chaque etat. C'est le cas d'un des domaines etudies dans ubl: la geometrie elementaire. Afin d'ameliorer ses capacites de choix, notre systeme apprend deux types de connaissances en analysant ses propres solutions. Il construit de nouveaux theoremes correspondant a des situations prototypiques, ce qui lui permettra de deduire plus rapidement des faits importants dans d'autres exercices. Il memorise des methodes de resolution adaptees a un but donne. Celles-ci consistent a proposer un ensemble de sous-buts qui se sont averes utiles pour la resolution de l'exercice analyse. L'utilisateur peut aider le systeme lors de la resolution, les methodes alors apprises permettent au systeme de resoudre des exercices qu'il ne savait pas traiter avant apprentissage