Formal Verification of Debates in Argumentation Theory

TL;DR

This paper introduces a formal methodology for verifying debates modeled as abstract argumentation frameworks using transition systems and temporal logic, enabling automated model checking of debate properties.

Contribution

It presents a novel translation from debates to transition systems and formalizes debate properties for automated verification, advancing the analysis of argumentative discussions.

Findings

Model checking debates is feasible with current tools.

The translation enables formal analysis of debate evolution.

Performance metrics show practical applicability.

Abstract

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.