Formal Representation and Proof for Cooperative Games: A Foundation for Complex Social Behaviour

本研究通过研究一类称为掠夺博弈的合作博弈，将数学知识管理和定理证明的方法和工具应用于理论经济学。掠夺游戏是2006年由约旦引入的，它提供了一种思考强大联盟从弱小联盟手中夺取资源能力的正式方式。虽然掠夺游戏的名字暗示着原始的暴力互动，但它更适用于先进的民主国家，在这些国家，联盟寻求组建政府，以改变社会资源的分配，使其有利于自己。如果对于社会资源的某种分配，偏好另一种分配的联盟强于偏好现状的联盟，则另一种分配“支配”了现状。对于合作游戏来说，最吸引人的概念和最难以计算的解决方案是“稳定集”。一个稳定的集合，有两个特征：集合中没有分配支配另一个；集合外的每个分配都由集合内的分析支配。对于在一些附加条件下具有三个代理的掠夺游戏，我们已经确定了何时存在稳定集，它们是唯一的并且包含不超过15个分配，以及如何在给定的功率函数中确定它们。在本研究中，我们首先使用数学知识管理工具sTeX对Jordan和我们的工作中开发的数学知识进行形式化表示。这允许，例如，自动识别各种结果是如何相互依赖的。然后，我们使用两个现代自动定理证明器（atp）， Isabelle和theorma，来正式证明这些结果。定理证明是一项艰巨的任务，如果不提供特定领域的知识，atp必须在大的搜索空间中搜索才能找到证明。为了增加它们的推理能力，我们将寻求识别证明中重复出现的模式，并提取证明策略，减少交互证明定理所必需的交互。由于掠夺游戏中的重要结果可以用包含计算和非计算步骤的伪算法来总结，我们将研究这些伪算法，试图将它们推向更有效的计算步骤。最后，我们将使用识别证明策略来帮助atp证明新的结果，以便评估它们的真实价值。这项研究试图做出一些贡献。为了改进定理，掠夺游戏形成了一组新的挑战问题。由于掠夺游戏的研究是新的，适用的知识标准很少，这给了一个前所未有的机会来编码其中的大部分。该研究将拓展atp的可处理问题领域；并且——通过确定成功的策略——提高atp寻找证据的效率，以及——理想地——他们建立新结果的能力。对于经济学来说，这是正式知识管理和定理证明技术的第一个主要应用。以前将ATP应用于经济学的少数几次，都是将孤立的结果正式化，而没有让经济学家参与进来，因此在很大程度上被这门学科所忽视。由于合作游戏是一类已知的经济难题，而掠夺游戏则是易于处理的，因此，本研究为atp在经济学中的应用提供了强有力的“概念证明”。合作博弈论在形式上类似于图论，所开发的技术和见解可能适用于匹配问题、网络经济学、运筹学研究和更普遍的组合优化。此外，研究人员将把ATP技术引入顶尖的计算经济学博士暑期学校，并与具有强大计算背景的经济理论家合作。因此，本研究试图为经济学中的形式知识管理和定理证明工作形成一个焦点。

This research applies methods and tools from mathematical knowledgemanagement and theorem proving to theoretical economics, by workingwith a class of cooperative games called pillage games. Pillagegames, introduced by Jordan in 2006, provide a formal way ofthinking about the ability of powerful coalitions to take resourcesfrom less powerful ones. While their name suggests primitive,violent interactions, pillage games are more applicable to advanceddemocracies, in which coalitions seek to form governments to alterthe distribution of society's resources in their favour. If, forsome allocation of society's resources, the coalition preferringanother allocation is stronger than that preferring the status quo,the other allocation `dominates' the status quo.The most conceptually intriguing, and the most computationallyintractable solution concept for cooperative games is the `stableset'. A stable set, has two features: no allocation in the setdominates another; each allocation outside the set is dominated by anallocation in the set. For pillage games with three agents under a fewadditional conditions, we have determined when stable sets exist, thatthey are unique and contain no more than 15 allocations, and how todetermine them for a given power function.In this research, we first formally represent the mathematicalknowledge developed in Jordan's and our work using sTeX, amathematical knowledge management tool. This allows, e.g., automaticidentification of how various results depend on each other.We then use two modern automated theorem provers (ATPs), Isabelle andTheorema, to formally prove these results. Theorem proving is a hardtask and if not provided with domain specific knowledge ATPs have tosearch through big search spaces in order to find proofs. To increasetheir reasoning power, we shall seek to identify recurring patterns inproofs, and extract proof tactics, reducing the interactions necessaryto prove the theorems interactively. As important results in pillagegames can be summarised in pseudo-algorithms, containing bothcomputational and non-computational steps, we shall study suchpseudo-algorithms, seeking to push them towards the much moreefficient computational steps. Finally, we shall use the identifiedproof tactics to help the ATPs prove new results in order evaluatetheir true value.The research seeks to make a number of contributions. For theoremproving, pillage games form a new set of challenge problems. As thestudy of pillage games is new, and the canon of applicable knowledgesmall, this gives an unprecedented opportunity to encode most ofit. The research will expand the tractable problem domain for ATPs;and - by identifying successful tactics - increase both the efficiencywith which ATPs search for proofs, and - ideally - their ability toestablish new results.For economics, this is the first major application of formal knowledgemanagement and theorem proving techniques. The few previousapplications of ATP to economics have formalised isolated resultswithout engaging economists and have thus largely gone unnoticed bythe discipline. As cooperative games are a known hard class ofeconomic problems, and pillage games known to be tractable, thisresearch therefore presents a strong `proof of concept' for the use ofATP within economics. Cooperative game theory is formally similarto graph theory, the techniques and insights developed may beapplicable to matching problems, network economics, operationsresearch, and combinatorial optimisation more generally.Additionally, the researchers will introduce ATP techniques to theleading PhD summer school in computational economics, and are workingin collaboration with economic theorists with strong computationalbackgrounds. Thus, the research seeks to form a focal point for formalknowledge management and theorem proving efforts in economics.