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

Lead Research Organisation: University of Birmingham
Department Name: School of Computer Science


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.

Planned Impact

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

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

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.
Description We have developed an approach to generate provably reliable software in applications of the field of economics. We have applied the method in the area of auction design. The approach consists of formalising an auction in the formal language of the Isabelle theorem prover, proving its properties within the system and using the code extraction mechanism to generate the code automatically.
Exploitation Route Up to now the approach has been used to give a proof of principle. The next step will be to apply it to one (or some) of the most recently developed auction schemas.
Sectors Creative Economy,Retail,Other

Description We have actively approached economists and have found interest there, but up to now the results have not been used (to our knowledge). We put further efforts into the application in the auction domain. We have continued applying formal methods developed in the project to other domains. We (the two investigators) have founded a company and try to offer services on applying formal verification in finance, in particular, by proving formal properties of risk analysis.
First Year Of Impact 2017
Sector Financial Services, and Management Consultancy
Impact Types Economic

Title Auction Theory Toolbox (ATT) 
Description We have used different languages for the formalisation of Auctions. For details, see 
Type Of Technology Software 
Year Produced 2012 
Open Source License? Yes  
Impact Building on the implementation it is much easier to formalise and implement other auction schemas. 
Description An economist's guide to mechanized reasoning or My computer just proved 84 impossibility theorems 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? Yes
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Invited lecture at the Summer School of the Initiative for Computational Economics, 2012 in Chicago, USA. We gave an overview of the potential of applying formal methods to economics from an economics perspective.

We have been in touch with a number of economists who showed interest in our work. This is essential for our project, since we want to show the usefulness of formal systems in economics.
Year(s) Of Engagement Activity 2012
Description Departmental Seminar 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Other academic audiences (collaborators, peers etc.)
Results and Impact Application of different theorem proving systems

Exchange of ideas
Year(s) Of Engagement Activity 2015
Description Formalising "100" Theorems/Models/Theories in Economics 
Form Of Engagement Activity A magazine, newsletter or online publication
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact This page attempts to do for theorems in economics what Freek Wiedijk's page does for mathematical theorems more generally. It inherits the same caveats, as well as adopting a dynamic definition of 100.

This has not yet attracted major attention to our knowledge.
Year(s) Of Engagement Activity 2012
Description Invited Talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Policymakers/politicians
Results and Impact Discussion on Electricity Auctions
Year(s) Of Engagement Activity 2013
Description Seminar at the Technical University of Munich, Isabelle Group 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact Presentation of a seminar and discussion on the application of the Isabelle system for the verification of auctions.
Year(s) Of Engagement Activity 2016