@inproceedings{chatzikyriakidis-2015-natural,
title = "Natural Language Reasoning using Coq: Interaction and Automation",
author = "Chatzikyriakidis, Stergios",
booktitle = "Actes de la 22e conf{\'e}rence sur le Traitement Automatique des Langues Naturelles. Articles courts",
month = jun,
year = "2015",
address = "Caen, France",
publisher = "ATALA",
url = "https://aclanthology.org/2015.jeptalnrecital-court.2",
pages = "7--13",
abstract = "Dans cet article, nous pr{\'e}sentons une utilisation des assistants des preuves pour traiter l{'}inf{\'e}rence en Language Naturel (NLI). D{'} abord, nous proposons d{'}utiliser les theories des types modernes comme langue dans laquelle traduire la s{\'e}mantique du langage naturel. Ensuite, nous impl{\'e}mentons cette s{\'e}mantique dans l{'}assistant de preuve Coq pour raisonner sur ceux-ci. En particulier, nous {\'e}valuons notre proposition sur un sous-ensemble de la suite de tests FraCas, et nous montrons que 95.2{\%} des exemples peuvent {\^e}tre correctement pr{\'e}dits. Nous discutons ensuite la question de l{'}automatisation et il est d{\'e}montr{\'e} que le langage de tactiques de Coq permet de construire des tactiques qui peuvent automatiser enti{\`e}rement les preuves, au moins pour les cas qui nous int{\'e}ressent.",
}
Markdown (Informal)
[Natural Language Reasoning using Coq: Interaction and Automation](https://aclanthology.org/2015.jeptalnrecital-court.2) (Chatzikyriakidis, JEP/TALN/RECITAL 2015)
ACL