Apr, 2016

利用SMT求解证明效率和策略无关的矛盾性

TL;DR本文提供了一个计算机辅助证明,指出每个有效的聚合机制都可以针对代理人的偏好进行操作,这解决了一个悬而未决的问题并加强了现有定理的几个声明,并首次将SMT解算器应用于计算社会选择。