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

本研究通过研究一类称为掠夺博弈的合作博弈，将数学知识管理、定理证明等方法和工具应用于理论经济学。由约旦于2006年推出的Pillagegars提供了一种正式的方式来思考强大的联盟从实力较弱的联盟那里获取资源的能力。尽管它们的名字让人联想到原始的、暴力的互动，但掠夺游戏更适用于先进的民主国家，在这些国家中，联盟寻求组建政府，以改变社会资源的分配，使之有利于自己。对于社会资源的某种分配，如果联盟倾向于另一种分配比倾向于现状的联盟更强，那么另一种分配“主导”现状。合作博弈中最耐人寻味、最难计算的解概念是“稳定集”。一个稳定的集合有两个特征：集合中没有分配支配另一个分配；集合外的每一个分配都由集合中的一个分配支配。对于具有三个代理的掠夺博弈，在几个附加条件下，我们确定了稳定集何时存在，它们是唯一的，包含不超过15个分配，以及如何确定它们对于给定的幂函数。在本研究中，我们首先使用数学知识管理工具STEX来形式化地表示Jordan和我们的工作中发展的数学知识。然后，我们使用两个现代自动定理证明器(ATP)，Isabelle和Theorema，来形式化地证明这些结果。定理证明是一项艰巨的任务，如果没有特定领域的知识，则自动测试程序必须在大的搜索空间中搜索才能找到证明。为了提高他们的推理能力，我们将寻求识别证明中的递归模式，并提取证明策略，减少交互式证明定理所需的交互。由于博弈论中的重要结果可以概括为伪算法，包括计算步骤和非计算步骤，我们将研究这种伪算法，试图将它们推向更有效的计算步骤。最后，我们将使用身份证明策略来帮助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.