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

This research applies methods and tools from mathematical knowledge management and theorem proving to theoretical economics, by working with a class of cooperative games called pillage games. Pillage games, introduced by Jordan in 2006, provide a formal way of thinking about the ability of powerful coalitions to take resources from less powerful ones. While their name suggests primitive, violent interactions, pillage games are more applicable to advanced democracies, in which coalitions seek to form governments to alter the distribution of society's resources in their favour. If, for some allocation of society's resources, the coalition preferring another allocation is stronger than that preferring the status quo, the other allocation `dominates' the status quo. The most conceptually intriguing, and the most computationally intractable solution concept for cooperative games is the `stable set'. A stable set, has two features: no allocation in the set dominates another; each allocation outside the set is dominated by an allocation in the set. For pillage games with three agents under a few additional conditions, we have determined when stable sets exist, that they are unique and contain no more than 15 allocations, and how to determine them for a given power function. In this research, we first formally represent the mathematical knowledge developed in Jordan's and our work using sTeX, a mathematical knowledge management tool. This allows, e.g., automatic identification of how various results depend on each other. We then use two modern automated theorem provers (ATPs), Isabelle and Theorema, to formally prove these results. Theorem proving is a hard task and if not provided with domain specific knowledge ATPs have to search through big search spaces in order to find proofs. To increase their reasoning power, we shall seek to identify recurring patterns in proofs, and extract proof tactics, reducing the interactions necessary to prove the theorems interactively. As important results in pillage games can be summarised in pseudo-algorithms, containing both computational and non-computational steps, we shall study such pseudo-algorithms, seeking to push them towards the much more efficient computational steps. Finally, we shall use the identified proof tactics to help the ATPs prove new results in order evaluate their true value. The research seeks to make a number of contributions. For theorem proving, pillage games form a new set of challenge problems. As the study of pillage games is new, and the canon of applicable knowledge small, this gives an unprecedented opportunity to encode most of it. The research will expand the tractable problem domain for ATPs; and - by identifying successful tactics - increase both the efficiency with which ATPs search for proofs, and - ideally - their ability to establish new results. For economics, this is the first major application of formal knowledge management and theorem proving techniques. The few previous applications of ATP to economics have formalised isolated results without engaging economists and have thus largely gone unnoticed by the discipline. As cooperative games are a known hard class of economic problems, and pillage games known to be tractable, this research therefore presents a strong `proof of concept' for the use of ATP within economics. Cooperative game theory is formally similar to graph theory, the techniques and insights developed may be applicable to matching problems, network economics, operations research, and combinatorial optimisation more generally. Additionally, the researchers will introduce ATP techniques to the leading PhD summer school in computational economics, and are working in collaboration with economic theorists with strong computational backgrounds. Thus, the research seeks to form a focal point for formal knowledge management and theorem proving efforts in economics.