Une technique d'abstraction et de partage de structure pour une methode de démonstration automatique non expérimentée jusqu'à présent est proposée. On donne aussi une généralisation de la règle d'inférence pour le cas propositionnel. Une preuve est séparée en plan + validation, ce qui correspond à séparer la partie purement déductive de l'algorithme d'unification. Cette séparation est utilisée pour détecter les ensembles responsables des échecs de validation pour un retour arrière non aveugle

Cette thèse, s'intéresse aux systèmes d'interaction, une notion visant à modéliser les interactions entre un système informatique et son environnement.<br /><br />La première partie développe, dans le cadre de la théorie des types de Martin-Löf, la théorie de base des systèmes d'interaction et des constructions inductives et co-inductives qu'ils permettent. On trouve dans cette partie une étude des liens entre systèmes d'interaction et topologies formelles et une formulation (en terme de systèmes d'interaction) d'un théorème de complétude vis-à-vis d'une sémantique topologique des théories géométriques (linéaires).<br /><br />Dans cette étude, la notion complètement standard de simulation, joue un rôle fondamental car elle permet de définir la notion de morphisme entre systèmes d'interaction. Ceci permet d'établir une équivalence entre la catégorie ainsi définie et une autre catégorie, beaucoup plus simple à décrire, celle des transformateurs de prédicats.<br /><br />En traduisant dans ce nouveau vocabulaire les constructions précédentes, on observe que les transformateurs de prédicats forment un nouveau modèle de la logique linéaire, qui est décrit puis étendu au second ordre.<br /><br />Enfin, les propriétés particulières des systèmes d'interaction / transformateurs de prédicats sont mises à profit pour donner une interprétation du lambda-calcul différentiel. Cela suppose d'introduire du non déterminisme, ce que les systèmes d'interaction et les transformateurs de prédicats permettent de faire.

Notre thèse traite la complétive objet et ses prédicats introducteurs en chinois. Nous adoptons, dans l'ensemble, le cadre théorique du lexique-grammaire de Gross (1984) et dans l'analyse concrète, celle de la structure prédicative de Muller (2001). Elle est divisée en cinq chapitres. Dans le premier " Etat des lieux ", nous présentons la conception de la complétive en tant qu'un type de subordonnée et nous adoptons l'analyse de la dépendance énonciative de Muller (1996). Ensuite nous présentons quelques analyses qui intègre la sémantique dans l'analyse de la complétive. Le chapitre 2 a pour objectif de délimiter notre objet d'étude, qui inclut trois sous-types : la complétive propositionnelle, le complément verbal sans sujet syntaxique (l'équivalent de la complétive infinitive du français) et l'interrogative indirecte dont la spécificité sémantique est bien prise en compte.Dans le troisième chapitre nous étudions les propriétés de sélection des prédicats introducteurs de la complétive en chinois : celles concernant le complément nominal et verbal sans sujet syntaxique d'une part, et celle entre la complétive déclarative et l'II d'autre part, à propos de laquelle nous étudions aussi les éléments qui la modifient. Dans le chapitre 4 la complétive objet est mise en parallèles avec trois autre types de constructions qui partagent le même schéma de construction [(SN1) +SV1+SN2+SV2] avec elle et qui impliquent aussi une relation de dépendance entre deux prédicats, ce sont la construction à double complément, la construction à 2nd complément et la construction à contrôle objet. Nous tenterons de fournir quelques outils de distinction d'ordre lexical ou contextuel.Le chapitre 5 concerne les propriétés syntaxiques de la complétive objet. Nous discuterons d'abord du morphème 'shuo' à propos de son statut de 'conjonction émergente' et de quelques caractéristiques d'intégration sous le terme de " main clause phenomena ". Ensuite seront scrutés les verbes " recteurs faibles " dans les termes de Blanche-Benveniste (1988) qui s'avéreront assez similaires à leurs équivalents en français et en anglais. Enfin nous analyserons les références temporelles dans la construction complétive. Nous postulerons qu'elles se basent principalement sur la télicité des prédicats matrice et la sémantique de leurs arguments ; les marqueurs aspectuels -le, -guo et -zhe modifient cette interprétation par défaut selon leur sémantique propre. Et nous donnerons une analyse détaillée des contraintes de différents degrés imposées sur les différents types de prédicats.

Nous présentons une recherche en ingénierie des connaissances appliquée aux prédicats linguistiques et aux définitions lexicographiques de la théorie Sens-Texte (TST). Notre méthodologie comporte trois étapes. 1. Nous montrons en quoi la conceptualisation de la TST devrait être étendue pour faciliter sa formalisation. Nous justifions la nécessité de définir un niveau sémantique profond (SemP) à base de graphes. Nous y définissons la notion de type d'unité sémantique profonde et sa structure actancielle, de sorte que leur organisation hiérarchique puisse correspondre à une hiérarchie de sens au sein de laquelle ces structures actancielles sont héritées et spécialisées. Nous reconceptualisons les définitions lexicographiques au niveau SemP, et au niveau du dictionnaire. Finalement, nous présentons un prototype d'éditeur de définitions basé sur la manipulation directe de graphes. 2. Nous proposons un formalisme de représentation des connaissances adapté à cette conceptualisation. Nous démontrons que les logiques de description et le formalisme des Graphes Conceptuels ne sont pas adaptés, et nous construisons alors un nouveau formalisme, dit des Graphes d'Unités. 3. Nous étudions l'opérationnalisation du formalisme des Graphes d'Unités. Nous lui associons une sémantique formelle basée sur la théorie des modèles et l'algèbre relationnelle, et montrons que les conditions de décidabilité du raisonnement logique correspondent aux intuitions des lexicographes. Nous proposons également une implémentation du formalisme avec les standards du web sémantique, ce qui permet de profiter des architectures existantes pour l'interopérationnalisation sur le web des données lexicales liées.

Le travail de cette thèse se situe dans le domaine de la sémantique nominale et porte sur un échantillon de noms dénotant les humains (NH) pendant les différentes phases de vie : bébé, enfant, adolescent, adulte, vieillard (N-[âge]). Elle poursuit un triple objectif. D'abord, il s'agit d'offrir une description linguistique fine d'un ensemble de N-[âge] dont le fonctionnement est resté méconnu jusqu'à présent. En démontrant leur caractère hybride - les N-[âge] dénotent à la fois des propriétés référentiellement essentielles et intrinsèquement transitoires - nous mettons en évidence des paramètres inédits pour la description des NH en général. Enfin, notre thèse explore la possibilité d'un élargissement notionnel du domaine aspectuel vers la sémantique nominale en interrogeant la notion de phase et en démontrant que l'ensemble des N-[âge] bénéficie d'une structure phasale.

Le travail de cette thèse se situe dans le domaine de la sémantique nominale et porte sur un échantillon de noms dénotant les humains (NH) pendant les différentes phases de vie : bébé, enfant, adolescent, adulte, vieillard (N-[âge]). Elle poursuit un triple objectif. D’abord, il s’agit d’offrir une description linguistique fine d’un ensemble de N-[âge] dont le fonctionnement est resté méconnu jusqu’à présent. En démontrant leur caractère hybride – les N-[âge] dénotent à la fois des propriétés référentiellement essentielles et intrinsèquement transitoires – nous mettons en évidence des paramètres inédits pour la description des NH en général. Enfin, notre thèse explore la possibilité d’un élargissement notionnel du domaine aspectuel vers la sémantique nominale en interrogeant la notion de phase et en démontrant que l’ensemble des N-[âge] bénéficie d’une structure phasale. / This thesis research lies in the field of nominal semantics and focuses on a sample of nouns denoting humans (HN) during different stages of life: infant, child, teenager, adult, elderly (N-[age]). It is three fold. First, this works aims at offering a linguistic description of a set of N-[age] whose operation has remained unknown until now. Demonstrating their hybrid nature - N-[age] denote both referentially essential and intrinsically transient properties - we provide novel parameters for the description of HN in general. Finally, this thesis explores the possibility of notional extension of the aspectual domain to nominal semantics by questioning the concept of phase and by demonstrating that all N-[age] have a phasal structure.

Dans cette thèse, nous nous intéressons aux trois types d’expressions dont la structure s’écarte du modèle de la proposition transitive canonique, à savoir les constructions : anticausatives, à causalité interne, et impersonnelles en polonais et en russe. Leur point commun est que l’écart par rapport à une phrase transitive porte sur la référence du sujet de la proposition. Dans tous les cas, le référent du sujet est non-agentif. Dans certains cas, le marquage morphologique reflète cette absence, tant sur le prédicat qui est marqué à la troisième personne du singulier neutre que par l’absence d’un sujet nominatif. Ailleurs, la morphologie ne laisse rien, ou presque rien apparaître, le prédicat s’accordant avec l’argument Thème ou le Patient. Ces expressions feront l’objet d’une étude comparative, dans laquelle seront étudiées : la nature de chaque participant non-canonique qui apparaît dans la proposition, les caractéris¬tiques de chaque prédicat présent, et enfin, les propriétés combinatoires entre les participants et les prédicats. Il sera montré que la nature et la structure et enfin la manière dont sont légi¬timés les sujets non-canoniques ne sont pas seulement liées aux propriétés du réfé¬rent de sujet, mais aussi dépendent de la nature du prédicat. Tout comme cela a été proposé pour les constructions anticausatives et à causalité interne (cf. Alexiadou & Anagnostopou¬lou (2003), Alexiadou, Anagnostopoulou & Schäfer (2006), Schäfer (2008)), nous avancerons que les constructions impersonnelles comportent un prédicat Cause qui est responsable de la légitimation thématique des caus(at)eurs nominatifs et obliques. Les différences entre ces structures sont dues à la présence ou à l’absence de la tête Voice. Vues sous cet angle, les constructions impersonnelles sont une sorte de causativisation. Le caus(at)eur indéfini (cf. Kibort (2004)) présent dans les constructions impersonnelles d’une part, et la possible présence des causeurs obliques d’autre part, sont des preuves qui étaient cette hypothèse. / In this dissertation we study three kinds of expressions that deviate from the model of canonical transitive sentences, namely anticausative, internal causation and impersonal constructions in Polish and in Russian. The common point is that the deviation from a transitive sentence has to do with the subject’s reference. In all cases, the referent of the subject is non-agentive. In some cases, the morphological marking reflects this absence, both on the predicates which is frozen in the third person singular (neuter), and by the absence of a nominative subject. In the other two cases, the non-canonicity is not morpologically revealed because the inflected verb agrees with the nominative argument whose referent is the Theme or the Patient.A comparative study of these expressions will be given, in so far as the nature of the non-canonical participants that appear in the sentence, the characteristics of each predicate, and finally, the combinatorial properties between participants and predicates are concerned.It will be shown that the nature, the structure and ultimately the way that non-canonical subjects are licensed are not only related to the properties of the subject’s reference, but also depend on the nature of the predicate. Just as it was proposed for anticausatives and internal causal constructions (Alexiadou & Anagnostopoulou (2003), Alexiadou, Anagnostopoulou & Schäfer (2006), Schäfer (2008)), it will be shown that impersonal constructions include a Cause predicate that is responsible for the thematical licensing of nominative and oblique causers. The differences between these structures are due to the presence or absence of a Voice head. From this perspective, impersonal constructions encode a kind of causativisation. The indefinite causer (analysed in Kibort (2004)), which is present in impersonal constructions on the one hand, and the possible presence of other oblique causer, are thus deemed to be evidence that supports this hypothesis.

Le système de types de la logique d'ordre supérieur permet d'exclure certaines expressions indésirables telles que l'application d'un prédicat à lui-même. Cependant, il ne suffit pas pour vérifier des critères plus complexes comme l'absence de divisions par zéro. Cette thèse est consacrée à l’étude d’une extension de la logique d’ordre supérieur appelée sous-typage par prédicats (predicate subtyping), dont l'objet est de rendre l'attribution de types aussi expressive que l'attribution de prédicats. A partir d'un type A et d'un prédicat P(x) de domaine A, le sous-typage par prédicats permet de construire un sous-type de A, noté {x : A | P(x)}, dont les éléments sont les termes t de type A tels que P(t) est démontrable. Le sous-typage par prédicats est au coeur du système PVS.Ce travail présente la formalisation d'un système minimal incluant le sous-typage par prédicats, appelé PVS-Core, ainsi qu'un système de certificats vérifiables pour PVS-Core. Ce deuxième système, appelé PVS-Cert, repose sur l'introduction de termes de preuves et de coercions explicites. PVS-Core et PVS-Cert sont munis d'une notion de conversion correspondant respectivement à l'égalité modulo beta et à l'égalité modulo beta et effacement des coercions, choisi pour établir une correspondance simple entre les deux systèmes.La construction de PVS-Cert est semblable à celle des PTS (Pure Type Systems) avec paires dépendantes et PVS-Cert peut être muni de la notion de beta-sigma-réduction utilisée au coeur de ces systèmes. L'un des principaux théorèmes démontré dans ce travail est la normalisation forte de la réduction sous-jacente à la conversion et de la beta-sigma-réduction. Ce théorème permet d'une part de construire un algorithme de vérification du typage (et des preuves) pour PVS-Cert et d'autre part de démontrer un résultat d'élimination des coupures, utilisé à son tour pour prouver plusieurs propriétés importantes des deux systèmes étudiés. Par ailleurs, il est également démontré que PVS-Cert est une extension conservative du PTS lambda-HOL, et qu'en conséquence PVS-Core est une extension conservative de la logique d'ordre supérieur.Une deuxième partie présente le prototype d'une instrumentation de PVS pour produire des certificats de preuve. Une troisième et dernière partie est consacrée à l'étude de liens entre logique classique et constructive avec la définition d'une traduction par double négation minimale ainsi que la présentation d'un algorithme de constructivisation automatique des preuves. / The type system of higher-order logic allows to exclude some unexpected expressions such as the application of a predicate to itself. However, it is not sufficient to verify more complex criteria such as the absence of divisions by zero. This thesis is dedicated to the study of an extension of higher-order logic, named predicate subtyping, whose purpose is to make the assignment of types as expressive as the assignment of predicates. Starting from a type A and a predicate P(x) of domain A, predicate subtyping allows to build a subtype of A, denoted {x : A | P(x)}, whose elements are the terms t of type A such that P(t) is provable. Predicate subtyping is at the heart of the proof system PVS.This work presents the formalization of a minimal system expressing predicate subtyping, named PVS-Core, as well as a system of verifiable certificates for PVS-Core. This second system, named PVS-Cert, is based on the introduction of proof terms and explicit coercions. PVS-Core and PVS-Cert are equipped with a notion of conversion corresponding respectively to equality modulo beta and to equality modulo beta and the erasure of coercions, chosen to establish a simple correspondence between the two systems.The construction of PVS-Cert is similar to that of PTSs (Pure Type Systems) with dependent pairs and PVS-Cert can be equipped with the notion of beta-sigma-reduction used at the core of these systems. One of the main theorems proved in this work is the strong normalization of both the reduction underlying the conversion and beta-sigma-reduction. This theorem allows, on the one hand, to build a type-checking (and proof-checking) algorithm for PVS-Cert and, on the other hand, to prove a cut elimination result, used in turn to prove important properties of the two studied systems. Furthermore, it is also proved that PVS-Cert is a conservative extension of the PTS lambda-HOL and that, as a consequence, PVS-Core is a conservative extension of higher-order logic.A second part presents the prototype of an instrumentation of PVS to generate proof certificates. A third and final part is dedicated to the study of links between classical and constructive logic, with the definition of a minimal double-negation translation as well as the presentation of an automated proof constructivization algorithm.

Cette thèse a un double objectif : 1) Étudier le comportement sémantique et syntaxique des verbes simples persans par rapport aux prédicats complexes dans les événements spatiaux respectant la typologie de Talmy sur cadrage verbal ou cadrage satellitaire ; et 2) Analyser la systématicité sémantique dans la formation des prédicats complexes basée sur une approche constructionnelle et expliquer leurs comportements exacts, à savoir leur productivité, la causalité, leur durée, et le comportement syntaxique de leurs pré-verbes en fonction de leurs significations. Dans la première partie de l’analyse, nous parlons du comportement des verbes simples par rapport aux prédicats complexes dans les événements spatiaux. Notre analyse est basée sur un vaste corpus. Les prédicats complexes expriment fréquemment le comportement et d’autres informations sémantiques tandis qu’une fréquence élevée de verbes simples apparaît comme des constructions neutres sans exprimer aucune information spécifique. La distribution syntaxique des prédicats complexes respecte la règle de l’« économie de la langue » étant donné que toutes les informations sémantiques sont aussi encodées dans la construction elles-mêmes. Par ailleurs, les verbes simples exigent, dans la majorité des cas, des clauses dépendantes pour exprimer le comportement. En outre, les prédicats complexes encodent, à la fois, le mouvement et les événements d’emplacement, tandis que les verbes simples sont pour la plupart intransitifs et se réfèrent aux événements locatifs. Les lacunes mentionnées ci-dessus sur des verbes simples ont conduit au remplacement de ces derniers par des prédicats complexes au fil du temps. Dans la deuxième partie de notre analyse, nous traitons les caractéristiques sémantiques de prédicats complexes dans des événements spatiaux à la lumière de la théorie de Grammaire de Construction et des approches fondées sur le corpus. Selon Goldberg, nous considérons des constructions de prédicats complexes à part entière. Kardan, "Faire" ; dādan, 'Donner'; zadan, 'Frapper' ; et bordan, 'Prendre', sont les verbes supports étudiés dans cette thèse. Ces verbes supports sont parmi ceux les plus fréquents ayant le plus de pré-verbes en commun dans notre corpus. Premièrement, nous avons identifié les extensions sémantiques de chaque verbe support. Cette catégorisation nous a permis de révéler un certain degré de productivité sémantique ainsi que la généralisation entre chaque verbes supports et le type de pré-verbes avec lesquels il pourrait co-se produire. Autrement dit, chaque verbe support se combine avec un type spécifique de pré-verbe. Il est à note que même des extensions métaphoriques ont un certain degré de productivité et les locuteurs peuvent ainsi les généraliser. Nous tenons également à noter que les prédicats complexes dans les événements spatiaux font partis de la famille de constructions résultatives. Certains comportements des prédicats complexes, tels que leur causalité et la durée de l’activité, sont expliqués en fonction de leur sémantique, et il est démontré que toute la construction est responsable de tels comportements. La comparaison entre les combinaisons qui ont des verbes supports différents mais des pré-verbes identiques évoque quelques différences sémantiques et syntaxiques, ce qui est la preuve de la systématicité existante dans la formation des prédicats complexes. Grâce à une analyse collostructionnelle, nous parlons du degré d’attraction de chaque verbe support par rapport aux catégories sémantiques. Enfin, le type de fréquences de prédicats complexes révèle le degré de productivité dans chaque verbe support, qui ressemble à: Kardan=Zadan > dādan > bordan. / The purpose of this dissertation is twofold : 1) to investigate the semantic and syntactic behavior of Persian simplex verbs vs. CPs in spatial events with respect to Talmy’s typology of satellite-framed and verb-framed languages ; and 2) to analyze the semantic systematicity in the formation of CPs based on a constructional approach and explain their certain behaviors, namely, their productivity, causativity, duration, and syntactic behavior of their PVs through the meaning of the construction.In the first part of the analysis, we discuss the behaviour of simplex verbs vs. CPs in spatial events. Our analysis is based on an extensive corpus. CPs express manner and other semantic information frequently while a high frequency of simplex verbs appears as neutral constructions without expressing any specific information. The syntactic distribution of CPs follow the ‘economy of language’ rule since all the semantic information is encoded in the construction itself; on the other hand, simplex verbs require dependent clauses to express manner in the majority of cases. Furthermore, CPs encode both motion and location events while simplex verbs are mostly intransitive and refer to locative events. The above-mentioned shortcomings of simplex verbs have led to the replacement of these verbs by CPs over time. In the second part of our analysis, we deal with the semantic features of CPs in spatial events in the light of Construction Grammar theory and corpus-based approaches. Following Goldberg we consider CPs constructions in their own right. Kardan, ‘do’ ; dādan, ‘give’; zadan, ‘hit’; and bordan, ‘take’, are the LVs under the study in this thesis. These LVs found to be among the most frequent ones with the most PVs in common in our corpus. Firstly, we identified the semantic extensions of each LV. This categorization reveals a certain degree of semantic productivity and generalization between each LV and the type of PVs with which it can co-occur. In other words, each LV combines with a specific type of PVs. Even metaphorical extensions have a certain degree of productivity and speakers can generalize about them. We also argue that CPs in spatial events are a family of resultative constructions. Certain behaviors of CPs, namely, their causativity, and the duration of the activity, are explained based on their semantics, and it is shown that the whole construction is responsible for such behaviors. The comparison between combinations that have different LVs but identical PVs reveals certain semantic and syntactic differences, which is evidence for the existing systematicity in the formation of CPs. Through a collostructional analysis we discuss the degree of attraction of each LV with respect to the semantic categories.

Le travail de thèse présenté dans ce document porte sur la conception d'un service de validation et d'enrichissement d'annotations pour un outil industriel de gestion des connaissances basé sur le langage des Topic Maps (TM). Un tel service nécessitant la mise en oeuvre de raisonnements sur les connaissances, il a été nécessaire de doter le langage des TM d'une sémantique formelle. Ceci a été réalisé par l'intermédiaire d'une transformation réversible des TM vers le formalisme logique des graphes conceptuels qui dispose d'une représentation graphique des connaissances (les TM pouvant facilement en être munie d'une). La solution a été mise en oeuvre dans deux applications, l'une conçue pour la veille médiatique et l'autre pour la promotion de ressources touristiques. Schématiquement, des annotations sont extraites automatiquement des documents selon le domaine concerné (actualité/économie ou tourisme) puis ajoutées à la base de connaissances. Elles sont ensuite fournies au service d'enrichissement et de validation qui les complète de nouvelles connaissances et décide de leur validité, puis retourne à la base de connaissance le résultat de l'enrichissement et de la validation.