Abstract
Dans cet article, nous présentons une utilisation des assistants des preuves pour traiter l’inférence en Language Naturel (NLI). D’ abord, nous proposons d’utiliser les theories des types modernes comme langue dans laquelle traduire la sémantique du langage naturel. Ensuite, nous implémentons cette sémantique dans l’assistant de preuve Coq pour raisonner sur ceux-ci. En particulier, nous évaluons notre proposition sur un sous-ensemble de la suite de tests FraCas, et nous montrons que 95.2% des exemples peuvent être correctement prédits. Nous discutons ensuite la question de l’automatisation et il est démontré que le langage de tactiques de Coq permet de construire des tactiques qui peuvent automatiser entièrement les preuves, au moins pour les cas qui nous intéressent.- Anthology ID:
- 2015.jeptalnrecital-court.2
- Volume:
- Actes de la 22e conférence sur le Traitement Automatique des Langues Naturelles. Articles courts
- Month:
- June
- Year:
- 2015
- Address:
- Caen, France
- Venue:
- JEP/TALN/RECITAL
- SIG:
- Publisher:
- ATALA
- Note:
- Pages:
- 7–13
- Language:
- URL:
- https://aclanthology.org/2015.jeptalnrecital-court.2
- DOI:
- Cite (ACL):
- Stergios Chatzikyriakidis. 2015. Natural Language Reasoning using Coq: Interaction and Automation. In Actes de la 22e conférence sur le Traitement Automatique des Langues Naturelles. Articles courts, pages 7–13, Caen, France. ATALA.
- Cite (Informal):
- Natural Language Reasoning using Coq: Interaction and Automation (Chatzikyriakidis, JEP/TALN/RECITAL 2015)
- PDF:
- https://preview.aclanthology.org/auto-file-uploads/2015.jeptalnrecital-court.2.pdf