Thèses (M.A.)--Université de Sherbrooke (Canada), 1999. / Titre de l'écran-titre (visionné le 20 juin 2006). Publié aussi en version papier.

Thèse doctorat : Traitement du signal et télécommunications : Rennes 1 : 2006. / Bibliogr. p. 197-204.

Thèses (M.A.)--Université de Sherbrooke (Canada), 1997. / Titre de l'écran-titre (visionné le 20 juin 2006). Publié aussi en version papier.

Thèse (Ph. D.)--Université Laval, 2008. / Titre de l'écran-titre (visionné le 12 janvier 2009). Bibliogr.

Cette thèse a pour objet de décrire précisément le sémantisme des quantificateurs vagues du français quelques et plusieurs, et de l’allemand einig-, ein paar, etlich- et mehrer- afin d’en proposer une comparaison. Une analyse qualitative d’un corpus littéraire français nous a permis de dégager des critères de fonctionnement sémantique permettant de rapprocher et de différencier les deux quantificateurs entre eux. Ces critères de fonctionnement ont pu, pour la plupart, être appliqués ensuite aux quantificateurs de l’allemand, analysés à partir d’un corpus parallèle au corpus français. L’étude d’un second corpus allemand, journalistique, a permis de cerner des préférences d’emploi relatives à ce genre de discours. Tous ces quantificateurs vagues partagent un noyau dur de sens « petite quantité vague » et ce sont donc les sèmes et les traits potentiels secondaires qui permettent de connaître le profil sémantique propre de chacun, de comprendre leur fonctionnement et donc leurs préférences d’emploi. Dans une dernière partie nous rapprochons le fonctionnement des quantificateurs des deux langues, proposons des équivalences par contextes d’emploi et des améliorations de leur traitement lexicographique aussi bien monolingue que bilingue. / The purpose of this thesis is to describe precisely the semantics of the French vague quantifiers quelques and plusieurs, and of the German einig-, ein paar, etlich- and mehrer- in order to propose a comparison. A qualitative analysis of a French literary corpus has allowed us to extricate semantic operating criteria allowing to differentiate the quantifiers from each other. These operating criteria had the possibility, for the most part, to be then applied to German quantifiers, analyzed from a similar corpus to the French one. The study of a second German corpus, journalistic, has allowed to hone on the preferences of use relative to that kind of speech. All these vague quantifiers share a core meaning of “small vague quantities” and therefore the semes and the secondary potential traits allow to know each’s own semantic profile, to understand their operation and thus their preferred use. In the last part we put together the functioning of both language’s quantifiers, offer equivalencies by context and improvements of their monolingual and bilingual lexicographic treatment.

Cette thèse est une contribution à la théorie des modèles des corps valués. Les principaux résultats de ce texte sont des résultats d’éliminations des quantificateurs et des imaginaires. Le premier chapitre contient une étude des imaginaires dans les extensions finies de Qp. On y démontre que ces corps ainsi que leurs ultraproduits éliminent les imaginaires dans le langage géométrique. On en déduit un résultat de rationalité uniforme pour les fonctions zêta associées aux familles de relations d’équivalences définissables dans les extensions finies de Qp. La motivation première du deuxième chapitre est l’étude de W(F_p^alg) en tant que corps valué analytique de différence. Plus généralement, on démontre un théorème d’élimination des quantificateurs de corps dans le langage RV pour les corps valués analytiques -Henséliens de caractéristique nulle. On donne aussi une axiomatisation de la théorie de W(F_p^alg) ainsi qu’une preuve qu’elle est NIP. Dans le troisième chapitre, on prouve la densité des types définissables dans certains enrichissements d’ACVF. On en déduit un critère pour l’élimination des imaginaires et la propriété d’extension invariante. Ce chapitre contient aussi des résultats abstraits sur les ensembles extérieurement définissables dans les théories NIP. Dans le dernier chapitre, les résultats du chapitre précédent sont appliqués à VDF, la modèle complétion des corps valués munis d’une dérivation qui préserve la valuation, pour obtenir l’élimination des imaginaires dans le langage géométrique ainsi que la densité des types définissables et la propriété d’extension invariante. Ce chapitre contient aussi des considérations sur les fonctions définissables, les types et les groupes définissables dans VDF. / This thesis is about the model theory of valued fields. The main results in this text are eliminationsof quantifiers and imaginaries. The first chapter is concerned with imaginaries in finite extensions of Qp. I show that these fields and their ultraproducts eliminate imaginaries in the geometric language. As a corollary, I obtain the uniform rationality of zeta functions associated to families of equivalence relations that aredefinable in finite extensions of Qp.The motivation for the second chapter is to study W(F_p^alg) as an analytic difference valued field. More generally, I show a field quantifier elimination theorem in the RV-language for -Henselian characteristic zero valued fields with an analytic structure. I also axiomatise the theory of W(F_p^alg) and I show that this theory is NIP.In the third chapter, I prove the density of definable types in certain enrichments of ACVF. From this result, I deduce a criterion for the elimination of imaginaries and the invariant property. This chapter also contains abstract results on externally definable sets in NIP theories. In the last chapter, the previous chapter is applied to VDF, the model completion of valued fields with a valuation preserving derivation, to obtain the elimination of imaginaries in the geometric language, as well as the density of definable types and the invariant extension property. This chapter also contains considerations about definable functions, types and definable groupes in VDF.

Cette thèse traite des questions quantifiées (QQs) et, plus spécifiquement, de trois phénomènes : « Pair-List Readings » (PLRs), « Weak Islands » (WIs) et « Intervention Effects » (IEs). Nous observons que, dans plusieurs cas, il existe contraintes sur l’interprétation des QQs qui s’avèrent purement linguistiques. Par exemple, ni la logique ni la pragmatique n’empêche de répondre à la question Who did few girls see? par l’usage d’ une « pair list »; néanmoins, on ne le ferait pas spontanément. La question fondamentale qui sous-tend cette thèse est la suivante : quelles présuppositions ontologiques soutiennent le mieux une sémantique explicite des langues naturelles? Cette recherche contribue à l’ensemble de preuves que la langue naturelle quantifie sur au moins deux domaines, celui des individus et celui des évènements. Nous avons conçu une méthode novatrice pour tester les intuitions des locuteurs quant aux « conditions de réponse » des questions. Elle nous a permis de constater que des phrases interrogatives quantifiées peuvent être ambigües et avoir a la fois une lecture dite « d’objet » et une autre dite « d’événement ». Nous démontrons que les conditions de vérité de la réponse PL à une QQ sont celles de sa lecture événement. Nous postulons est que les possibilités d’interprétation d’une QQ dépendent de l’interaction des valeurs de deux paramètres : le domaine de quantification, (celui des événements ou celui des individus, E or D) et le type sémantique de la phrase sujet, (référentiel ou quantificatif, < d> ou < < dt> t> ). Une lecture PL résulte de la combinaison [E, < d> ]. Les WIs se produisent de la combinaison *[ E, < < dt> t> ]. Nous avançons l’hypothèse que les langues naturelles ne génèrent pas cette combinaison, et qu’elle est exclue à cause d’un « type mismatch ». Les combinaisons [D, < d> ] et [D, < < dt> t> ] donnent lieu toutes les deux a une lecture « objet ». Les IEs sont dus à la combinaison de celle-ci avec un autre élément (« WH-AGENT ») qui s’interpose. Nous proposons deux alternatives pour la sémantique des QQs. La première est algébrique et emploie des « alternative sets »; la deuxième est dynamique. Ici, nous suggérons que l’opérateur interrogatif, Q, fonctionne à la manière d’un quantificateur adverbial comme généralement ou toujours. Cette approche permet un traitement plus uniforme des phrases déclaratives et interrogatives et elle contribue à l’unification de la sémantique des expressions nominales et verbales. / This dissertation looks at quantified questions (“QQs”) and, specifically, at Pair-List readings, Weak Islands and Intervention Effects (“PLRs, ” “WIs” and “IEs”). In many cases, we observe that there are constraints on the interpretation of QQs that are irreducibly linguistic. Although no logical or pragmatic constraint precludes understanding, say, Who did few girls see? as a request for a pair-list, that interpretation is unavailable. The “big question” that structures this project is: What ontological presuppositions best support an explicit semantics for natural language? We contribute to the growing body of evidence that natural language quantifies over at least two basic domains, viz., individuals and events. We develop a somewhat novel method of testing speakers’ intuitions with regard to the “answerhood conditions” of questions. We found, first, that some quantified interrogatives can be ambiguous between an object- and an event-related reading. The truth conditions of the PL response to a quantified question are those of its event-related reading. The truth conditions of responses to non-quantified in-situ questions are also those of the event-related reading; the truth conditions of responses to raised quantified questions are those of the object-related reading. We hypothesize that the interpretive possibilities in QQs are a function of the values of two parameters: the domain being quantified over (events or individuals, E or D) and the type of the subject phrase (referential or quantificational, < d> or < < dt> t> ). A PL reading results from the combination [E, < d> ]. WIs are the product of the “combination” *[E, < < dt> t> ]. We hypothesize that there are no extant examples of this combination in natural language – a type mismatch precludes it. Both the combinations [D, < d> ] and [D, < < dt> t> ] yield object-related readings. IEs result from the combination of the combination [D, < < dt> t> ] and an intervener, “WH-AGENT.” We develop two proposals for the semantics of QQs. The first is algebraic and makes use of “alternative sets.” The second is dynamic. Here, the question operator, Q, is treated like an adverbial quantifier of the ilk of usually or always. This approach permits a more uniform treatment of the semantics of nominal and verbal expressions and of declaratives and interrogatives.

Les structures o-minimales, introduites dans les années '80 par Van den Dries et largement étudiées par Wilkie et Macintyre répondent à Grothendick en donnant le cadre d'une géométrie modérée. <br /> <br />Cette thèse montre un théorème du complémentaire explicite pour les<br />structures o-minimales polynomialement bornées, ce qui équivault à la modèle-complétude en théorie des modèles.<br /><br />En 1968, Gabrielov montre un théorème du complémentaire pour<br />les sous-analytiques globaux, qui en implique la o-minimalité. Il améliore ce résultat en 96, avec un théorème explicite. Une généralisation de celui-ci est présentée ici.<br /><br />Par des arguments de valuation dus à Lojaciewicz et à Miller, des propriétés de quasi-analycité sont exhibées, qui permettent d'adapter le schéma classique des preuves de modèle-complétude. Ce résultat permet de mieux comprendre la façon dont sont générées les structures o-minimales et donne un langage réduit sur lequel une structure polynomialement bornée est modèle-complète.

Dans cette thèse, nous aborderons deux aspects fondamentaux qui se posent dans les systèmes de commande modernes du fait de l'interaction entre des processus en temps continu et des dispositifs numériques: la synthèse de lois de commande en présence de quantificateurs et l'estimation d'état en présence de mesures sporadiques. Une des caractéristiques principales de cette thèse consiste également à proposer des méthodes constructives pour résoudre les problèmes envisagés. Plus précisément, pour répondre à cette exigence, nous allons nous tourner vers une approche basée sur les inégalités matricielles linéaires (LMI). Dans la première partie de la thèse, nous proposons un ensemble d'outils constructifs basés sur une approche LMI, pour l'analyse et la conception de systèmes de commande quantifiés impliquant des modèles et des correcteurs linéaires. L'approche est basée sur l'utilisation des inclusions différentielles qui permet de modéliser finement le comportement de la boucle fermée et ainsi d'obtenir des résultats intéressants. Dans la seconde partie de la thèse, inspirés par certains schémas d'observation classiques présentés dans la littérature, nous proposons deux observateurs pour l'estimation de l'état d'un système linéaire en présence de mesures sporadiques, c'est-à-dire prenant en compte la nature discrète des mesures disponibles. De plus, en se basant sur une des deux solutions présentées, une architecture de commande basée observateur est proposée afin de stabiliser asymptotiquement un système linéaire en présence à la fois de mesures sporadiques et d'un accès intermittent à l'entrée de commande du système. / In this dissertation, two fundamental aspects arising in modern engineered control systems will be addressed:On the one hand, the presence of quantization in standard control loops. On the other hand, the state estimation in the presence of sporadic available measurements. These two aspects are addressed in two different parts. One of the main feature of this thesis consists of striving to derive computer-aided tools for the solution to the considered problems. Specifically, to meet this requirement, we revolve on a linear matrix inequalities (LMIs) approach. In the first part, we propose a set of LMI-based constructive Lyapunov-based tools for the analysis and the design of quantized control systems involving linear plants and linear controllers. The entire treatment revolves on the use of differential inclusions as modeling tools, and on stabilization of compact sets as a stability notion. In the second part of the thesis, inspired by some of the classical observation schemes presented in the literature of sampled-data observers, we propose two observers to exponentially estimate the state of a linear system in the presence of sporadic measurements. In addition, building upon one of the two observers, an observer-based controller architecture is proposed to asymptotically stabilize a linear plant in the presence of sporadic measurements and intermittent input access.

Des nombreuses applications de méthodes formelles se fondent sur les solveurs SMT pour valider automatiquement les conditions à vérifier et fournissent des certificats de leurs résultats. Nous visons à la fois à améliorer l'efficacité des solveurs SMT et à accroître leur fiabilité. Notre première contribution est un cadre uniforme pour le raisonnement avec des formules quantifiées dans les solveurs SMT, dans lequel généralement diverses techniques d'instanciation sont utilisées. Nous montrons que les principales techniques d'instanciation peuvent être jetées dans ce cadre. Le cadre repose sur le problème de l'E-ground (dis)unification. Nous présentons une procédure de décision pour résoudre ce problème en pratique: Fermeture de congruence avec variables libres (CCFV}). Nous mesurons l'impact de CCFV dans les solveurs SMT veriT et CVC4. Nous montrons que nos implémentations présentent des améliorations par rapport aux approches à la fine pointe de la technologie. Notre deuxième contribution est un cadre pour le traitement des formules tout en produisant des preuves détaillées. Les principaux composants de notre cadre de production de preuve sont un algorithme de récurrence contextuelle générique et un ensemble extensible de règles d'inférence. Avec des structures de données appropriées, la génération des preuves ne crée que des frais généraux linéaires et les vérifications peuvent être vérifiées en temps linéaire. Nous avons également mis en œuvre l'approche en veriT. Cela nous a permis de simplifier considérablement la base du code tout en augmentant le nombre de problèmes pour lesquels des preuves détaillées peuvent être produites / In many formal methods applications it is common to rely on SMT solvers to automatically discharge conditions that need to be checked and provide certificates of their results. In this thesis we aim both to improve their efficiency of and to increase their reliability. Our first contribution is a uniform framework for reasoning with quantified formulas in SMT solvers, in which generally various instantiation techniques are employed. We show that the major instantiation techniques can be all cast in this unifying framework. Its basis is the problem of E-ground (dis)unification, a variation of the classic rigid E-unification problem. We introduce a decision procedure to solve this problem in practice: Congruence Closure with Free Variables (CCFV). We measure the impact of optimizations and instantiation techniques based on CCFV in the SMT solvers veriT and CVC4, showing that our implementations exhibit improvements over state-of-the-art approaches in several benchmark libraries stemming from real world applications. Our second contribution is a framework for processing formulas while producing detailed proofs. The main components of our proof producing framework are a generic contextual recursion algorithm and an extensible set of inference rules. With suitable data structures, proof generation creates only a linear-time overhead, and proofs can be checked in linear time. We also implemented the approach in veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced