MVArg

新多赢家投票系统MVArg引入形式化验证

研究人员引入了一种名为MVArg的新型多赢家投票系统，该系统允许选民使用论证式选票表达对候选人的可否认偏好。该系统比使用赞成式选票的现有多种获胜者投票方法更具表现力。该研究确立了关键的理论属性，包括选民凝聚力和正当代表性公理的保守推广，并表明虽然JR的MVArg对应项总是可以满足，但PJR和EJR却不能总是满足。JR满足的验证是coNP-hard的，但可以在多项式时间内构建获胜者集合，并且所有形式化都已在Lean 4中进行了机械检查。