摘要：Cet article propose une formalisation de la gestion de dialogue via la recherche de preuves de formules de la logique linéaire. C’est-à-dire que nous proposons que la logique linéaire constitue une base naturelle de la formalisation de systèmes de gestion de dialogue basé sur un état d’information. Nous prêtons une attention particulière à la modélisation des séquences de questions-réponses (y compris les demandes de clarification), et nous arguons que les métavariables, résultant des unifications issue de la recherche de preuves, jouent un rôle décisif dans la formalisation. Nous montrons que notre système est non seulement adéquat d’un point de vue théorique, mais également d’un point de vue pratique. Ainsi, nous complétons notre argument d’une implementation d’un système de recherche de preuve générique, ainsi que d’un exemple de gestion de dialogue l’utilisant.
其他摘要：In this paper, we study the formalisation of a dialogue management system using proof-search on top of a linear logic. We argue that linear logic is the natural formalism to implement information-state dialogue management. We give particular attention to modelling question-answering sequences, including clarification requests, and argue that metavariables, arising from unification in the proof search, play a decisive role in providing a natural formalisation. We show that our framework is not only well suited from a theoretical perspective, but it is also suitable for implementation which we exemplify with a small scale implementation.
