Cette Thèse est la conclusion de trois ans de travail sur un projet nommé DemoNat. Le but de ce projet est la conception d'un système d'analyse et de vérification de démonstrations mathématiques écrites en langue naturelle.<br><br>L'architecture générale du système se décrit en 4 phases :<br>- analyse de la démonstration par des outils linguistiques ;<br>- traduction de la démonstration dans un langage restreint ;<br>- interprétation du texte traduit en un arbre de règles de déduction ;<br>- validation des règles de déduction à l'aide d'un démonstrateur automatique.<br><br>Ce projet a mobilisé des équipes de linguistes et de logiciens, les deux premières phases étant la tâche des linguistes, et les deux dernières étant la tâche des logiciens.<br><br>Cette thèse présente plus en détail ce projet et développe principalement les points suivants :<br>- définition du langage restreint et de son interprétation ;<br>- propriétés du type principal de termes d'un lambda-calcul typé avec deux flèches entrant dans le cadre d'un outil linguistique, les ACGs ;<br>- description du démonstrateur automatique.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00414773 |
| Date | 05 December 2006 |
| Creators | Patrick, Thévenon |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.002 seconds