<p> In this thesis we develop a mathematical framework to express and reason about properties of fault-tolerant computing systems. The main idea behind this mathematical framework is to use axiomatic theories to specify systems. The standard logical operators allow us to describe the basic behavior of the system, while we use deontic predicates on actions to express prescriptions about the system's behavior. Deontic logics have proved to be useful for reasoning about legal and moral systems, where the situation is more or less similar to fault-tolerance: there exists a set of rules that states what the normal behaviours or scenarios are. Violations arise when these rules are not followed and, as a consequence, some actions must be performed to return to a normal or desirable state. We develop our own deontic logic, keeping in mind that we want to use it for specifying fault-tolerant systems. We investigate the properties of this logic, commenting on those that are relevant to the use of the logic in practice. We provide two different deductive systems; one of them is a standard (Hilbert style) deductive system, while the other one is a tableaux system, which can be applied automatically to prove properties of specifications.</p> <p> In any specification language, it is important to have at hand mechanisms which enable designers to modularize the system description; we investigate how to apply these mechanisms to the logics proposed in this thesis, and, in particular, we focus on how the modularization of specifications affects the local prescriptions of a module (or component). We study the problems that arise from the interaction between components. We show that, in some cases, we can guarantee that the locality of violations in a particular component is preserved. Some examples are provided throughout this thesis to illustrate how the ideas described below can be applied in practice. </p> / Thesis / Doctor of Philosophy (PhD)

No description available.

No description available.

The purpose of this research is to improve the performance for the query processing of Cyrano, a prototype deductive object-oriented meta model for Federated Database Systems (FDBSs). The hypothesis was that query optimization techniques such as Semi-Naive algorithm and Magic-Sets Rewrite algorithm could be used to improve the performance of Cyrano prototype query processing. Query optimization has not been used for an FDBS with a deductive object-oriented meta model. Most existing FDBS query optimization techniques are for FDBSs with relational meta models. This research involves two major stages. The first stage was to investigate the existing query processing methodologies and query optimization techniques for FDBSs, deductive databases, and object-oriented databases. The research analyzed the methodologies and techniques of representative works. Two typical systems, one from the object-oriented database family and the other from the deductive object-oriented database family, were studied and analyzed in detail. The survey showed that there had been no work reported on query optimization for FDBSs with deductive object-oriented meta models. The analysis showed that the established query optimization techniques for deductive and object-oriented databases could be viable candidates for query optimization in the Cyrano prototype. The second stage was to develop a new query processing methodology for Cyrano based on the analytical results of the first stage. A new query processing methodology was proposed, and Semi-Naive and Magic-Sets Rewrite algorithms were employed. Experiments showed that the application of the new query processing methodology improved the performance of the Cyrano query processing up to several hundred percent. Furthermore, the new Cyrano query processing methodology is a general methodology for deductive object-oriented data models, and it can well be applied to other FDBSs with deductive object-oriented meta models. In conclusion, the research proves that the performance of the Cyrano prototype query processing can be significantly improved with query optimization. It also suggests that query optimization will improve the performance of query processing of other FDBSs with deductive object-oriented meta models. / Master of Science

Résumé : Au Québec, la situation en termes d’apprentissage des savoirs grammaticaux, et surtout de mobilisation de ces derniers en situation d’écriture, est inquiétante. Pour rendre son intervention plus efficiente, l'enseignant peut choisir une approche pédagogique déductive (explication d'un concept suivi d'exercices) ou inductive (observation d'exemples avant la vérification d'hypothèse et les exercices). Notre objectif principal est d'évaluer les incidences d’une intervention éducative en grammaire selon des approches pédagogiques inductive ou déductive sur l’apprentissage par des élèves de 1re secondaire du complément du nom et son impact dans le développement de la compétence savoir écrire. Notre objet d’enseignement, le complément du nom (CN) est un concept de la grammaire actuelle, dont les caractéristiques facilitent son utilisation réfléchie en rédaction, surtout lors des phases de révision et de réécriture. Une méthodologie mixte de recherche a permis de recueillir des données auprès d'un échantillon de 269 élèves de première secondaire, de même qu’auprès de trois enseignants. Pour cette recherche exploratoire d’épistémologie pragmatique, nous avons réalisé des tests de connaissances, des analyses de rédactions et des entrevues auprès d’élèves et d'enseignants. Les résultats obtenus aux tests de connaissances nous montrent qu’il n’y a pas d’écart significatif entre l’amélioration des élèves ayant vécu l’approche inductive et ceux ayant vécu l’approche déductive, si ce n’est d’un léger avantage en ce qui concerne les accords pour les élèves ayant vécu l’approche déductive. Ce qui a par contre émergé de cette expérimentation est d’une part l’effet évident de l’apprentissage des CN sur leurs mobilisations en écriture, peu importe l’approche. D’autre part, les élèves ayant eu une forte amélioration ont confirmé que pour une approche ou une autre, leur implication cognitive demeure l’élément fondamental de l’efficacité de l’intervention éducative. Nous pouvons donc conclure qu’une approche n’est pas significativement supérieure à l’autre dans le cadre de l’enseignement des CN, mais que l’enseignant doit adapter son approche à la situation en tenant compte du contexte, des apprenants et des aspects de l'objet concernés. // Abstract : The choice of an educational approach by a teacher is a significant factor on student achievement. In Quebec, the situation in terms of apprentissage of grammatical knowledge, and especially using that knowledge in writing situations, is worrying. The success rate for the ministerial writing tests graze 60 %. One possible taxonomies to distinguish pedagogical approaches to teaching grammar lies between the inductive and deductive approaches. Our project has for main objective to assess the impact of an educational intervention according to inductive or deductive teaching approaches on learning, by high school students, of a grammar concept (complément du nom) and its impact on the development of writing competencies. In research, if the deductive approach always results, by the teacher explaining a concept, and the students practicing and being evaluated, the inductive approach is defined differently by the authors. For methodological considerations, and because it's a school tradition, we chose to consider an explicit approach focused on the discovery rather than a more implicit approach. Our teaching object, the « complément du nom » (CN) is a concept of the current grammar, including morphological, semantic and syntactic features, should facilitate thoughtful use for writing, especially during phases of revision and rewriting. For all these reasons, this(?) teaching is relevant of a competency-based program, especially since most of the concept notions are provided in Secondary 1 program by the « Progression des apprentissages » (MELS, 2010). A mixed research methodology was used to collect data from a sample of 269 students from eight classes of Secondary 1 , and of three French teachers. For this exploratory research, we used knowledge tests , reviews process marks by the students on writing productions, and interviews with students and teachers in order to document the impact of the teaching sequences, in terms of knowledge learning and 7 mobilization in writing productions. The comparative approach we used allowed us to assess the extent and nature of learning, according to our independent variable (the deductive and inductive teaching approaches), but also on the interrelation between this variable and other aspects of the educational intervention. The test of knowledge scores show that there is no significant difference between the improvement of students who lived an inductive approach and those who lived the deductive approach, except a slight advantage as regards as morphological characteristics for students who lived the deductive approach. What has emerged in this experiment is firstly the obvious effect of learning on their CN mobilizations in writing, regardless of the approach. On the other hand, students who had a strong improvement confirmed that with an approach or another, their cognitive involvement are fundamental to the effectiveness of the educational intervention. Finally, the quasi-experimental context has limited professional actions of the teachers, and at the same time limited their ability to adapt teaching situations. Those who chose to take certain liberties with the scenarios provided, by professional considerations, are those who have seen the results of their students rise, and that, regardless of the pedagogical approach. We can therefore conclude that an approach was not significantly superior to another for teaching of CN in High school, but the teacher must adapt his approach to the situation, taking into account the context, the learners and the aspects of the learning object.

In this thesis we examine the relationship between hypersequent and some types of labelled sequent calculi for a subset of intermediate logics—logics between intuitionistic (Int), and classical logics—that have geometric Kripke semantics, which we call Int∗/Geo. We introduce a novel calculus for a fragment of first-order classical logic, which we call partially-shielded formulae (or PSF for short), that is adequate for expressing the semantic validity of formulae in Int∗/Geo, and apply techniques from correspondence theory to provide translations of hypersequents, simply labelled sequents and relational sequents (simply labelled sequents with relational formulae) into PSF. Using these translations, we show that hypersequents and simply labelled sequents for calculi in Int∗/Geo share the same models. We also use these translations to justify various techniques that we introduce for translating simply labelled sequents into relational sequents and vice versa. In particular, we introduce a technique called "transitive unfolding" for translating relational sequents into simply labelled sequents (and by extension, hypersequents) which preserves linear models in Int∗/Geo. We introduce syntactic translations between hypersequent calculi and simply labelled sequent calculi. We apply these translations to a novel hypersequent framework HG3ipm∗ for some logics in Int∗/Geo to obtain a corresponding simply labelled sequent framework LG3ipm∗, and to an existing simply labelled calculus for Int from the literature to obtain a novel hypersequent calculus for Int. We introduce methods for translating a simply labelled sequent calculus into a cor- responding relational calculus, and apply these methods to LG3ipm∗ to obtain a novel relational framework RG3ipm∗ that bears similarities to existing calculi from the literature. We use transitive unfolding to translate proofs in RG3ipm∗ into proofs in LG3ipm∗ and HG3ipm∗ with the communication rule, which corresponds to the semantic restriction to linear models.

Dual Processing theory proposes that the ability to over ride associative (System 1) in favour of analytical (System 2) processed in deductive reasoning may depend on inhibitory control. The present study applies this association to a spatial reasoning task by adapting a mental rotation task to a multichoice format including System 1 (mirror) and System 2 (rotated image) responses. Fifty undergraduate volunteers from the University of Canterbury responded to a Stroop task as a measure of inhibitory control that was compared with System 1 and System 2 responding from a spatial and a deductive reasoning task. It was expected that people with weaker inhibitory potential would make more System 1 and fewer System 2 responses in both deductive and visual-spatial reasoning tasks. Contrary to expectation System 2 responding dominated for both tasks and correlations between both reasoning tasks and measures of inhibitory control were non-significant. The differing idiosyncratic demands of each task may have obscured any common variables associated with inhibitory control. This research initiated a test for the presence of System 1 and System 2 in spatial reasoning.

This thesis takes part in the formal verification of parallel programs. The aim of formal verification is to ensure that a program will run as it should, without making mistakes, blocking, or terminating abnormally. This is even more important in the parallel computation field, where the cost of calculations can be very high. The BSP model (Bulk Synchronous Parallelism) is a model of parallelism well suited for the use of formal methods. It guarantees a structure in the parallel program, by organising it into super-steps, each of them consisting of a phase of computations, then communications between the processes. In this thesis, we chose to extend an existing tool to adapt it for the proof of BSP programs. We based ourselves on Why, a VCG (verification condition generator) that has the advantage of being able to interface with several automatic provers and proof assistants to discharge the proof obligations. There are multiple contributions in this thesis. In a first part, we present a comparison of the existing BSP libraries, in order to show the most used BSP primitives, which are the most interesting to formalise. We then present BSP-Why, our tool for the proof of BSP programs. This tools uses a generation of a sequential program to simulate the parallel program in input, thus allowing the use of Why and the numerous associated provers to prove the proof obligations. We then show how BSP-Why can be used to prove the correctness of some basic BSP algorithms, and also on a more complex example, the generation of the state-space (model-checking) of systems, especially for security protocols. Finally, in order to ensure the greatest confidence in the BSP-Why tool, we give a formalisation of the language semantics, in the Coq proof assistant. We also prove the correctness of the transformation used to go from a parallel program to a sequential program

To obtain information regarding the effects of two divergent thought processes used in a college mathematics course for prospective elementary school teachers, this study compared the effectiveness of an adaptation of the traditional, deductive teaching method with that of an inductive method reflecting the recommendations of the Committee on the Undergraduate Program in Mathematics. In the spring semester of 1973, two sections of Mathematics for Elementary Teachers I, at Cameron College, Lawton, Oklahoma, served as experimental groups to test the two adaptations. The course followed the Committee on the Undergraduate Program in Mathematics recommendations for a first course in mathematics for prospective elementary teachers.

Cette thèse vise à contribuer à l’approche DDL (Data-Driven Learning) dans l’enseignement du lexique en FLE. Dans le cadre de l’approche DDL, on fait appel aux corpus pour enseigner différentes composantes d’une langue. Le lexique, étant un des premiers besoins d’un apprenant, car il donne accès à la communication en langue étrangère, fait l’objet de nombreux travaux de recherche actuels en linguistique et en didactique. L’idiomaticité, trait constitutif de toutes les langues, se manifeste sous forme d’expressions variées. Elle relève du champ de la lexicologie, et plus spécifiquement de la phraséologie. La linguistique de corpus permet d’observer ce fait de langue dans un cadre structure/sens. Les expressions idiomatiques en général, et en particulier les collocations, sont mises au centre de la démarche didactique dans cette thèse. Les collocations à verbe support restent une source d’erreurs importante même aux niveaux avancés d’apprentissage. Le matériel didactique présenté aux lecteurs de cette étude cherche à promouvoir l’exploitation directe des corpus bilingues par les apprenants en classe afin d’identifier ces collocations en L1 et en L2, de les comprendre, de trouver des correspondances et de les employer de manière appropriée. L’approche comparative français-russe renforcée par une observation des lignes de concordance issues de corpus authentiques devraient permettre une meilleure acquisition des faits linguistiques visés. Ce travail s’inscrit dans une perspective d’apprentissage déductif et d’autonomisation des apprenants. / This thesis aims to contribute to the DDL (Data-Driven Learning) approach in French vocabulary teaching. In the framework of the DDL approach we use corpora to teach different language phenomena. Vocabulary, one of the immediate needs of a language learner because it makes a communication in a foreign language possible, has become a popular research theme in the fields of linguistics and language teaching. Idiomaticity, an inherent part of all languages, manifests through various expressions. Phraseology studies different ways of expressing idiomaticity. Corpus linguistics permits to observe this language phenomenon in a structure/sense framework. Idiomatic expressions in general and collocations in particular are the heart and the main focus of the teaching perspective described in this thesis. Even advanced language learners make errors in light verb constructions. The teaching material presented in this study seeks to promote the search in bilingual corpora in the classroom in order to identify these collocations in L1 and in L2, to understand them, to find equivalents and finally, to use them correctly. A comparative French-Russian approach reinforced by a study of concordance lines from authentic corpora might contribute to better understanding of a particular language feature. This study falls in line with deductive learning practices and with the learners’ autonomisation perspective.