Thèse--Doct.-ing.--Paris 6, 1971. / Bibliogr.

Dans ce mémoire, nous examinons la dimension affective de la réfutation socratique et son rôle dans l’éducation. Nous voyons comment la réfutation traite du problème de la double-ignorance, et ce pour quoi elle pourrait être efficace pour provoquer le désir de connaître. Nous examinons la place que prend la honte et la colère dans le processus de même que les obstacles à la réfutation. / In this work, we examine the affective aspect of Socratic elenchus and its role in education. We see howrefutation deals with the problem of double ignorance, and how it could be an effective way to provoke thedesire to know. We examine the place that shame and anger take in the process as well as the obstaclesto refutation.

Depuis Frege (1893), les développements de la logique moderne ne se sont pas montrés à la hauteur de ses ambitions à l’égard de la détermination des objets, la temporalité, l’action, le langage et, d’une façon suréminente, le mouvement. Pour Rôdl (2012), la logique frégéenne et la logique moderne en général ne peuvent pas formaliser le mouvement parce que, comme il le démontre bien, elles reposent essentiellement sur un ordre logico-déductif. Nous voulons montrer que la source de cette faille n’est pas l’ordre logico-déductif de la logique moderne mais la thématisation de ses éléments selon les catégories pré-établies d’objet, de prédicat, de proposition et de valeur de vérité. La question suivante peut alors légitimement se poser : la logique peut-elle, tout en restant moderne, c’est-à-dire formaliste, symbolique et calculatoire, faire émerger la forme de la structure prédicative d’une proposition de façon à résoudre les fractures métaphysiques qui lui sont imputées dont, en premier lieu, celle du mouvement ? Nous proposons de répondre à l’affirmative sous la condition nécessaire d’une déthématisation de la logique, c’est-à-dire du passage d’une logique des prédicats à une logique des opérateurs. Les travaux de Déscles sur la théorie des opérateurs aspecto-temporels, formalisée dans le cadre de la logique combinatoire, répondent à cette condition. On montre comment il est alors possible de résoudre les fractures métaphysiques et de poser les jalons d’une nouvelle logique du mouvement. / Since Frege (1893), the developments of modern logic have not lived up to its ambitions with regard to the determination of objects, temporality, action, language and, priorly, movement. For Rödl (2012), Fregean logic, and modern logic in general, can not formalize the movement because, as he shows it well, they are essentially based on a logico-deductive order. We want to show that the source of the fault is not the logico-deductive order of modern logic but its pre-theming of its tokens according to the categories of object, predicate, proposition and truth value. The following question can then legitimately be asked: can logic, while remaining modern, that is to say, formal, symbolic and computational, exhibit the form of the predicative structure of a proposition in order to solve the metaphysical fractures that it is charged with including, in the first place, that of movement? We propose to answer that it is possible under the condition that logic be unthemed, that is to say going from a predicate logic to an operator logic. The work of Desclés on the theory of aspecto-temporal operators, formalized in the context of combinatorial logic, meet this condition. It shows how it is possible to solve metaphysical fractures and to lay the foundations of a new logic of movement.

Dans l'histoire générale de la logique, l'étape que constituent les travaux des logiciens arabes du Moyen Âge demeure en grande partie encore aujourd'hui terra incognita (Rescher, 1963). Portant sur la notion de proposition chez ces auteurs, la thèse se veut une contribution à l'exploration de cette étape importante du développement de la logique. Dans une première partie, on y trouve un exposé analytique de leur théorie de la signification. Une deuxième partie examine l'enseignement particulier des commentateurs arabes d'Aristote à propos des parties intégrales de la proposition. Une troisième et dernière partie, enfin, analyse les diverses définitions de la proposition que l'on trouve dans les écrits de cette époque. Les résultats de cette recherche tendent à montrer que la logique arabe, du moins pour le sujet et l'époque étudiés, même si elle a sa source chez Aristote, n'en demeure pas moins très fortement influencée dans son développement par le contexte général de la pensée arabo-musulmane, contexte dominé par la langue arabe (et sa grammaire) et la religion islamique (et son texte sacré, le Coran).

La réduction continuelle des dimensions dans les technologies CMOS a ouvert la porte à la conception de circuits complexes multi-cœurs (SoC). Malheureusement dans les technologies nanométriques, les performances des systèmes intégrés après fabrication ne sont pas complètement prédictibles. En effet, les variations des procédés de fabrication sont très importantes aux échelles des puces. Par conséquent, la conception de tels systèmes dans les technologies nanométriques est désormais contrainte par de nombreux paramètres tels que la robustesse aux variations des procédés de fabrication et la consommation d'énergie. Ceci implique de disposer d'algorithmes efficaces, intégrés dans la puce, susceptibles d'adapter le comportement du système aux variations des charges des processeurs tout en faisant face simultanément aux variations des paramètres qui ne peuvent pas être prédits ou modélisées avec précision au moment de la conception. Dans ce contexte, ce travail de thèse porte sur la conception de systèmes dit " GALS " (Globally Asynchronous Locally Synchronous) conçus autour d'un réseau de communication intégré à la puce (Network-on-Chip ou NoC) exploitant les nouvelles générations de technologie CMOS. Une nouvelle méthode permettant de contrôler dynamiquement la vitesse des différents îlots du NoC grâce à un contrôle de la tension et de la fréquence en fonction de la qualité locale des procédés de fabrication sur chaque îlot est proposée. Cette technique de contrôle permet d'améliorer les performances du système en consommation, et d'augmenter son rendement en fabrication grâce à l'utilisation des synergies au sein du système intégré. La méthode de contrôle est basée sur l'utilisation d'un anneau asynchrone programmable capable de prendre en compte la charge de travail dynamique et les effets de la variabilité des procédés de fabrication. Le contrôleur évalue en particulier la limite supérieure de fréquence de fonctionnement pour chaque domaine d'horloge. Ainsi, il n'est plus nécessaire de garantir les performances temporelles de chaque nœud au moment de la conception. Cela relâche considérablement les contraintes de fabrication et permet du même coup l'amélioration du rendement.

Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal.

Mémoire numérisé 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.

Cette thèse étudie des formalismes logiques exprimant des propriétés sur des programmes. L'intention originale de ces logiques est de vérifier formellement la correction de programmes manipulant des pointeurs. Dans l'ensemble, il ne sera pas proposé de méthode de vérification applicable dans cette thèse- nous donnons plutôt un éclairage nouveau sur la logique de séparation, une logique pour triplets de Hoare. Pour certains fragments essentiels de cette logique, la complexité et la décidabilité du problème de la satisfiabilité n'étaient pas connus avant ce travail. Aussi, sa combinaison avec certaines autres méthodes de vérification était peu étudiée. D'une part, dans ce travail nous isolons l'opérateur de la logique de séparation qui la rend indécidable. Nous décrivons le pouvoir expressif de cette logique, en la comparant à des logiques du second ordre. D'autre part, nous essayons d'étendre des fragments décidables de la logique de séparation avec la une logique temporelle et avec l'aptitude à décrire les données. Cela nous permet de donner des limites à l'utilisation de la logique de séparation. En particulier, nous donnons des limites à la création de logiques décidables utilisant ce formalisme combiné à une logique temporelle ou à l'aptitude à décrire les données. / This thesis studies logics which express properties on programs. These logics were originally intended for the formal verification of programs with pointers. Overall, no automated verification method will be proved tractable here- rather, we give a new insight on separation logic. The complexity and decidability of some essential fragments of this logic for Hoare triples were not known before this work. Also, its combination with some other verification methods was little studied. Firstly, in this work we isolate the operator of separation logic which makes it undecidable. We describe the expressive power of this logic, comparing it to second-order logics. Secondly, we try to extend decidable subsets of separation logic with a temporal logic, and with the ability to describe data. This allows us to give boundaries to the use of separation logic. In particular, we give boundaries to the creation of decidable logics using this logic combined with a temporal logic or with the ability to describe data.

Cette thèse de théorie de la démonstration étudie les interactions entre le λ-calcul différentiel d'Ehrhard et Regnier d'un côté, et certaines émanations calculatoires de la logique classique (le λμ-calcul de Parigot et le λ-barre-μ-calcul de Herbelin) de l'autre. L'étude est initiée et guidée par la décomposition de ces calculs dans des extensions de la logique linéaire de Girard.<br /><br />Dans une première partie, on définit un cadre commun pour ces extensions, dans le formalisme des réseaux d'interaction de Lafont, et on y rappelle des résultats de la littérature ou du folklore. On donne en particulier la traduction du λμ-calcul et du λ-barre-μ-calcul dans les réseaux polarisés de Laurent et celle du fragment finitaire du λ-calcul différentiel dans les réseaux différentiels d'Ehrhard et Regnier.<br /><br />Dans la deuxième partie, on introduit les réseaux différentiels polarisés (RDP), comme l'extension par une polarisation à la Laurent des réseaux différentiels. La pertinence des règles de réduction nouvelles est soulignée par l'étude d'un modèle dénotationnel commun aux réseaux différentiels et aux réseaux polarisés.<br /><br />Enfin, on présente trois calculs de termes, chacun pouvant être considéré comme une lecture en arrière de tout ou partie des interactions définies par les RDP : un λμ-calcul différentiel, qui correspond à la réunion des réseaux différentiels et des réseaux polarisés ; un λ-barre-μ-calcul avec produit de convolution sur les piles, qui fait intervenir la structure de bigèbre des types polarisés introduite dans les RDP, mais pas la dérivée ; enfin, un λ-barre-μ-calcul différentiel qui développe toute l'expressivité des RDP.