Voir la notice de l'article provenant de la source Numdam
Un système de règles grammaticales est présenté pour analyser un fragment du français permettant l'expression de théorémes et de preuves mathématiques. 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 parenthè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 grammaire, basées sur l'implémentation déclarative de la grammaire dans ALF, un éditeur de preuves.
A system of grammatical rules is presented to analyse a fragment of French that permits the expression of mathematical theorems and proofs. To this end, a version of Montague grammar is developed, with syntactic categories relativized to a context and to domains of individuals. This system can be interpreted in the constructive type theory of Martin-,Löf. It is first applied to French without mathematical symbols, paying special attention to selectional restrictions and to dependencies on context. The fragment includes verbs and adjectives, plurals, relative clauses, and coordinated phrases of different categories. Second, the grammar is extended to mathetimatical symbolism and its embedding in French text. The fragment comprises arithmetical formulae, decimal notation, parenthesis conventions, explicit variables, statements of theorems, and textual structures of proofs. Finally, some applications of the grammar are studied, based on a declarative implementation in the proof editor ALF.
@article{MSH_1997__139__5_0, author = {Ranta, Aarne}, title = {Structures grammaticales dans le fran\c{c}ais math\'ematique : {II} - (suite et fin)}, journal = {Math\'ematiques informatique et sciences humaines}, pages = {5--36}, publisher = {Ecole des hautes-\'etudes en sciences sociales}, volume = {139}, year = {1997}, mrnumber = {1600696}, zbl = {0891.03008}, language = {fr}, url = {http://geodesic.mathdoc.fr/item/MSH_1997__139__5_0/} }
TY - JOUR AU - Ranta, Aarne TI - Structures grammaticales dans le français mathématique : II - (suite et fin) JO - Mathématiques informatique et sciences humaines PY - 1997 SP - 5 EP - 36 VL - 139 PB - Ecole des hautes-études en sciences sociales UR - http://geodesic.mathdoc.fr/item/MSH_1997__139__5_0/ LA - fr ID - MSH_1997__139__5_0 ER -
%0 Journal Article %A Ranta, Aarne %T Structures grammaticales dans le français mathématique : II - (suite et fin) %J Mathématiques informatique et sciences humaines %D 1997 %P 5-36 %V 139 %I Ecole des hautes-études en sciences sociales %U http://geodesic.mathdoc.fr/item/MSH_1997__139__5_0/ %G fr %F MSH_1997__139__5_0
Ranta, Aarne. Structures grammaticales dans le français mathématique : II - (suite et fin). Mathématiques informatique et sciences humaines, Tome 139 (1997), pp. 5-36. http://geodesic.mathdoc.fr/item/MSH_1997__139__5_0/