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.

Le terme agent a été introduit pour masquer l'origine diverse des participants (produits logiciels ou humains) intervenant dans une interaction. Un agent est considéré comme une boîte noire capable de contrôler son comportement. Cette propriété, appelée autonomie, est en contradiction avec la possibilité de contrôler l'agent depuis l'extérieur. Dans cette thèse, nous proposons la norme sociale comme une solution de compromis à ce conflit. Une norme a le double rôle d'informer quel est le comportement désirable et d'influencer les agents pour qu'ils l'adoptent. Cette thèse comprend deux parties, la première introduit les concepts, la seconde propose les outils. La première partie est centrée autour du paradigme de la conception sociale des Systèmes Multi-Agents (SMA). Nous montrons comment les notions de dépendance sociale, d'organisation et de rôle permettent de mieux décrire l'interaction entre agents. La notion de norme est définie dans ses diférentes acceptions : domaine juridique, sécurité informatique, systèmes distribués, et SMA. Ensuite, nous présentons nos choix et nos solutions concernant l'interaction normative. Les structures architecturales qui en résultent sont appelées Système d'Agents Normatifs (SAN). Nous montrons quels en sont les acteurs majeurs et quels sont les outils pour les construire. La description des normes utilise les concepts d'action, de temps, d'obligation et d'agence. La deuxième partie montre comment ces concepts sont formalisés dans la littérature (p. ex. logique temporelle, déontique, de l'action) et présente leurs inconvénients majeurs. Ensuite, nous proposons un modèle temporel pour décrire l'interaction normative en expliquant les choix des éléments utilisés et nous montrons son applicabilité. Le modèle est utilisé pour produire les outils nécessaires à la construction des SAN : le monitoring des comportements des agents, la détection des violations, l'ordonnancement déontique, la communication normative.

Maintenant que le Programme de formation de l'école québécoise est implanté depuis plusieurs années au niveau primaire, il fait l'objet d'évaluation. Par contre, le domaine de l'évaluation de programme se fait souvent remettre en question par rapport à sa capacité de produire des recommandations pertinentes. Il existe donc un besoin de recherche fondamentale dans le domaine de l'évaluation de programme. Pour améliorer l'évaluation de programme dans le domaine de l'éducation, il est essentiel d'effectuer de la recherche fondamentale dans le domaine de l'évaluation de programme. Fournier (1995) et Hurteau et Houle (2006) ont effectué des recherches qui visaient la pratique en évaluation de programme. Leurs réflexions portaient sur la distinction entre ce qui constitue la pratique et ce qui a été élaboré pour la soutenir. Par contre, il existe une confusion dans la littérature à ce niveau car cette distinction n'a jamais fait l'objet d'une étude empirique. Notre recherche s'inscrit dans cette perspective afin d'établir un cadre de référence pertinent et d'examiner si le processus propre à l'évaluation de programme diffère de l'application de son instrumentation. Nous avons analysé des réponses à un scénario simulé. Ces réponses représentent trois orientations théoriques: méthodes, jugement de valeur et utilisation. Même si ces orientations ne sont pas nécessairement des catégories mutuellement exclusives, chacune s'attarde à une perspective distincte. L'orientation théorique associée aux méthodes utilise une approche expérimentale ou quasi-expérimentale où la rigueur est fondamentale. L'orientation du jugement de valeur souligne l'importance de porter un jugement sur la valeur du programme évalué afin d'offrir l'information nécessaire à une prise de décision. L'orientation théorique de l'utilisation s'attarde à l'utilisation des résultats de l'évaluation afin d'obtenir un changement au niveau organisationnel. Des grilles d'analyse sont utilisées pour identifier les éléments du processus de l'évaluation de programme et une analyse croisée des données quantitatives démontre le taux de présence de chaque élément dans chaque orientation théorique. Ces données sont ensuite appliquées à une analyse de contenue et font l'objet d'une analyse qualitative. Les composantes de l'instrumentation sont aussi appliquées à chaque orientation théorique. Les standards de pratique provenant du Joint Committee servent de cadre de référence pour identifier les variances et les choix méthodologiques sont étudiés à partir de critères prédéterminés. Les résultats démontrent qu'à un niveau global les trois orientations théoriques ont présenté les éléments du processus de l'évaluation de programme. Par contre, des différences ont été identifiées dans l'orientation de l'utilisation. C'est à souhaiter que la présente recherche éclaire notre sujet en stimulant la discussion et de futures études.

Ce travail montre comment un formalisme logique, la logique de configuration, est intégré au sein d'un outil de gestion de configuration de réseaux, ValidMaker. Le principal objectif de ce travail est de démontrer que la logique de configuration est particulièrement bien adaptée à la vérification automatique de configuration de réseaux. À cette fin, nous développons un exemple réel de configuration de réseaux et nous trouvons des règles qui doivent être vérifiées pour qu'une telle configuration soit fonctionnelle. Ensuite, nous expliquons comment nous avons implanté la logique de configuration dans ValidMaker et nous illustrons le fonctionnement de notre algorithme de vérification.

L'objectif de notre mémoire est d'apporter une contribution épistémologique et éventuellement pédagogique à l'enseignement de la logique. La philosophie développe des logiques formelles, des normes idéales du raisonnement, tandis que la psychologie découvre des tendances naturelles de l'esprit humain à raisonner de manière spécifique, lesquelles sont parfois conformes aux lois de la logique et, parfois pas. De quelle manière sont compatibles ces approches? Le problème soulevé dans ce contexte, et qui est traité dans ce mémoire, est celui de la compatibilité ou de l'incompatibilité entre l'approche psychologique descriptive et l'approche philosophique normative du raisonnement. Nous développons une perspective compatibiliste et pensons ses conséquences pour la logique et son enseignement. À cette fin, nous présentons dans le premier chapitre la perspective épistémologique naturaliste modérée dans laquelle nous nous situons et qui motive notre projet. Nous verrons dans le chapitre II les normes qui régissent l'implication logique. Les résultats issus d'expérimentations psychologiques donnent lieu à différentes théories du raisonnement déductif, nous présentons au troisième chapitre deux théories psychologiques qui tentent d'expliquer nos capacités logiques intuitives, soit, la théorie de la logique mentale, ainsi que la théorie des modèles mentaux. Grâce aux techniques récentes d'imagerie cérébrale, les bases neuronales du raisonnement seront utiles afin de mieux juger de la pertinence des théories de la logique intuitive. Ces techniques d'imagerie cérébrale ont permis de découvrir plusieurs processus neuronaux intervenant dans le raisonnement et ont ainsi appuyé la théorie des processus duaux. Nous présentons cette théorie et la défendrons au chapitre quatre, en montrant ses avantages sur les théories précédentes. Enfin, au dernier chapitre, nous montrons les conséquences épistémologiques de la théorie des processus duaux et tentons une ouverture sur une éventuelle révision de l'enseignement de la logique. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : raisonnement logique, sophisme, raisonnement conditionnel, psychologie du raisonnement, neurosciences.

Le présent mémoire de maîtrise déposé au département de philosophie de l'Université du Québec à Montréal s'inscrit dans le domaine de la théorie de l'argumentation et des logiques non formelles. Il traite spécifiquement du concept de sophisme. Traditionnellement conçu comme une forme typique de mauvais raisonnement, le sophisme est un concept fondamental dans l'enseignement de la pensée critique et de l'argumentation. Cette conception traditionnelle fut toutefois remise en question à la seconde moitié du XXe siècle par des logiciens et des philosophes. Il semble qu'elle ne rende pas adéquatement compte des sophismes et présente des faiblesses tant sur les plans théoriques que pratiques. Suite à cette remise en question, plusieurs projets de recherche furent mis sur pied pour répondre au problème. La théorie pragma-dialectique de l'argumentation fut certainement des plus fertiles. Concevant l'argumentation dans un cadre dialectique et intégrant les outils descriptifs de la pragmatique linguistique, elle propose une redéfinition du concept problématique. Selon elle, le sophisme est une manœuvre argumentative illicite venant freiner le processus de résolution de conflits d'opinion par la discussion rationnelle. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Sophisme, Argumentation, Pensée critique, Logique

Texte remanié de: Th. doct.--Sci. du langage--Paris--EHESS, 1995. Titre de soutenance : Réinterprétation et scalarité, les instructions de relecture dans la langue. / Bibliogr. p. 261-276.