SMT-Based Encoding of Argumentation Dialogue Games
Magdalena Kacprzak , Anna Sawicka , Andrzej Zbrzezny
AbstractThe aim of this work is to explore possibilities of performing semantic verification of dialogue game argumentation protocols. To this end, we analyse a chosen dialogue system which allows for the simulation of a parent-child discourse. The system under analysis is enriched by the addition of elements of emotional reasoning. In this paper, we show only the first stage of applying the verification technique. It consists of encoding a mathematical game model as an SMT formula. Then, we compute the satisfiability of the conjunction of this formula with another formula that encodes a feature of the model. This technique can be used to verify the correctness of the protocol in the sense of it satisfying the expected properties.
|Publication size in sheets||0.5|
|Book||Rutkokowski Leszek, Korytkowski Marcin, Scherer Rafał, Tadeusiewicz Ryszard, Pedrycz Witold, Zurada Jacek M. (eds.): Artificial Intelligence and Soft Computing: 18th International Conference, ICAISC 2019: proceedings, Lecture Notes In Computer Science, vol. Part 2, no. 11509: Lecture Notes in Artificial Intelligence, 2019, Springer, ISBN 978-3-030-20914-8, [978-3-030-20915-5], 712 p., DOI:10.1007/978-3-030-20915-5|
|Keywords in English||Argumentation dialogue game, Dialogue protocol, Reachability analysis, Bounded model checking, SMT solver|
|Internal identifier||ROC 19-20|
|Score||= 20.0, 27-03-2020, ChapterFromConference|
* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.