Ce travail de thèse interroge la structure fondamentale du langage. Il s’inscrit dans la tradition greimassienne en ce sens qu’elle assume son affiliation avec les théories de Hjelmslev, Jakobson, Lévi-Strauss et Propp. Mais au-delà, il cherche ce que ces théories ont en commun et qu’elles n’avaient peut-être pas encore suffisamment abordé, notamment certaines relations avec la théorie thomienne/petitotienne. Nous postulons dans cette étude que le discours subit la contrainte d’un ordre sémantico-syntaxique sous-jacent et structurant. Plus précisément, nous postulons que le discours tend à s’organiser à partir, et/ou autour, d’une même chaîne sous-jacente, hiérarchique, contraignante, non aléatoire, transphrastique et restreinte de catégories sémantiques fondamentales. Nous nous inscrivons de fait dans le champ morphodynamique. A partir d’une double approche sémasiologique et distributionnelle, puis par des méthodes statistiques et mathématiques, nous montrons que certains sèmes, assimilables à des universaux et aux propriétés topologiques sous-jacentes, s’incrémentent naturellement dans le corps des énoncés. Ainsi, ce ne sont plus principalement des sèmes isolés que nous étudions mais des séries, des chaînes, des agencements syntagmatiques qui débouchent sur une forme de « proto-raisonnement » associant des sèmes. Enfin, nous montrons par l’expérimentation qu’il existe vraisemblablement aussi d’autres régularités à l’intérieur de cette structure continue ; régularités qui permettent de conforter l’hypothèse d’un principe autosimilaire entre structure profonde et structure superficielle. Notre thèse s’attache en principal à décrire, et à justifier l’existence d’un tel phénomène structural. / This thesis questions the fundamental structure of language. It belongs to the Greimas tradition in the sense that it assumes its affiliation with the theories of Hjelmslev, Jakobson , Levi-Strauss, and Propp. This work tries to go beyond by defining connections with Thom and Petitot theory. In this study, we postulate that discourse is constrained by an underlying semantic and syntactic structural order. More specifically, our assumption is that the discourse tends to be organized from and/or around a same underlying chain, involving non-random hierarchy, going beyond the sentences and being constrained to semantic fundamental categories. Our analysis is also included in a morphodynamic framework.From a double semasiologic and distributional approach, and from statistical and mathematical methods, we show that various semes, linked to universals and topological underlying properties, are naturally incremented in the discourse.As a consequence, what we are studying is not a collection of isolated semes but series, chains, syntagmatic arrangements that yield to a form of "proto-reasoning" associating semes. Finally, we show by experimentation, as there are likely other regularity patterns within the continuous structure. These regularities allow us to support the hypothesis of a self-similar principle between deep structure and surface structure. This thesis work is mainly focused on the description and the justification of the existence of such a structural phenomenon.

Dans cette thèse, on étudie des problèmes liés à la vérification de systèmes (logiciels). On s’intéresseplus particulièrement à la conception sûre de procédures de décision utilisées en vérification. De plus, onconsidère également un problème de modularité pour un langage de modélisation utilisé dans la plateformede vérification Why.De nombreux problèmes de vérification peuvent se réduire à un problème de satisfaisabilité modulodes théories (SMT). Pour construire des procédures de satisfaisabilité, Armando et al. ont proposé en2001 une approche basée sur la réécriture. Cette approche utilise un calcul général pour le raisonnementéquationnel appelé paramodulation. En général, une application équitable et exhaustive des règles ducalcul de paramodulation (PC) conduit à une procédure de semi-décision qui termine sur les entréesinsatisfaisables (la clause vide est alors engendrée), mais qui peut diverger sur les entrées satisfaisables.Mais ce calcul peut aussi terminer pour des théories intéressantes en vérification, et devient ainsi uneprocédure de décision. Pour raisonner sur ce calcul, un calcul de paramodulation schématique (SPC)a été étudié, en particulier pour prouver automatiquement la décidabilité de théories particulières etde leurs combinaisons. L’avantage de ce calcul SPC est que s’il termine sur une seule entrée abstraite,alors PC termine pour toutes les entrées concrètes correspondantes. Plus généralement, SPC est unoutil automatique pour vérifier des propriétés de PC telles que la terminaison, la stable infinité et lacomplétude de déduction.Une contribution majeure de cette thèse est un environnement de prototypage pour la conception etla vérification de procédures de décision. Cet environnement, basé sur des fondements théoriques, estla première implantation du calcul de paramodulation schématique. Il a été complètement implanté surla base solide fournie par le système Maude mettant en oeuvre la logique de réécriture. Nous montronsque ce prototype est très utile pour dériver la décidabilité et la combinabilité de théories intéressantes enpratique pour la vérification.Cet environnement est appliqué à la conception d’un calcul de paramodulation schématique dédié àune arithmétique de comptage. Cette contribution est la première extension de la notion de paramodulationschématique à une théorie prédéfinie. Cette étude a conduit à de nouvelles techniques de preuveautomatique qui sont différentes de celles utilisées manuellement dans la littérature. Les hypothèses permettantd’appliquer nos techniques de preuves sont faciles à satisfaire pour les théories équationnellesavec opérateurs de comptage. Nous illustrons notre contribution théorique sur des théories représentantdes extensions de structures de données classiques comme les listes ou les enregistrements.Nous avons également contribué au problème de la spécification modulaire pour les classes et méthodesJava génériques. Nous proposons des extensions du language de modélisation Krakatoa, faisant partiede la plateforme Why qui permet de prouver qu’un programme C ou Java est correct par rapport à saspécification. Les caractéristiques essentielles de notre apport sont l’introduction de la paramétricité à lafois pour les types et les théories, ainsi qu’une relation d’instantiation entre les théories. Les extensionsproposées sont illustrées sur deux exemples significatifs: tri de tableaux et fonctions de hachage.Les deux problèmes traités dans cette thèse ont pour point commun les solveurs SMT. Les procéduresde décision sont les moteurs des solveurs SMT, et la plateforme Why engendre des conditions devérification dérivées d’un programme source annoté, qu’elle transmet aux solveurs SMT (ou assistants depreuve) pour vérifier la correction du programme.Mots-clés: / In this thesis we address problems related to the verification of software-based systems. We aremostly interested in the (safe) design of decision procedures used in verification. In addition, we alsoconsider a modularity problem for a modeling language used in the Why verification platform.Many verification problems can be reduced to a satisfiability problem modulo theories (SMT). In orderto build satisfiability procedures Armando et al. have proposed in 2001 an approach based on rewriting.This approach uses a general calculus for equational reasoning named paramodulation. In general, afair and exhaustive application of the rules of paramodulation calculus (PC) leads to a semi-decisionprocedure that halts on unsatisfiable inputs (the empty clause is then generated) but may diverge onsatisfiable ones. Fortunately, it may also terminate for some theories of interest in verification, and thusit becomes a decision procedure. To reason on the paramodulation calculus, a schematic paramodulationcalculus (SPC) has been studied, notably to automatically prove decidability of single theories and oftheir combinations. The advantage of SPC is that if it halts for one given abstract input, then PC haltsfor all the corresponding concrete inputs. More generally, SPC is an automated tool to check propertiesof PC like termination, stable infiniteness and deduction completeness.A major contribution of this thesis is a prototyping environment for designing and verifying decisionprocedures. This environment, based on the theoretical studies, is the first implementation of theschematic paramodulation calculus. It has been implemented from scratch on the firm basis provided bythe Maude system based on rewriting logic. We show that this prototype is very useful to derive decidabilityand combinability of theories of practical interest in verification. It helps testing new saturationstrategies and experimenting new extensions of the original (schematic) paramodulation calculus.This environment has been applied for the design of a schematic paramodulation calculus dedicated tothe theory of Integer Offsets. This contribution is the first extension of the notion of schematic paramodulationto a built-in theory. This study has led to new automatic proof techniques that are different fromthose performed manually in the literature. The assumptions to apply our proof techniques are easyto satisfy for equational theories with counting operators. We illustrate our theoretical contribution ontheories representing extensions of classical data structures such as lists and records.We have also addressed the problem of modular specification of generic Java classes and methods.We propose extensions to the Krakatoa Modeling Language, a part of the Why platform for provingthat a Java or C program is a correct implementation of some specification. The key features arethe introduction of parametricity both for types and for theories and an instantiation relation betweentheories. The proposed extensions are illustrated on two significant examples: the specification of thegeneric method for sorting arrays and for generic hash map.Both problems considered in this thesis are related to SMT solvers. Firstly, decision procedures areat the core of SMT solvers. Secondly, the Why platform extracts verification conditions from a sourceprogram annotated by specifications, and then transmits them to SMT solvers or proof assistants to checkthe program correctness.

L'évolution des réflexions et la prise en compte du développement durable à tous les niveaux rendent indispensable l'intégration de ce concept dans les formations des élèves ingénieurs. L'intérêt grandissant pour cette thématique ne doit cependant pas faire oublier ses particularités : la dimension évolutive, la complexité, les incertitudes, les divergences de points de vue, la difficulté à le transformer en approche pragmatique... L'ensemble de ces éléments nous a conduit à émettre deux hypothèses. La première est que le concept de développement durable ne peut être assimilé à une connaissance supplémentaire à acquérir, il correspond à une prise de conscience et à un changement de paradigme. La seconde est que la modification des enseignements visant à une intégration du développement durable ne peut se faire par simple implémentation, elle nécessite une réflexion pédagogique, une innovation ciblée. La validation de ces hypothèses nous a amené à définir des objectifs pédagogiques et à proposer l'utilisation d'approches basées sur les pédagogies innovantes. L'étude menée s'est focalisée plus particulièrement sur l'utilisation des jeux de rôles. Ce type d'approche s'est avérée être une des possibilités pour aider l'étudiant à aborder de manière systémique et concrète les principes liés au développement durable. Pour répondre à une problématique d'évaluation et d'identification des contenus cognitifs associés au concept de développement durable, une méthode d'analyse basée sur l'utilisation des cartes cognitives a été développée. L'utilisation des cartes cognitives est apparue pertinente, en effet, cette forme de représentation schématique demandée aux élèves leur a permis d'avoir une vision holistique et de réfléchir aux interactions entre les différents éléments constitutifs du développement durable. Cette méthode présente plusieurs potentialités d'évolution : outil d'amélioration des formations, aide aux réflexions métacognitives ou encore support de réflexion collective sur le développement durable.

Dans cette thèse, nous abordons la question de l’identité sémantique respective des prépositions russes в (/v/) et на (/na/) en établissant pour chacune d’elles un schéma relationnel de base, en construisant leur configuration idéographique, en regroupant leurs relations sémantiques dans le but d’expliquer les emplois polysémiques de ces prépositions. Nous considérons la signification de la préposition comme un réseau complexe, où le sens abstrait de la préposition est précisé par un nombre d’éléments sémantiques (traits idéographiques et relationnels) qui font partie du contexte dans lequel se fixent les différents champs d’application de la préposition. Les systèmes prépositionnels du russe et du français ne sont pas identiques car les champs sémantico-relationnels des prépositions dans les deux langues sont différents : le caractère de la relation (l’activation des traits idéographiques) et le nombre d’entités mises en rapport, régies par telle ou telle préposition, diffèrent d’une langue à l’autre. / The thesis tackles the question of the semantic identity of the Russian prepositions « в » and « нa » establishing for each of them a relational basic scheme, by building their ideographic configuration, by grouping together their semantic relations in order to explain the polysemous use of them. It is argued that the meaning of the preposition is a complex system, where the abstract meaning of the preposition is specified by a number of semantic elements (ideographic and relational features) which are part of the context in which settle the various fields of application of the preposition. The Russian and French prepositional systems diverge because the semantico-relational fields of the prepositions are different in both languages : the character of the relation (activation of the ideographic features) and the number of entities in contact, governed by such or such preposition, differ from one language to another.

Les verbes de position sont décrits du point de vue d'une invariance mise au point pour chacun d'entre eux en fonction de la diversité des contextes dans laquelle on les trouve. Cela conduit d'une part à considérer que dans certains contextes leur sens n'est pas inutile au contenu informatif de l'énoncé et qu'il n'est pas équivalent à celui d'un verbe d'existence. Au contraire, l'emploi d'un verbe de position par un locuteur correspond à un choix motivé par la désignation de quelque chose de plus que l'être ou la présence du sujet. D'autre part, cette invariance mène à distinguer clairement le fonctionnement sémantique de chacun de ces verbes alors qu'ils semblent entrer en concurrence lorsqu'ils apparaissent dans des contextes visiblement similaires. / Posture verbs are described from the perspective of an invariance developed for each of them according to the diversity of the contexts where they can be found. It conduces, on the one hand, to consider that in some contexts their meaning is not ancillary to the informative content of the statement, and that it is not equivalent to the meaning of a being verb. In fact, the use of a posture verb by a speaker refers to a choice motivated by something more than the being or the presence of the subject. On the other hand, this invariance facilitates clear distinction of the semantical function of each of these verbs, while they may seem to have the same meaning, when they occur in contexts which seem similar at first glance.