论抽象论证框架中稳定扩展的计算

一个抽象论证框架（简称 {\sc af}）是一个有向图 $(A,R)$，其中 $A$ 是抽象论证的集合，$R\subseteq A \times A$ 是攻击关系。设 $H=(A,R)$ 为一个 {\sc af}，$S \subseteq A$ 为论证的集合，且 $S^+ = \{y \mid \exists x\in S \text{ 且 }(x,y)\in R\}$。则 $S$ 是 $H$ 中的稳定扩展当且仅当 $S^+ = A\setminus S$。本文对一个已知的用于列举给定 {\sc af} 中所有稳定扩展的回溯算法进行了彻底的、形式化的验证。