Abstract FR:

La modelisation des connaissances est un point central dans les systemes d'enseignement intelligemment assiste par ordinateur (e. I. A. O. ). En effet, l'enseignant possede non seulement les connaissances faisant l'objet de l'apprentissage, mais egalement celles, beaucoup plus etendues, qui lui permettent de juger celles de l'apprenant et de les completer en l'assistant et le corrigeant. Mentoniezh est un systeme d'e. I. A. O. De la geometrie plane, a destination des classes de college. Dans un tel systeme, l'expertise du domaine releve d'un demonstrateur automatique ou resolveur. En raison de son role dans le logiciel, ce dernier differe notablement d'un demonstrateur traditionnel. Il s'agit en effet plutot d'un developpeur de l'espace de recherche d'un probleme (au sens classique de ce terme en i. A. ) produisant l'ensemble des pas de deduction possibles et un ensemble significatif de preuves. Dans ce document, nous construisons un modele de la geometrie elementaire permettant de construire un tel developpeur, en utilisant la logique des predicats du premier ordre. Nous proposons des solutions permettant de depasser certaines limitations generalement observees sur les demonstrateurs automatiques, a savoir celles concernant la creation d'objets geometriques tels que les droites en cours de developpement et la gestion de l'egalite entre ces objets. Ce modele constitue d'une certaine facon, une reponse positive a la question : la geometrie elementaire est-elle reductible a des clauses de horn ?. Nous abordons egalement l'etude de l'ensemble des preuves d'un enonce donne, une preuve etant definie comme un ensemble de pas de deduction verifiant certaines proprietes de minimalite et definissons un outil permettant de mesurer la qualite d'une preuve. L'ensemble des resultats obtenus a fait l'objet d'une validation dans le cadre d'un demonstrateur destine a s'integrer comme module dans le systeme mentoniezh.