Formal Verification of Debates in Argumentation Theory
This work addresses the need for formal verification in argumentation theory, which could benefit fields like AI and law, but it appears incremental as it applies existing model checking techniques to a new domain.
The paper tackles the problem of verifying debates formalized as abstract argumentation frameworks by developing a methodology that translates debates into transition systems and formalizes properties using temporal and strategy logics, enabling automated verification with model checkers, and it measures performance to discuss feasibility.
Humans engage in informal debates on a daily basis. By expressing their opinions and ideas in an argumentative fashion, they are able to gain a deeper understanding of a given problem and in some cases, find the best possible course of actions towards resolving it. In this paper, we develop a methodology to verify debates formalised as abstract argumentation frameworks. We first present a translation from debates to transition systems. Such transition systems can model debates and represent their evolution over time using a finite set of states. We then formalise relevant debate properties using temporal and strategy logics. These formalisations, along with a debate transition system, allow us to verify whether a given debate satisfies certain properties. The verification process can be automated using model checkers. Therefore, we also measure their performance when verifying debates, and use the results to discuss the feasibility of model checking debates.