Cette thèse propose trois contributions aux preuves mathématiques assistées par ordinateur. On s'intéresse non seulement aux preuves reposant sur le calcul, mais aussi aux preuves formelles, qui sont àla fois produites et vérifiées à l'aide d'un logiciel appelé assistant à la preuve.Dans la première partie, nous illustrons le thème de l'expérimentation au service de la preuve en nous intéressant au problème de la complexité des algorithmes de multiplication matricielle. Cette question a historiquement été posée de manière de plus en plus abstraite: les approches modernes ne construisent pas d'algorithmes explicites mais utilisent des résultats théoriques pour améliorer la borne inférieure sur la célèbre constante oméga. Nous sommes revenus à une approche plus pratique en essayant de programmer certains des algorithmes impliqués par ces résultats théoriques. Cette approche expérimentale a révélé un motif inattendu dans des algorithmes existants. Alors que ces algorithmes contiennent une nouvelle variable epsilon dont la présence est réputée les rendre impraticables pour des tailles de matrices raisonnables, nous avons découvert que nous pouvions construire des algorithmes de multiplication matricielle en parallèle sans epsilon avec une complexité asymptotique qui peut théoriquement battre l'algorithme de Strassen pour les multiplications. Un sous-produit de cette exploration est un outil symbolique en Ocaml qui peut analyser, composer et exporter des algorithmes de multiplication matricielle. Nous pensons aussi qu'il pourrait être utilisé pour construire de nouveaux algorithmes pratiques de multiplication matricielle.Dans la deuxième partie, nous décrivons une preuve formelle de l'irrationalité de la constante zeta(3), en suivant la démonstration historique due à Apéry. L'étape cruciale de cette preuve est d'établir que deux suites de nombres rationnels satisfont une surprenante récurrence commune. Il est en fait possible de "découvrir"cette récurrence en utilisant des algorithmes symboliques, et leurs implémentations existantes dans un système de calcul formel. De fait,ce travail constitue un exemple d'une approche dite sceptique de la démonstration formelle de théorèmes, dans lequel des calculs sont principalement réalisés par un logiciel efficace de calcul formel puis vérifiés formellement dans un assistant à la preuve. Incidemment, ce travail questionne la valeur des certificats de télescopage créatif comme preuves complètes d'identités. Cette preuve formelle est également basée sur de nouvelles bibliothèques de mathématiques,formalisées pour ses besoins. En particulier, nous avons formalisé et simplifié une étude du comportement asymptotique de la suite ppcm(1,.., n). Ce travail est conduit dans l'assistant à la preuve Coq et prolonge les bibliothèques Mathematical Components.Dans la dernière partie, nous présentons une procédure qui calcule les approximations d'une classe d'intégrales propres et impropres tout en produisant simultanément un preuve formelle Coq de la correction du résultat de ce calcul. Cette procédure utilise une combinaison d'arithmétique d'intervalles et d'approximations polynomiales rigoureuses de fonctions. Ce travail utilise crucialement les possibilités de calculer efficacement à l'intérieur de la logique sous-jacente au système Coq. Il s'agit d'une extension de la bibliothèque CoqInterval d'approximation numérique d'une classe d'expressions réelles. Sa mise en œuvre a également donné lieu à des extensions de la bibliothèque Coquelicot d'analyse réelle, notamment pour améliorer le traitement des intégrales impropres. Nous illustrons l'intérêt de cet outil et ses performances en traitant des exemples standards mais non triviaux de la littérature, sur lesquels d'autres outils se sont en certains cas révélés incorrects. / This thesis proposes three contributions to computer-aidedmathematical proofs. It deals, not only with proofs relying oncomputations, but also with formal proofs, which are both produced andverified using a piece of software called a proof assistant.In the first part, we illustrate the theme of experimentation at theservice of proofs by considering the problem of the complexity ofmatrix multiplication algorithms. This problem has historically beenapproached in an increasingly abstract way: modern approaches do notconstruct algorithms but use theoretical results to improve the lowerbound on the famous omega constant. We went back to a more practicalapproach by attempting to program some of the algorithms implied bythese theoretical results. This experimental approach reveals anunexpected pattern in some existing algorithms. While these algorithmscontain a new variable epsilon whose presence is reputed to renderthem inefficient for the purposes of reasonable matrix sizes, we havediscovered that we could build matrix multiplication algorithms inparallel without epsilon's with an asymptotic complexity which cantheoretically beat Strassen's algorithm in terms of the number ofmultiplications. A by-product of this exploration is a symbolic toolin Ocaml which can analyze, compose and export matrix multiplicationalgorithms. We also believe that it could be used to build newpractical algorithms for matrix multiplication.In the second part, we describe a formal proof of the irrationality ofthe constant zeta (3), following the historical demonstration due toApéry. The crucial step of this proof is to establish that twosequences of rational numbers satisfy a suprising commonrecurrence. It is in fact possible to "discover" this recurrence usingsymbolic algorithms, and their existing implementations in a computeralgebra system. In fact, this work is an example of a skepticalapproach to the formal proof of theorems, in which computations aremainly accomplished by an efficient computer algebra program, and thenformally verified in a proof assistant. Incidentally, this workquestions the value of creative telescoping certificates as completeproofs of identities. This formal proof is also based on newmathematical libraries, which were formalised for its needs. Inparticular, we have formalized and simplified a study of theasymptotic behaviour of the sequence lcm(1,..., n). This work isdeveloped in the Coq proof assistant and extends the MathematicalComponents libraries.In the last part, we present a procedure which computes approximationsof a class of proper and improper integrals while simultaneouslyproducing a Coq formal proof of the correction of the result of thiscomputation. This procedure uses a combination of interval arithmeticand rigorous polynomial approximations of functions. This work makescrucial use of the possibility to efficiently compute inside Coq'slogic. It is an extension of the CoqInterval library providingnumerical approximation of a class of real expressions. Itsimplementation has also resulted in extensions to the Coquelicotlibrary for real analysis, including a better treatment of improperintegrals. We illustrate the value of this tool and its performanceby dealing with standard but nontrivial examples from the literature,on which other tools have in some cases been incorrect.

De nombreux bugs informatiques ont mis en lumière le besoin de certifier les programmes informatiques et la vérification de programmes a connu un développement important au cours des quarante dernières années. Parmi les méthodes possibles, on trouve le model-checking, développé par Clarke et Emerson dans les années 80. Le model-checking consiste à trouver un modèle abstrait pour le système et un formalisme logique pour le comportement puis à vérifier si le modèle vérifie la propriété exprimée dans la logique. La difficulté consiste alors à développer des algorithmes efficaces pour les différents formalismes. Nous nous intéresserons en particulier au formalisme logique de strategy Logic SL, utilisée sur les systèmes multiagents. SL est particulièrement expressif de par son traitement des stratégies (comportements possibles pour les agents du système) comme des objets du premier ordre. Dans sa définition, divers choix sémantiques sont faits et, bien que ces choix se justifient, d'autres possibilités n'en sont pas plus absurdes: tel ou tel choix donne telle ou telle logique et chacune permet d'exprimer des propriétés différentes. Dans cette thèse, nous étudions les différentes implications des différents choix sémantiques. Nous commencerons par introduire SL et préciserons l'étendue des connaissances actuelles. Nous nous intéresserons ensuite aux possibilités non explorées par la sémantique originale. Nous étudierons aussi la logique sur des systèmes quantitatifs (ajout de contraintes d'énergie et de contraintes de compteurs). Finalement, nous examinerons la question des dépendances dans SL[BG] (un fragment de SL). / With the proliferation of computerised devices, software verification is more prevalent than ever. Since the 80's, multiple costly software failures have forced both private and public actors to invest in software verification. Among the main procedures we find the model-checking, developed by Clarke and Emerson in the 80's. It consists in abstracting both the system into a formal model and the property of expected behaviour in some logical formalism, then checking if the property's abstraction holds on the system's abstraction. The difficulty lies in finding appropriate models and efficient algorithms. In this thesis, we focus on one particular logical formalism: the Strategy Logic SL, used to express multi-objectives properties of multi-agents systems. Strategy Logic is a powerful and expressive formalism that treats strategies (i.e. potential behaviours of the agents) like first-order objects. It can be seen as an analogue to first-order logic for multi-agents systems. Many semantic choices were made in its definition without much discussion. Our main contributions are relative to the possibilities left behind by the original definition. We first introduce SL and present some complexity results (including some of our owns). We then outline some other semantic choices within SL's definition and study their influence. Third, we study the logic's behaviour under quantitative multi-agents systems (games with energy and counter constraints). Finally, we address the problem of dependencies within SL[BG], a fragment of SL.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Québec Université Laval, Bibliothèque 2014

De nos jours, la transmission du patrimoine culturel immatériel reste une problématique internationale qui touche à la fois la question de conservation de notre passé et la question actuelle du développement de l’économie créative. Cependant, cette transmission se réalise à travers de différents biais éducatifs, qui pourraient être formels ou non formels, qui pourraient viser à former les professionnels ou les amateurs. Cette présente thèse a choisi le patrimoine artisanal et sa transmission comme le sujet de recherche, avec une attention particulière portée sur les formations formelles et non formelles, qui sont considérées comme les dispositifs de transmission professionnelle du patrimoine artisanal, le chercheur s’est approché vers un terrain spécifique, celui de l’artisanat de la céramique et a mené une étude comparative sur les formations formelles et non formelles, organisées dans les deux sociétés contrastées dont celle de la Chine et celle de la France, qui transmettent cet artisanat. En analysant les discours de 28 céramistes dont 14 céramistes indépendants (7 Chinois et 7 Français) et 14 céramistes salariés (7 Chinois et 7 Français), cette thèse vise à faire comprendre quels sont actuellement les modes (formels et non formels) de formation professionnelle en artisanat de la céramique, les plus respectivement favorisés par les céramistes praticiens en Chine et en France. Des perspectives sont dégagées sur les similarités et les écarts dans les comportements et les routines des activités de transfert, d’appropriation des savoirs et des savoir-faire concernés et de création à partir des savoirs et des savoir-faire transmis de chacun des modes de formation, employés dans ces deux contextes sociaux dissemblables que sont ceux de la Chine et de la France. / Today, the transmission of intangible cultural heritage remains an international issue that touches not only the preservation of the past but also the practical question of the development of creative economy. However, this transmission can be realized via various educational channels, whether it is formal or non-formal, which could aim to train professionals or amateurs. This thesis decided to choose the artisanal heritage and its transmission as the research subject, with a particular focus on formal and non-formal formations, which are considered as devices for the professional transmission of the artisanal heritage. The author advanced the topic towards a specific field, that of the craft of ceramics and carried out a comparative study on formal and non-formal formations, organized under the context of two contrasting societies, that of China and France, which transmit this craft. By analyzing the talks of 28 ceramists, including 14 independent ceramists (7 Chinese and 7 French) and 14 ceramists-employees (7 Chinese and 7 French), this thesis aims to offer a clear understanding on what are the prevailing modes (formal and non-formal) of vocational training in the craft of ceramics, that favored mostly by the ceramic practitioners in China and France. Observations and perspectives have been made on the similarities and differences in terms of practices and routines of transfer, acquisition, and creation of knowledge and the know-how of each of the training mode, adopted under the different social contexts of China and France, which are marked by sharp contrasts.