SMT-Based Encoding of Argumentation Dialogue Games

Magdalena Kacprzak , Anna Sawicka , Andrzej Zbrzezny


The 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.
Author Magdalena Kacprzak (FCS / DTCS)
Magdalena Kacprzak,,
- Department of Theoretical Computer Science
, Anna Sawicka
Anna Sawicka,,
, Andrzej Zbrzezny
Andrzej Zbrzezny,,
Publication size in sheets0.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 EnglishArgumentation dialogue game, Dialogue protocol, Reachability analysis, Bounded model checking, SMT solver
Internal identifierROC 19-20
Languageen angielski
Score (nominal)20
Score sourceconferenceList
ScoreMinisterial score = 20.0, 27-03-2020, ChapterFromConference
Citation count*
Share Share

Get link to the record

* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.
Are you sure?