Zugl.: Berlin, Techn. Univ., Diss., 2009

Le thème principal de ce travail de thèse est de montrer l’interaction existant entre les jeux et les mathématiques au travers d’une catégorie de jeux bien particuliers : les jeux combinatoires. Ces jeux se font sans hasard, sans information cachée et pour chacun des deux joueurs il existe une façon optimale de jouer. Les premiers exemples rencontrés se trouvent dans des écrits de la Renaissance. Les jeux se diffusent aux 17ème et 18ème siècles dans le cadre des récréations mathématiques, genre littéraire et éditorial nouveau qui propose une pratique ludique des sciences fondée sur le défi à l’entendement. L’analyse des jeux combinatoires intéresse ensuite les mathématiciens du début du 20ème siècle, notamment pour les jeux de type Nim. La thèse s’attache à retracer le développement de la théorie mathématique qui se construit autour des jeux combinatoires et aboutit au corps des nombres surréels de John Conway en 1976. En parallèle, elle montre qu’un autre résultat fondamental, attribué à Zermelo (1912), sur la détermination du jeu d’Échecs permet aux jeux combinatoires de s’implanter sur un plan technologique et culturel. Nous voyons les premières machines électromécaniques destinées à jouer au Nim apparaître vers 1940 et se confronter au public lors d’expositions et de salons scientifiques. La naissance des ordinateurs dans les années 1950 ouvre de nouvelles voies pour la programmation du jeu d’Échecs, jeu combinatoire par excellence. La thèse fait revivre les moments forts, faits d’espoirs et de déceptions, qu’a traversés la recherche en programmation d’Échecs, depuis ses débuts jusqu’à la victoire du programme Deep Blue sur le champion du monde Garry Kasparov en 1997. / The main theme of this thesis is to point out the interaction between games and mathematics by means of a category of very specific games, the combinatorial games. These games are no chance games of perfect information and either player (Arthur or Bertha) can force a win, or both players can force at least a draw. The first examples of combinatorial games can be found in Renaissance works. Throughout the seventeenth and eighteenth centuries, games spread as part of recreational mathematics, a new literary and editorial genre that offered an entertaining practice of science based on a challenge to understanding. Then, the analysis of combinatorial games, especially Nim games, aroused the interest of the early-twentieth-century mathematicians. This thesis is devoted to trace the development of the mathematical theory that was formulated around combinatorial games and that led to John Conway’s Field of Surreal Numbers in 1976. In parallel, it shows that another fundamental result on Chess determination, attributed to Zermelo (1912), enabled combinatorial games to become established on a cultural and technological level. Around 1940 appeared the first electromechanical machines, designed to play Nim and to meet the challenges of the audience during scientific exhibitions. The emergence of computers during the 1950s opened new paths for programming Chess, the ultimate combinatorial game. This work brings the highlights, made of hopes and disappointments, which the Chess programming research went through, since its very beginning up to the victory for Deep Blue program over the world champion Garry Kasparov in 1997.

In this thesis we consider a few results related to the Zermelo and Extended Zermelo Model as well as outline some partial results and open problems related thereto. First we will analyze a discrete dynamical system considering under what conditions the convergence of this dynamical system predicts the outcome of the Extended Zermelo Model. In the following chapter we will focus on the Zermelo Model by giving a method for simplifying the derivation of Zermelo ratings for tournaments in terms of specific types of strongly connected components. Following this, the idea of stability of a tournament will be discussed and an upper bound will be obtained on the stability of three-team tournaments. Finally, we will conclude with some partial results related to the topics presented in the previous chapters.

Thesis (doctoral)--Universität Bonn, 1986. / Includes bibliographical references (p. 141-147).

Orientador : Luiz Paulo de Alcantara / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciencias Humanas / Made available in DSpace on 2018-07-13T23:56:02Z (GMT). No. of bitstreams: 1 Gonzales_CarlosGustavo_M.pdf: 6198402 bytes, checksum: 9b5335ba71cdb3ada914a6454eba59bc (MD5) Previous issue date: 1991 / Resumo: Não informado / Abstract: Not informed. / Mestrado / Mestre em Lógica e Filosofia da Ciência

No description available.

In dieser Arbeit möchte ich dem Wesen des Auswahlaxioms auf den Grund gehen und verstehen, inwieweit es problematisch sein könnte, es zu benutzen, aber auch wie nützlich es ist, dieses mächtige Instrument als Mathematiker zu besitzen.

The specification of enterprise information systems using formal specification languages enables the formal verification of these systems. Reasoning about the properties of a formal specification is a tedious task that can be facilitated much through the use of an automated reasoner. However, set theory is a corner stone of many formal specification languages and poses demanding challenges to automated reasoners. To this end a number of heuristics has been developed to aid the Otter theorem prover in finding short proofs for set-theoretic problems. This dissertation investigates the applicability of these heuristics to next generation theorem provers. / Computing / M.Sc. (Computer Science)

The specification of enterprise information systems using formal specification languages enables the formal verification of these systems. Reasoning about the properties of a formal specification is a tedious task that can be facilitated much through the use of an automated reasoner. However, set theory is a corner stone of many formal specification languages and poses demanding challenges to automated reasoners. To this end a number of heuristics has been developed to aid the Otter theorem prover in finding short proofs for set-theoretic problems. This dissertation investigates the applicability of these heuristics to next generation theorem provers. / Computing / M.Sc. (Computer Science)

There have been numerous studies on formal methods but little utilisation of formal methods in the commercial world. This can be attributed to many factors, such as that few specialists know how to use formal methods. Moreover, the use of mathematical notation leads to the perception that formal methods are difficult. Formal methods can be described as system design methods by which complex computer systems are built using mathematical notation and logic. Formal methods have been used in the software development world since 1940, that is to say, from the earliest stage of computer development. To date, there has been a slow adoption of formal methods, which are mostly used for mission-critical projects in, for example, the military and the aviation industry. Researchers worldwide are conducting studies on formal methods, but the research mostly deals with path planning and control and not the runtime verification of autonomous systems. The main focus of this dissertation is the question of how to increase the pace at which formal methods are adopted in the business or commercial world. As part of this dissertation, a framework was developed to facilitate the use of formal methods in the commercial world. The framework mainly focuses on education, support tools, buy-in and remuneration. The framework was validated using a case study to illustrate its practicality. This dissertation also focuses on different types of formal methods and how they are used, as well as the link between formal methods and other software development techniques. An ERP system specification is presented in both natural language (informal) and formal notation, which demonstrates how a formal specification can be derived from an informal specification using the enhanced established strategy for constructing a Z specification as a guideline. Success stories of companies that are applying formal methods in the commercial world are also presented. / School of Computing