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.
|