VCG_Stable:Vickrey Clarke Groves拍卖算法和机制的形式化 源码

VCG(稳定可靠) 通用Vickrey-Clarke-Groves(VCG)拍卖机制和VCG for Search拍卖算法的Coq / SSReflect形式化项目,被视为通用机制的一个实例。 此外,我们提供了重要属性的证明,即无正向转移,合理性和(部分原因,因为仅限于稳定的出价变化,即,不会改变出价人顺序的出价)真实性。 有关简短介绍和说明,请参见此资料库中的MINES ParisTech / CRI技术报告,。 有关正确的说明,另请参见文件头。 用法 从VCG_Search_as_General_VCG.v文件开始,以运行整个项目。 否则,如果只想运行此General_VCG_mechanism.v ,则在General_VCG_mechanism.v文件的开头添加注释掉的Require 。 已在MacOS Catalina 10.15.7上使用以下运行环境测试了此形式化: n