EPSRC logo

Details of Grant 

EPSRC Reference: EP/J007498/1
Title: Formal Representation and Proof for Cooperative Games: A Foundation for Complex Social Behaviour
Principal Investigator: Kerber, Dr M
Other Investigators:
Rowat, Dr C
Researcher Co-Investigators:
Project Partners:
Department: School of Computer Science
Organisation: University of Birmingham
Scheme: Standard Research
Starts: 01 May 2012 Ends: 30 April 2015 Value (£): 389,557
EPSRC Research Topic Classifications:
Artificial Intelligence Economics
Fundamentals of Computing Mathematical Aspects of OR
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
06 Sep 2011 EPSRC ICT Responsive Mode - Sep 2011 Announced
Summary on Grant Application Form
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.

Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.bham.ac.uk