Sebastian Haufe

Automated Theorem Proving for General Game Playing

Dokumente und Dateien


Bitte nutzen Sie beim Zitieren immer folgende Url:

Kurzfassung in Englisch

While automated game playing systems like Deep Blue perform excellent within their domain, handling a different game or even a slight change of rules is impossible without intervention of the programmer. Considered a great challenge for Artificial Intelligence, General Game Playing is concerned with the development of techniques that enable computer programs to play arbitrary, possibly unknown n-player games given nothing but the game rules in a tailor-made description language. A key to success in this endeavour is the ability to reliably extract hidden game-specific features from a given game description automatically. An informed general game player can efficiently play a game by exploiting structural game properties to choose the currently most appropriate algorithm, to construct a suited heuristic, or to apply techniques that reduce the search space. In addition, an automated method for property extraction can provide valuable assistance for the discovery of specification bugs during game design by providing information about the mechanics of the currently specified game description. The recent extension of the description language to games with incomplete information and elements of chance further induces the need for the detection of game properties involving player knowledge in several stages of the game.

In this thesis, we develop a formal proof method for the automatic acquisition of rich game-specific invariance properties. To this end, we first introduce a simple yet expressive property description language to address knowledge-free game properties which may involve arbitrary finite sequences of successive game states. We specify a semantic based on state transition systems over the Game Description Language, and develop a provably correct formal theory which allows to show the validity of game properties with respect to their semantic across all reachable game states. Our proof theory does not require to visit every single reachable state. Instead, it applies an induction principle on the game rules based on the generation of answer set programs, allowing to apply any off-the-shelf answer set solver to practically verify invariance properties even in complex games whose state space cannot totally be explored. To account for the recent extension of the description language to games with incomplete information and elements of chance, we correctly extend our induction method to properties involving player knowledge. With an extensive evaluation we show its practical applicability even in complex games.

weitere Metadaten

Künstliche Intelligenz, Generelle Spieleprogramme, Automatisches Theorembeweisen, Antwortmengenprogrammierung, Wissensrepräsentation
Artificial Intelligence, General Game Playing, Automated Theorem Proving, Answer Set Programming, Knowledge Representation
DDC Klassifikation004
RVK KlassifikationST 300, ST 324
HochschuleTechnische Universität Dresden
FakultätFakultät Informatik
ProfessurComputational Logic
BetreuerProf. Dr. rer. nat. habil. Michael Thielscher
GutachterProf. Dr. rer. nat. habil. Michael Thielscher
Prof. Dr. rer. nat. habil. Torsten Schaub
Tag d. Einreichung (bei der Fakultät)24.11.2011
Tag d. Verteidigung / Kolloquiums / Prüfung22.06.2012
Veröffentlichungsdatum (online)10.07.2012
persistente URNurn:nbn:de:bsz:14-qucosa-89998

Hinweis zum Urheberrecht

Diese Website ist eine Installation von Qucosa - Quality Content of Saxony!
Sächsische Landesbibliothek Staats- und Universitätsbibliothek Dresden