Une bibliothèque Coq pour le traitement des langues naturelles

摘要

Cet article présente les différentes fonctionnalités de l'outil ICHARATE qui est un atelier logique basé sur l'assistant de preuves Coq et destiné à la recherche et l'enseignement de la linguistique computationnelle. Cet atelier est particulièrement dédié à la formalisation des grammaires catégorielles multimodales en Coq. Il permet de faciliter l'appréhension de ces modèles complexes en offrant aux utilisateurs la possibilité d'effectuer interactivement leurs analyses syntaxiques de phrases, d'obtenir leurs interprétations sémantiques et d'établir des propriétés génériques de classes entières de grammaires en se référant à un catalogue riche de règles dérivées. En outre, ICHARATE dispose d'une interface utilisateur conviviale qui met en oeuvre diverses techniques pour faciliter l'interaction avec les novices.%This paper presents the logical toolkit ICHARATE which is built upon a formaliza-tion of multimodal categorial grammars in Coq proof assistant. This toolkit aims at facilitating the study of these complicated formalisms by allowing users to build interactively the syntactic derivations of different sentences, compute their semantic interpretations and also prove universal properties of entire classes of grammars using a collection of already established derived rules. Moreover, ICHARATE is provided with a user-friendly interface that implements various techniques in order to ease the interaction with beginners.