@inproceedings{chatzikyriakidis-2015-natural,
    title = "Natural Language Reasoning using Coq: Interaction and Automation",
    author = "Chatzikyriakidis, Stergios",
    editor = "Lecarpentier, Jean-Marc  and
      Lucas, Nadine",
    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://preview.aclanthology.org/icon-24-ingestion/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."
}