Cette thèse est consacrée à la théorie des modèles des groupes abéliens valués. Nousdonnons à la fin du premier chapitre un exemple assez simple montrant qu’au contrairedes groupes abéliens ordonnés, les groupes abéliens valués ne sont pas tous dépendants(NIP). La question de la propriété d’indépendance est d’ailleurs au coeur du manuscrit.Nous travaillons dans un langage à deux sortes constitué de symboles pour : la loi de groupe,le symétrique et l’élément neutre (sorte du groupe), l’ordre sur la chaîne et l’infini (sortede la chaîne de valuation) et enfin la valuation elle-même. La première partie (chapitres 2,3 et 4) traite le cas du groupe additif Z des entiers relatifs muni d’une valuation p-adique(avec p premier) et de la théorie commune à ces structures. Dans chaque cas, on obtientune axiomatisation et une élimination des quanteurs dans un langage un peu enrichi, lecaractère NIP est démontré et une étude succincte des types définissables est proposée.La deuxième partie commence par le seul chapitre généraliste du texte, où l’on adapte lapp-élimination des quantificateurs dans les modules au cadre des groupes abéliens valués.Le chapitre 6 s’intéresse aux groupes valués à chaîne finie construits sur Z : on y axiomatiseleur théorie commune et les complétions de celle-ci, pour lesquelles on donne également uneélimination des quanteurs. Enfin, le chapitre 7 s’appuie sur les résultats des chapitres 5 et 6pour fournir une élimination des quantificateurs dans le cas d’un groupe valué quelconqueconstruit sur Z et pour en déduire le caractère NIP. / The purpose of this thesis is to study model theory of abelian valued groups. At theend of the first chapter, a basic example is given, showing that, in sharp contrast to orderedabelian groups, abelian valued groups may not be dependent (NIP). The topic of IndependenceProperty is focused on throughout the manuscript. The language used is two-sortedand contains symbols for : the group operation, the inverse and the identity element (sortof the group), the order on the chain and the infinity (sort of the value chain) and finallythe valuation itself. The first part (chapters 2, 3 and 4) deals with the case of the additivegroup Z of integers endowed with a p-adic valuation (with p a prime number) and withthe common theory to these structures. In each case, an axiomatization and a quantifierelimination in a language a bit larger are obtained, the lack of the Independence Propertyis proven and a short study of definable types is propounded. The second part begins withthe only general chapter of the work, where the pp-elimination of quantifiers for modules isadapted to the framework of valued abelian groups. The chapter 6 aims at studying valuedgroups with finite chains, with Z as the underlying group : their common theory and itscompletions, for which a quantifier elimination result is also given, are axiomatized. Finally,the chapter 7, based upon the results of chapters 5 and 6, gives a quantifier eliminationfor any valued group having Z as the underlying group and deduces from this the fact thatthese valued groups are NIP.

This dissertation deals with aspects of axiomatization, intuition and visualization in thehistory of mathematics. Particular focus is put on the end of the 19th century, before DavidHilbert's (1862–1943) work on the axiomatization of Euclidean geometry. The thesis consistsof three papers. In the first paper the Swedish mathematician Torsten Brodén (1857–1931)and his work on the foundations of Euclidean geometry from 1890 and 1912, is studied. Athorough analysis of his foundational work is made as well as an investigation into his generalview on science and mathematics. Furthermore, his thoughts on geometry and its nature andwhat consequences his view has for how he proceeds in developing the axiomatic system, isstudied. In the second paper different aspects of visualizations in mathematics areinvestigated. In particular, it is argued that the meaning of a visualization is not revealed bythe visualization and that a visualization can be problematic to a person if this person, due to alimited knowledge or limited experience, has a simplified view of what the picture represents.A historical study considers the discussion on the role of intuition in mathematics whichfollowed in the wake of Karl Weierstrass' (1815–1897) construction of a nowheredifferentiable function in 1872. In the third paper certain aspects of the thinking of the twoscientists Felix Klein (1849–1925) and Heinrich Hertz (1857–1894) are studied. It isinvestigated how Klein and Hertz related to the idea of naïve images and visual thinkingshortly before the development of modern axiomatics. Klein in several of his writingsemphasized his belief that intuition plays an important part in mathematics. Hertz argued thatwe form images in our mind when we experience the world, but these images may containelements that do not exist in nature.

A spatial logic is any formal language with geometric interpretation. Research on region-based spatial logics, where variables are set to range over certain subsets of geometric space, have been investigated recently within the qualitative spatial reasoning paradigm in AI. We axiomatised the theory of (ROQ(R 2), conv, ≤) , where ROQ(R 2) is the set of regular open rational polygons of the real plane; conv is the convexity property and ≤ is the inclusion relation. We proved soundness and completeness theorems. We also proved several expressiveness results. Additionally, we provide a historical and philosophical overview of the topic and present contemporary results relating to affine spatial logics.

This dissertation deals with aspects of axiomatization, intuition and visualization in the history of mathematics. Particular focus is put on the end of the 19th century, before David Hilbert's (1862–1943) work on the axiomatization of Euclidean geometry. The thesis consists of three papers. In the first paper the Swedish mathematician Torsten Brodén (1857–1931) and his work on the foundations of Euclidean geometry from 1890 and 1912, is studied. A thorough analysis of his foundational work is made as well as an investigation into his general view on science and mathematics. Furthermore, his thoughts on geometry and its nature and what consequences his view has for how he proceeds in developing the axiomatic system, is studied. In the second paper different aspects of visualizations in mathematics are investigated. In particular, it is argued that the meaning of a visualization is not revealed by the visualization and that a visualization can be problematic to a person if this person, due to a limited knowledge or limited experience, has a simplified view of what the picture represents. A historical study considers the discussion on the role of intuition in mathematics which followed in the wake of Karl Weierstrass' (1815–1897) construction of a nowhere differentiable function in 1872. In the third paper certain aspects of the thinking of the two scientists Felix Klein (1849–1925) and Heinrich Hertz (1857–1894) are studied. It is investigated how Klein and Hertz related to the idea of naïve images and visual thinking shortly before the development of modern axiomatics. Klein in several of his writings emphasized his belief that intuition plays an important part in mathematics. Hertz argued that we form images in our mind when we experience the world, but these images may contain elements that do not exist in nature.

Το θέμα στην ουσία αφορά την Αξιωματική θεμελίωση του Ευκλείδη (καθ'ύλη αξιωματική) που έχει ως αντικείμενο την μελέτη της γεωμετρίας του φυσικού χώρου, και επομένως διατηρεί τον εμπειρικό της χαρακτήρα. Επομένως ο φυσικός αυτός χώρος εφοδιάζει τον μελετητή και με μια ισχυρή γεωμετρική διαίσθηση. Από την άλλη μεριά η αφηρημένη αξιωματική του Hilbert, και η σχετική θεμελίωση της Γεωμετρίας, καταφέρνει να εξοβελίσει την γεωμετρική διαίσθηση. Από κει και πέρα η αλγεβροποίηση των μαθηματικών, εξοβελίζει και αυτή την γεωμετρική άποψη. / We present the axiomatic method of Euclid's elements in geometry (~300 B.C.) and the axiomatization of Euclid's geometry later (first quarter of the twentieth century) by Hilbert and Tarski (formalization).

Les solveurs SMT sont des outils dédiés à la vérification d'un ensemble de formules mathématiques, en général sans quantificateurs, utilisant un certain nombre de théories prédéfinies, telles que la congruence, l'arithmétique linéaire sur les entiers, les rationnels ou les réels, les tableaux de bits ou les tableaux. Ajouter une nouvelle théorie à un solveur SMT nécessite en général une connaissance assez profonde du fonctionnement interne du solveur, et, de ce fait, ne peut en général être exécutée que par ses développeurs. Pour de nombreuses théories, il est également possible de fournir une axiomatisation finie en logique du premier ordre. Toutefois, si les solveurs SMT sont généralement complets et efficaces sur des problèmes sans quantificateurs, ils deviennent imprévisibles en logique du premier ordre. Par conséquent, cette approche ne peut pas être utilisée pour fournir une procédure de décision pour ces théories. Dans cette thèse, nous proposons un cadre d'application permettant de résoudre ce problème en utilisant des déclencheurs. Les déclencheurs sont des annotations permettant de spécifier la forme des termes avec lesquels un quantificateur doit être instancié pour obtenir des instances utiles pour la preuve. Ces annotations sont utilisées par la majorité des solveurs SMT supportant les quantificateurs et font partie du format SMT-LIB v2. Dans notre cadre d'application, l'utilisateur fournit une axiomatisation en logique du premier ordre de sa théorie, ainsi qu'une démonstration de sa correction, de sa complétude et de sa terminaison, et obtient en retour un solveur correct, complet et qui termine pour sa théorie. Dans cette thèse, nous décrivons comment un solveur SMT peut être étendu à notre cadre nous basant sur l'algorithme DPLL modulo théories, utilisé traditionnellement pour modéliser ls solveurs SMT. Nous prouvons également que notre extension a bien les propriétés attendues. L'effort à fournir pour implémenter cette extension dans un solveur SMT existant ne doit être effectué qu'une fois et le mécanisme peut ensuite être utilisé sur de multiples théories axiomatisées. De plus, nous pensons que, en général, cette implémentation n'est pas plus compliquée que l'ajout d'une unique théorie au solveur. Nous avons fait ce travail pour le solveur SMT Alt-Ergo, nous en présentons certains détails dans la thèse. Pour valider l'utilisabilité de notre cadre d'application, nous avons prouvé la complétude et la terminaison de plusieurs axiomatizations, dont une pour les listes impératives doublement chaînée, une pour les ensembles applicatifs et une pour les vecteurs de Ada. Nous avons ensuite utilisé notre implémentation dans Alt-Ergo pour discuter de l’efficacité de notre système dans différents cas. / SMT solvers are efficient tools to decide the satisfiability of ground formulas, including a number of built-in theories such as congruence, linear arithmetic, arrays, and bit-vectors. Adding a theory to that list requires delving into the implementation details of a given SMT solver, and is done mainly by the developers of the solver itself. For many useful theories, one can alternatively provide a first-order axiomatization. However, in the presence of quantifiers, SMT solvers are incomplete and exhibit unpredictable behavior. Consequently, this approach can not provide us with a complete and terminating treatment of the theory of interest. In this thesis, we propose a framework to solve this problem, based on the notion of instantiation patterns, also known as triggers. Triggers are annotations that suggest instances which are more likely to be useful in proof search. They are implemented in all SMT solvers that handle first-order logic and are included in the SMT-LIB format. In our framework, the user provides a theory axiomatization with triggers, along with a proof of completeness and termination properties of this axiomatization, and obtains a sound, complete, and terminating solver for her theory in return. We describe and prove a corresponding extension of the traditional Abstract DPLL Modulo Theory framework. Implementing this mechanism in a given SMT solver requires a one-time development effort. We believe that this effort is not greater than that of adding a single decision procedure to the same SMT solver. We have implemented the proposed extension in the Alt-Ergo prover and we discuss some implementation details in the thesis. To show that our framework can handle complex theories, we prove completeness and termination of three axiomatization, one for doubly-linked lists, one for applicative sets, and one for Ada's vectors. Our tests show that, when the theory is heavily used, our approach results in a better performance of the solver on goals that stem from the verification of programs manipulating these data-structures.

Cette thèse est consacrée à l'étude d'un point de vue modèle théorique de corps valués algébriquement clos enrichis d'un prédicat qui représente soit un sous-groupe multiplicatif soit un sous-corps. Nous donnons un résultat d'élimination partielle des quantificateurs pour les structures du type (M , G), où M est un corps valué algébriquement clos et où G un sous-groupe multiplicatif sur lequel la valuation est injective... / This thesis is dedicated to the model theoretic study of algebraically closed valued fields equipped with a additional unary predicate for either a multiplicative subgroup or a subfield.We give a result of relative quantifier elimination for structures of the kind (M , G), where M is an algebraically closed valued field and G is a multiplicative subgroup on wich the valuation is injective...

No description available.

Cette Thèse pose la question de la décision collective sous incertitude possibiliste. On propose différents règles de décision collective qualitative et on montre que dans un contexte possibiliste, l'utilisation d'une fonction d'agrégation collective pessimiste égalitariste ne souffre pas du problème du Timing Effect. On étend ensuite les travaux de Dubois et Prade (1995, 1998) relatifs à l'axiomatisation des règles de décision qualitatives (l'utilité pessimiste) au cadre de décision collective et montre que si la décision collective comme les décisions individuelles satisfont les axiomes de Dubois et Prade ainsi que certains axiomes relatifs à la décision collective, particulièrement l'axiome de Pareto unanimité, alors l'agrégation collective égalitariste s'impose. Le tableau est ensuite complété par une axiomatisation d'un pendant optimiste de cette règle de décision collective. Le système axiomatique que nous avons développé peut être vu comme un pendant ordinal du théorème de Harsanyi (1955). Ce résultat á été démontré selon un formalisme qui et basé sur le modèle de de Von NeuMann and Morgenstern (1948) et permet de comparer des loteries possibilistes. Par ailleurs, on propose une première tentative pour la caractérisation des règles de décision collectives qualitatives selon le formalisme de Savage (1972) qui offre une représentation des décisions par des actes au lieu des loteries. De point de vue algorithmique, on considère l'optimisation des stratégies dans les arbres de décision possibilistes en utilisant les critères de décision caractérisés dans la première partie de ce travail. On offre une adaptation de l'algorithme de Programmation Dynamique pour les critères monotones et on propose un algorithme de Programmation Multi-dynamique et un algorithme de Branch and Bound pour les critères qui ne satisfont pas la monotonie. Finalement, on établit une comparaison empirique des différents algorithmes proposés. On mesure les CPU temps d'exécution qui augmentent linéairement en fonction de la taille de l'arbre mais restent abordable même pour des grands arbres. Ensuite, nous étudions le pourcentage d'exactitude de l'approximation des algorithmes exacts par Programmation Dynamique: Il apparaît que pour le critère U-max ante l'approximation de l'algorithme de Programmation Multi-dynamique n'est pas bonne. Mais, ceci n'est pas si dramatique puisque cet algorithme est polynomial (et efficace dans la pratique). Cependant, pour la règle U+min ante l'approximation par Programmation Dynamique est bonne et on peut dire qu'il devrait être possible d'éviter une énumération complète par Branch and Bound pour obtenir les stratégies optimales. / This Thesis raises the question of collective decision making under possibilistic uncertainty. We propose several collective qualitative decision rules and show that in the context of a possibilistic representation of uncertainty, the use of an egalitarian pessimistic collective utility function allows us to get rid of the Timing Effect. Making a step further, we prove that if both the agents' preferences and the collective ranking of the decisions satisfy Dubois and Prade's axioms (1995, 1998) and some additional axioms relative to collective choice, in particular Pareto unanimity, then the egalitarian collective aggregation is compulsory. The picture is then completed by the proposition and the characterization of an optimistic counterpart of this pessimistic decision rule. Our axiomatic system can be seen as an ordinal counterpart of Harsanyi's theorem (1955). We prove this result in a formalism that is based on Von NeuMann and Morgenstern framework (1948) and compares possibilisitc lotteries. Besides, we propose a first attempt to provide a characterization of collective qualitative decision rules in Savage's formalism; where decisions are represented by acts rather than by lotteries. From an algorithmic standpoint, we consider strategy optimization in possibilistic decision trees using the decision rules characterized in the first part of this work. So, we provide an adaptation of the Dynamic Programming algorithm for criteria that satisfy the property of monotonicity and propose a Multi-Dynamic programming and a Branch and Bound algorithm for those that are not monotonic. Finally, we provide an empirical comparison of the different algorithms proposed. We measure the execution CPU times that increases linearly according to the size of the tree and it remains affordable in average even for big trees. Then, we study the accuracy percentage of the approximation of the pertinent exact algorithms by Dynamic Programming: It appears that for U-max ante criterion the approximation of Multi-dynamic programming is not so good. Yet, this is not so dramatic since this algorithm is polynomial (and efficient in practice). However, for U+min ante decision rule the approximation by Dynamic Programming is good and we can say that it should be possible to avoid a full Branch and Bound enumeration to find optimal strategies.

Cette thèse traite de la theorie de la preuve pour les logiques a points fixes, telles que le μ-calcul, lalogique lineaire a points fixes, etc. ces logiques sont souvent munies de systèmes de preuves finitairesavec des règles d’induction à la Park. Il existe néanmoins d’autres sytèmes de preuves pour leslogiques à points fixes, qui reposent sur la notion de preuve infinitaire, mais qui sont beaucoupmoins developpés dans la litterature. L’objectif de cette thèse est de pallier à cette lacune dansl’état de l’art, en developpant la théorie de la preuve infnitaire pour les logiques a points fixes,avec deux domaines d’application en vue: les langages de programmation avec types de données(co)inductifs et la vérification des systèmes réactifs.Cette thèse contient trois partie. Dans la première, on rappelle les deux principales approchespour obtenir des systèmes de preuves pour les logiques à points fixes: les systèmes finitaires avecrègle explicite d’induction et les systèmes finitaires, puis on montre comment les deux approchesse relient. Dans la deuxième partie, on argumente que les preuves infinitaires ont effectivement unréel statut preuve-theorique, en montrant que la logique lineaire additive multiplicative avec pointsfixes admet les propriétés d’élimination des coupures et de focalisation. Dans la troisième partie,on utilise nos developpements sur les preuves infinitaires pour monter de manière constructive lacomplétude du μ-calcul lineaire relativement à l’axiomatisation de Kozen. / The subject of this thesis is the proof theory of logics with fixed points, such as the μ-calculus,linear-logic with fixed points, etc. These logics are usually equipped with finitary deductive systemsthat rely on Park’s rules for induction. other proof systems for these logics exist, which relyon infinitary proofs, but they are much less developped. This thesis contributes to reduce thisdeficiency by developing the infinitary proof-theory of logics with fixed points, with two domainsof application in mind: programming languages with (co)inductive data types and verification ofreactive systems.This thesis contains three parts. In the first part, we recall the two main approaches to theproof theory for logics with fixed points: the finitary and the infinitary one, then we show theirrelationships. In the second part, we argue that infinitary proofs have a true proof-theoreticalstatus by showing that the multiplicative additive linear-logic with fixed points admits focalizationand cut-elimination. In the third part, we apply our proof-theoretical investigations to obtain aconstructive proof of completeness for the linear-time μ-calculus w.r.t. Kozen’s axiomatization.