Contenu du sommaire

Un système de règles grammaticales est présenté pour analyser un ragment du français permettant l'expression de théorèmes et de preuves mathéma-tiques. Pour cet objectif, on développe une version de la grammaire de Montague, avec des catégories syntaxiques relatives au contexte et aux domaines d'individus. Ce système peut être interprété dans la théorie constructive des types de Martin-Löf. Il est appliqué, d'abord, au français sans symboles mathématiques, avec une attention spéciale aux restrictions de sélection et aux dépendances par rapport à un contexte. Le fragment comprend des verbes et des adjectifs, des formes plurielles, des propositions relatives, et des syntagmes coordonnés. Ensuite, la grammaire est étendue au symbolisme mathématique et à son usage dans le texte français. Le fragment comprend des formules arithmétiques, la notation décimale, les conventions de paren-thèses, les variables explicites, des énoncés de théorèmes et des structures textuelles de preuves. On finit par étudier quelques applications de la gram-maire, basées sur l'implémentation déclarative de la grammaire dans ALF, un éditeur de preuves.

Nous nous intéressons à l'apprentissage à partir d'exemples et à la résolution de problème dans un univers évolutif représenté par une base de con-naissances incomplète. Nous formalisons un cadre de représentation de connaissances susceptible d'être élaboré et critiqué par des humains comme par des machines. Cette représentation des connaissances est appelée théorie semi-empirique car cette forme de théorie n'est pas complètement axiomatique. Nous avons formalisé la gestion de la croissance incrémentale de la connaissance dans notre système autour de l'idée de noyau central, issue des recherches en psychologie sociale, en définissant un sous-ensemble cohérent de la base de connaissances comme le concept à apprendre, et en obligeant l'apprenti à persévérer dans cette croyance. La pro-priété essentielle de ce sous-ensemble est la mono-tonie du raisonnement.