| 1 |
Vers un outillage informatique optimisé pour corpus langagiers oraux en vue d'une exploitation textométrique : le cas des interrogatives partielles dans ESLO
|
|
|
|
In: Corpus ; https://halshs.archives-ouvertes.fr/halshs-03133017 ; Corpus, 2021 (2021)
|
|
BASE
|
|
Show details
|
|
|
| 2 |
CLAPI : étudier l'interaction avec les corpus oraux
|
|
|
|
In: https://halshs.archives-ouvertes.fr/halshs-03083003 ; 2020 (2020)
|
|
BASE
|
|
Show details
|
|
|
| 3 |
Methodology to harmonize and process the oral data of CEFC ; Méthodologie d’harmonisation et de traitement des données orales du CÉFC
|
|
|
|
In: ISSN: 0458-726X ; EISSN: 1958-9549 ; Langages ; https://halshs.archives-ouvertes.fr/halshs-03008795 ; Langages, Armand Colin (Larousse jusqu'en 2003), 2020, Orféo : un corpus et une plateforme pour l'étude du français contemporain, pp.39-52. ⟨10.3917/lang.219.0039⟩ ; https://www.revues.armand-colin.com/lettres-langues/langages/langages-no-219-32020 (2020)
|
|
BASE
|
|
Show details
|
|
|
| 4 |
Interoperability between proof systems using the logical framework Dedukti ; Interopérabilité entre systèmes de preuves en utilisant le cadre logique Dedukti
|
|
|
|
In: https://hal.archives-ouvertes.fr/tel-03224039 ; Logic in Computer Science [cs.LO]. Université Paris-Saclay, 2020. English. ⟨NNT : 2020UPASG053⟩ (2020)
|
|
Abstract:
There is today a large family of proof systems based upon variouslogics: The Calculus of Inductive Constructions, Higher-Order logic orSet theory, etc. The diversity of proof systems has the negativeconsequence that theorems are formalized many times. One way toovercome this issue would be to make proof systems interoperable. Inthis thesis, we have tackled the interoperability problem for proofsystems both on the theoretical and the practical side using theDedukti logical framework.We begin our journey by looking at Cumulative Type Systems (CTS), afamily of type systems which extends that of Pure Type Systemswith a subtyping relation. CTS provides a common skeleton to manylogics used today. The logic behind Coq, HOL-Light, Lean, Matita orPVS can be seen as an extension of CTS with various features(inductive types, proof irrelevance, predicate subtyping, …). Wedefine a new notion of embedding between CTS. We also provide a soundbut incomplete algorithm to decide whether a proof in one CTS can betranslated into another CTS. This algorithm can also be seen as anextension of Coq's algorithm to check that the floating universeconstraints are consistent. Then, we propose a new embedding of CTSinto Dedukti and give a soundness proof of this embedding. Theseresults show that Dedukti is suitable for studying interoperability onthe theoretical side.We continue our journey on a case of study: The proof of Fermat'slittle theorem written in Matita. We show how we were able totranslate this proof to various proof systems through Dedukti. Thistranslation mainly relies on two tools created for this purpose:— Dkmeta, a tool which proposes to use rewriting as a way to writeproofs transformation programs. One advantage of this tool is that itreuses the syntax of Dedukti itself.— Universo, a tool which implements the aforementioned algorithm whichallows to translate a proof in one CTS (written in Dedukti) toanother.This semi-automatic translation allows to translate the proof ofFermat's little theorem into a weak but expressive logic calledSTTforall. STTforall is a constructive version of Simple Type Theorywith prenex polymorphism. As a consequence, a proof in STTforall canbe exported easily to many proof systems. This case of study showsthat Dedukti is also suitable for interoperability on the practicalside.The tools used for these transformations could be reused also forproofs coming from other proof systems for which an encoding inDedukti is known (such as Coq or Agda).The journey ends with the exportation of the proof of Fermat's littletheorem encoded in STTforall towards 5 different proof systems: Coq,Lean, Matita, OpenTheory (a member of the HOL-family proof systems)and PVS. We have implemented a user interface for that via a websitecalled Logipedia.Logipedia was designed with the goal of containing many more proofs thatcould be shared between proof systems and as such is intended to be anencyclopedia of formal proofs. ; Il existe aujourd'hui une large famille de systèmes de preuve baséesur différentes logiques: Le calcul des constructions inductives, lalogique d'ordre supérieur, la théorie des ensembles, etc. Undésavantage majeur de cette diversité est, que les théorèmes sontprouvés de nombreuses fois. Une possibilité pour résoudre ce problèmeest de rendre les systèmes de preuve interoperables. Dans cette thèse,nous avons attaqué le problème d'interopérabilité entre systèmes depreuve aussi bien sur le plan théorique que le plan pratique enutilisant le cadre logique Dedukti.Notre voyage commence avec l'exploration des systèmes de typescumulatifs (CTS), une famille de systèmes de type qui étend celle dessystèmes de types pures avec une relation de sous-typage. Les CTSfournissent aujourd'hui une squelette commun a beaucoup de logiquesutilisés aujourd'hui. Les logiques derrières les systèmes Coq,HOL-Light, Lean, Matita ou bien PVS peuvent toutes être vues comme desextensions des CTS avec des fonctionnalités différentes (typesinductifs, irrelevance de la preuve, sous-typage propositionnel,.). Nous définissons une nouvelle notion de traduction entreCTS. Entre autre, nous expliquons un nouvel algorithme (correct maisincomplet) pour déterminer si une preuve écrite dans un CTS peut-êtretraduire dans un autre CTS. Cet algorithme peut aussi être vu commeune extension de l'algorithme de Coq qui permet de vérifier qu'unensemble de contraintes sur les univers est cohérent. Finalement, nousproposons un nouvel encodage des CTS dans Dedukti et nous prouvonsque cet encodage est correct. Ces résultats montrent que Dedukti estun cadre logique approprié sur le plan théorique pour étudierl'interopérabilité entre systèmes de preuve.Nous poursuivons notre voyage avec une étude de cas: le petit théorèmede Fermat prouvé en Matita. Nous montrons comment nous avons putraduire cette preuve vers différents systèmes à travers le cadrelogique Dedukti. Cette traduction se repose principalement sur deuxoutils que nous avons créees :- Dkmeta qui permet d'utiliser la réécriture comme un langage à partentière pour écrire des traductions de preuves. Un avantage de cetoutil est qu'il ré-utilise la syntaxe de Dedukti.- Universo, un outil qui permet d'implémenter l'algorithme mentionnéprécédemment qui permet de traduire une preuve d'un CTS (en Dedukti)vers un autre.Cette procédure semi-automatique permet de traduire la preuve du petitthéorème de Fermat dans une logique assez faible mais expressive quel'on appelle STTforall. STTforall est une version constructive de lathéorie des types simples avec du polymorphisme prénexe. La simplicitéde cette logique permet d'exporter des preuves de STTforall vers denombreux systèmes de preuve. Cette étude de cas montre que Deduktiest tout aussi efficace en tant qu'outil pour faire del'interopérabilité sur le plan pratique.Les outils que nous avons développés dans cette thèse ne sont passpécifiques à cette traduction et peuvent être réutilisés pourd'autres systèmes de preuve dont un encodage en Dedukti est connu(comme Coq ou bien Agda).Finalement, nous concluons ce voyage avec l'exportation du petitthéorème de Fermat vers cinq systèmes de preuve différents: Coq, Lean,Matita, OpenTheory (membre de la famille des systèmes de preuve basésur la logique d'ordre supérieure) et PVS. Cette traduction estdisponible via un site web appelé Logipedia.Logipedia n'a pas été créé seulement pour cette traduction mais avecl'objectif de contenir beaucoup plus de preuves que l'on pourraitpartager entre plusieurs systèmes de preuves. Cela rendrait Logipediaalors une encyclopédie de preuves formelles en ligne.
|
|
Keyword:
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]; Cadre logique; Dedukti; Interoperabilité; Interoperability; Logical Framework
|
|
URL: https://hal.archives-ouvertes.fr/tel-03224039
https://hal.archives-ouvertes.fr/tel-03224039v3/document
https://hal.archives-ouvertes.fr/tel-03224039v3/file/thesis%20%281%29.pdf
|
|
BASE
|
|
Hide details
|
|
|
| 5 |
Méthodologie d’harmonisation et de traitement des données orales du CÉFC
|
|
|
|
In: Langages, N 219, 3, 2020-08-11, pp.39-52 (2020)
|
|
BASE
|
|
Show details
|
|
|
| 6 |
Semantic Interoperability of Multilingual Lexical Resources in Lexical Linked Data ; Interopérabilité Sémantique Multi-lingue des Ressources Lexicales en Données Liées Ouvertes
|
|
|
|
In: https://tel.archives-ouvertes.fr/tel-01681358 ; Informatique et langage [cs.CL]. Université Grenoble Alpes, 2016. Français. ⟨NNT : 2016GREAM067⟩ (2016)
|
|
BASE
|
|
Show details
|
|
|
| 7 |
Semantic Interoperability of Multilingual Lexical Resources as Lexical Linked Data ; Interopérabilité sémantique multilingue des ressources lexicales en données lexicales liées ouvertes
|
|
|
|
In: https://tel.archives-ouvertes.fr/tel-01425123 ; Intelligence artificielle [cs.AI]. Université Grenoble Alpes, 2016. Français (2016)
|
|
BASE
|
|
Show details
|
|
|
| 8 |
Réconciliation d'alignements multilingues dans BioPortal
|
|
|
|
In: 27es Journées francophones d'Ingénierie des Connaissances ; IC: Ingénierie des Connaissances ; https://hal-lirmm.ccsd.cnrs.fr/lirmm-01395900 ; IC: Ingénierie des Connaissances, Jun 2016, Montpellier, France ; https://ic2016.sciencesconf.org/ (2016)
|
|
BASE
|
|
Show details
|
|
|
| 9 |
Utilisation d'un format commun pour structurer les métadonnées de corpus oraux : objectifs, enjeux et méthode
|
|
|
|
In: Données, métadonnées des corpus et catalogage des objets en sciences humaines et sociales ; https://halshs.archives-ouvertes.fr/halshs-01357271 ; Données, métadonnées des corpus et catalogage des objets en sciences humaines et sociales, Jun 2016, Poitiers, France (2016)
|
|
BASE
|
|
Show details
|
|
|
| 10 |
Utilisation d'un format commun pour structurer les métadonnées de corpus oraux : objectifs, enjeux et méthode
|
|
|
|
In: Données, métadonnées des corpus et catalogage des objets en sciences humaines et sociales ; https://halshs.archives-ouvertes.fr/halshs-01357271 ; Données, métadonnées des corpus et catalogage des objets en sciences humaines et sociales, Jun 2016, Poitiers, France (2016)
|
|
BASE
|
|
Show details
|
|
|
| 11 |
Observatology :Towards a science of observational adequacy in linguistics ; Observatologie : Vers une science de l'adéquation observationnelle en linguistique
|
|
|
|
In: https://hal.archives-ouvertes.fr/tel-01889762 ; Linguistique. Université Paris Ouest Nanterre la défense, 2015 (2015)
|
|
BASE
|
|
Show details
|
|
|
| 12 |
Intégrer la création de métadonnées multilingues dans une chaîne éditoriale ; : PACTOLS et OpenTheso
|
|
|
|
In: Multilinguisme, frein ou catalyseur de la diffusion scientifique en Europe et en Méditerranée ; https://halshs.archives-ouvertes.fr/halshs-01218971 ; Multilinguisme, frein ou catalyseur de la diffusion scientifique en Europe et en Méditerranée, Oct 2015, Marseille, France. 2015 ; http://medici2015.sciencesconf.org/ (2015)
|
|
BASE
|
|
Show details
|
|
|
| 13 |
FRANTIQ : faciliter l’interconnexion des données de la recherche en archéologie et sciences de l’Antiquité
|
|
|
|
In: Humanités numériques, l'exemple de l'Antiquité / Digital Humanities and Antiquity ; https://halshs.archives-ouvertes.fr/halshs-01212703 ; Humanités numériques, l'exemple de l'Antiquité / Digital Humanities and Antiquity, Sep 2015, Grenoble, France. 2015 ; http://dhant.sciencesconf.org/ (2015)
|
|
BASE
|
|
Show details
|
|
|
| 14 |
Mutualiser et diffuser des corpus : vraiment ? Pourquoi ? Comment ?
|
|
|
|
In: « Corpus complexes et enjeux méthodologiques : de la collecte de données à leur analyse » ; https://halshs.archives-ouvertes.fr/halshs-01165906 ; « Corpus complexes et enjeux méthodologiques : de la collecte de données à leur analyse », May 2015, Lyon, France (2015)
|
|
BASE
|
|
Show details
|
|
|
| 15 |
Modélisation et Exploitation de Profils : Accès Sémantique à des Ressources ; ÅÓÐÐ××ØØÓÒ Ø ÜÔÐÓÓØØØØÓÒ ÈÖÓÓÐ× × ËËÑÑÒØØÕÙÙ × ÊÊ××ÓÙÖ × È× ÐÐÒÒ ÄÄÙÖÖ Ì ÒÒÒÓÑ
|
|
|
|
In: https://hal.archives-ouvertes.fr/hal-01802093 ; Editions Universitaires Européennes, 2015, 978-3-8416-7617-7 ; https://www.editions-ue.com/ (2015)
|
|
BASE
|
|
Show details
|
|
|
| 16 |
OpenTheso, gestionnaire de thésaurus normalisé et multilingue pour un web de données ouvertes
|
|
|
|
In: Thésaurus et terminologies multilingues ; https://halshs.archives-ouvertes.fr/halshs-02973874 ; Thésaurus et terminologies multilingues, AthenaPlus-TOTh workshop, Dec 2014, Bruxelles, Belgique (2014)
|
|
BASE
|
|
Show details
|
|
|
| 17 |
De l'analyse au partage des données, quel(s) format(s) choisir ? L'exemple d'un corpus d'interactions parents-enfant
|
|
|
|
In: Traitement de corpus (Actes de Coldoc 2012) ; COLDOC 2012 : Traitement de corpus linguistiques ; https://hal.archives-ouvertes.fr/hal-00850172 ; COLDOC 2012 : Traitement de corpus linguistiques, Oct 2012, Paris, France. pp. 128-142 (2012)
|
|
BASE
|
|
Show details
|
|
|
| 18 |
Un système d'intégration des métadonnées dédiées au multimédia
|
|
|
|
In: https://tel.archives-ouvertes.fr/tel-00841157 ; Multimédia [cs.MM]. Université des Sciences et Technologie de Lille - Lille I, 2011. Français (2011)
|
|
BASE
|
|
Show details
|
|
|
| 19 |
Interopérabilité des éléments de métadonnées : vers une approche sémantique
|
|
|
|
BASE
|
|
Show details
|
|
|
| 20 |
Interopérabilité des éléments de métadonnées : vers une approche sémantique
|
|
|
|
BASE
|
|
Show details
|
|
|
|
|
