机械化推理导论
An Introduction to Mechanized Reasoning
摘要：
机械化推理使用计算机来验证证明，并帮助发现新的定理。计算机科学家已经将机械化推理应用于经济问题，但到目前为止，这项工作还没有在经济学期刊上得到适当的介绍。我们以三种方式向经济学家介绍机械化推理。首先，我们一般介绍机械化推理，描述技术和它们的成功应用。其次，我们解释了机械化推理如何被应用于经济问题，集中在两个领域，吸引了最多的关注：社会选择理论和拍卖理论。最后，我们提出了一个详细的例子，机械化推理在实践中的Vickrey的熟悉定理的第二价格拍卖的证明。
英文摘要：
Mechanized reasoning uses computers to verify proofs and to help discover new theorems. Computer scientists have applied mechanized reasoning to economic problems but -- to date -- this work has not yet been properly presented in economics journals. We introduce mechanized reasoning to economists in three ways. First, we introduce mechanized reasoning in general, describing both the techniques and their successful applications. Second, we explain how mechanized reasoning has been applied to economic problems, concentrating on the two domains that have attracted the most attention: social choice theory and auction theory. Finally, we present a detailed example of mechanized reasoning in practice by means of a proof of Vickrey's familiar theorem on second-price auctions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
