Using Theorema in the Formalization of Theoretical Economics

Manfred Kerber, Colin Rowat, W Windsteiger

Research output: Chapter in Book/Report/Conference proceedingChapter

5 Citations (Scopus)


Theoretical economics makes use of strict mathematical methods. For
instance, games as introduced by von Neumann and Morgenstern allow
for formal mathematical proofs for certain axiomatized economical
situations. Such proofs can---at least in principle---also be
carried through in formal systems such as Theorema. In this paper
we describe experiments carried through using the Theorema system
to prove theorems about a particular form of games
called pillage games. Each pillage game formalizes a particular
understanding of power. Analysis then attempts to derive the properties
of solution sets (in particular, the core and stable set), asking about
existence, uniqueness and characterization.

Concretely we use Theorema to show properties previously proved on
paper by two of the co-authors for pillage games with three agents.
Of particular interest is some pseudo-code which summarizes the
results previously shown. Since the computation involves infinite
sets the pseudo-code is in several ways
non-computational. However, in the presence of appropriate lemmas, the
pseudo-code has sufficient computational content that
Theorema can compute stable sets (which are always finite). We
have concretely demonstrated this for three different important
power functions.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publication18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings
EditorsJ Davenport, WM Farmer, J Urban, F Rabe
ISBN (Electronic)978-3-642-22673-1
ISBN (Print)978-3-642-22672-4
Publication statusPublished - 1 Jan 2011

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Using Theorema in the Formalization of Theoretical Economics'. Together they form a unique fingerprint.

Cite this