文件名称：VCG_Stable:Vickrey-Clarke-Groves拍卖算法和机制的形式化
文件大小：334KB
文件格式：ZIP
更新时间：2024-05-04 04:56:07
Coq
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
【文件预览】：
VCG_Stable-main
----LICENSE(1KB)
----VCG_Search_as_General_VCG.v(67KB)
----General_VCG_mechanism.v(7KB)
----README.md(1KB)
----report.pdf(317KB)