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.

The project seeks impact primarily by engaging with the academic
computer science and economics communities. This will be done in
departmental seminars, workshops (e.g., UK Automated Reasoning
Workshop), tutorials (e.g., the ESSLLI summer school) and
conferences (e.g., CICM, and conferences by economics societies
such as the Society for Computational Economics). We have been
invited to present the work to the 2012 Initiative for
Computational Economics in Chicago, economics' principle training
ground in computational methods for PhD students.

Finished work will be submitted to internationally recognised
journals. Within computer science, these are journals such as the
Journal of Automated Reasoning, Artificial Intelligence, the
Journal of Applied Logic. Within economics, outlets include leading
theory journals such as the International Journal of Game Theory,
Games and Economic Behavior, Computational Economics and, for a
survey article, the Journal of Economic Literature.

Efforts will be made to communicate results to the public more
broadly, ideally through a popular science journal.

The project will also establish a website with three goals. First,
to disseminate work and results, including research reports,
encodings of the problems for various theorem provers, all code and
algorithms written. Second, the website will seek to facilitate the
growth of an ATP sub-community within economics, encouraging the
use and understanding of ATP and a search for fruitful application
domains. Initially, this will be organised around a wiki on key
theorems in economics. It will also host a discussion forum for the
discussion of approaches, problems, and solutions in formalised
economics. Finally, the website will be a key resource for formally
representing and proving knowledge related to theoretical
economics, whether by hosting material itself, or linking to it
elsewhere.

Research in mechanised theorem proving has applications beyond
academia. We shall initially explore applications formally close to
either our work or to previous work. As our work is formally similar
to matching problems, they are a natural application domain. Matching
problems include that of matching students to schools, organ donors to
recipients, and interns to hospitals.

Existing applications of mechanised theorem proving to economics have
focused on results in social choice. One of these, the
Gibbard-Satterthwaite theorem, is a central result in mechanism
design, which includes auction theory as a subfield. Auctions are now
a major method for allocating resources, whether via Google's online
ads, oil fields development, contract auctions, or procurement
auctions. Further, good design can make large differences to the
revenues generated: the top two European spectrum license auctions in
2000 earned over 30 times what the bottom one earned. Thus, mechanised
theorem proving could aid in the design of and participation in
auctions.

Another important way to achieve impact is by our internationally
leading project partners. They will not only advise us but also
actively support us in our aspiration and in the dissemination of
the results. We have an industrial advisor who will not only advise
us on the research side of the project but will also give valuable
contributions on how to apply the work outside academia. Our other
project partners are senior figures in computer science and
economics. They have strong expertise in all relevant aspects of
the project. We have leading figures who are opinion formers in
their respective fields of expertise: development of mathematical
knowledge representation formalisms, theorem proving systems,
maintaining a large collection of challenge problems on the
computer science side of the project; pillage games, rationality,
computational economics, developing software for solving
non-cooperative games on the economics side.