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

点击翻译按钮获取中文摘要

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.