## Abstract

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.

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 language | English |
---|---|

Title of host publication | Intelligent Computer Mathematics |

Subtitle of host publication | 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings |

Editors | J Davenport, WM Farmer, J Urban, F Rabe |

Publisher | Springer |

Pages | 58-73 |

ISBN (Electronic) | 978-3-642-22673-1 |

ISBN (Print) | 978-3-642-22672-4 |

DOIs | |

Publication status | Published - 1 Jan 2011 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

Volume | 6824 |

ISSN (Print) | 0302-9743 |