Blast、Simp 和 Rule 对 Vickrey 定理的正式证明-研究论文

正式方法使用计算机来验证证明甚至发现新定理。 在过去的十年中，人们对将形式方法应用于经济学问题的兴趣增加了，但是 - 迄今为止 - 这些工作还没有发表在经济学期刊上。 本文将形式方法应用于熟悉的环境 - Vickrey 关于第二价格拍卖的定理 - 并作为背景提供了形式方法的介绍。