Region Connection Calculus: Composition Tables and Constraint Satisfaction Problems

Qualitative spatial reasoning (QSR) is an important field of AI that deals with qualitative aspects of spatial entities. Regions and their relationships are described in qualitative terms instead of numerical values. This approach models human based reasoning about such entities closer than other approaches. Any relationships between regions that we encounter in our daily life situations are normally formulated in natural language. For example, one can outline one's room plan to an expert by indicating which rooms should be connected to each other. Mereotopology as an area of QSR combines mereology, topology and algebraic methods. As mereotopology plays an important role in region based theories of space, our focus is on one of the most widely referenced formalisms for QSR, the region connection calculus (RCC). RCC is a first order theory based on a primitive connectedness relation, which is a binary symmetric relation satisfying some additional properties. By using this relation we can define a set of basic binary relations which have the property of being jointly exhaustive and pairwise disjoint (JEPD), which means that between any two spatial entities exactly one of the basic relations hold. Basic reasoning can now be done by using the composition operation on relations whose results are stored in a composition table. Relation algebras (RAs) have become a main entity for spatial reasoning in the area of QSR. These algebras are based on equational reasoning which can be used to derive further relations between regions in a certain situation. Any of those algebras describe the relation between regions up to a certain degree of detail. In this thesis we will use the method of splitting atoms in a RA in order to reproduce known algebras such as RCC15 and RCC25 systematically and to generate new algebras, and hence a more detailed description of regions, beyond RCC25.

L-Fuzzy Relations in Coq

Heyting categories, a variant of Dedekind categories, and Arrow categories provide a convenient framework for expressing and reasoning about fuzzy relations and programs based on those methods. In this thesis we present an implementation of Heyting and arrow categories suitable for reasoning and program execution using Coq, an interactive theorem prover based on Higher-Order Logic (HOL) with dependent types. This implementation can be used to specify and develop correct software based on L-fuzzy relations such as fuzzy controllers. We give an overview of lattices, L-fuzzy relations, category theory and dependent type theory before describing our implementation. In addition, we provide examples of program executions based on our framework.

Application du concept des transactions pour la modélisation et la simulation multicoeur des systèmes sur puce

Avec la complexité croissante des systèmes sur puce, de nouveaux défis ne cessent d’émerger dans la conception de ces systèmes en matière de vérification formelle et de synthèse de haut niveau. Plusieurs travaux autour de SystemC, considéré comme la norme pour la conception au niveau système, sont en cours afin de relever ces nouveaux défis. Cependant, à cause du modèle de concurrence complexe de SystemC, relever ces défis reste toujours une tâche difficile. Ainsi, nous pensons qu’il est primordial de partir sur de meilleures bases en utilisant un modèle de concurrence plus efficace. Par conséquent, dans cette thèse, nous étudions une méthodologie de conception qui offre une meilleure abstraction pour modéliser des composants parallèles en se basant sur le concept de transaction. Nous montrons comment, grâce au raisonnement simple que procure le concept de transaction, il devient plus facile d’appliquer la vérification formelle, le raffinement incrémental et la synthèse de haut niveau. Dans le but d’évaluer l’efficacité de cette méthodologie, nous avons fixé l’objectif d’optimiser la vitesse de simulation d’un modèle transactionnel en profitant d’une machine multicoeur. Nous présentons ainsi l’environnement de modélisation et de simulation parallèle que nous avons développé. Nous étudions différentes stratégies d’ordonnancement en matière de parallélisme et de surcoût de synchronisation. Une expérimentation faite sur un modèle du transmetteur Wi-Fi 802.11a a permis d’atteindre une accélération d’environ 1.8 en utilisant deux threads. Avec 8 threads, bien que la charge de travail des différentes transactions n’était pas importante, nous avons pu atteindre une accélération d’environ 4.6, ce qui est un résultat très prometteur.

A Categorical Framework for the Specification and the Verification of Aspect Oriented Systems

Un objectif principal du génie logiciel est de pouvoir produire des logiciels complexes, de grande taille et fiables en un temps raisonnable. La technologie orientée objet (OO) a fourni de bons concepts et des techniques de modélisation et de programmation qui ont permis de développer des applications complexes tant dans le monde académique que dans le monde industriel. Cette expérience a cependant permis de découvrir les faiblesses du paradigme objet (par exemples, la dispersion de code et le problème de traçabilité). La programmation orientée aspect (OA) apporte une solution simple aux limitations de la programmation OO, telle que le problème des préoccupations transversales. Ces préoccupations transversales se traduisent par la dispersion du même code dans plusieurs modules du système ou l’emmêlement de plusieurs morceaux de code dans un même module. Cette nouvelle méthode de programmer permet d’implémenter chaque problématique indépendamment des autres, puis de les assembler selon des règles bien définies. La programmation OA promet donc une meilleure productivité, une meilleure réutilisation du code et une meilleure adaptation du code aux changements. Très vite, cette nouvelle façon de faire s’est vue s’étendre sur tout le processus de développement de logiciel en ayant pour but de préserver la modularité et la traçabilité, qui sont deux propriétés importantes des logiciels de bonne qualité. Cependant, la technologie OA présente de nombreux défis. Le raisonnement, la spécification, et la vérification des programmes OA présentent des difficultés d’autant plus que ces programmes évoluent dans le temps. Par conséquent, le raisonnement modulaire de ces programmes est requis sinon ils nécessiteraient d’être réexaminés au complet chaque fois qu’un composant est changé ou ajouté. Il est cependant bien connu dans la littérature que le raisonnement modulaire sur les programmes OA est difficile vu que les aspects appliqués changent souvent le comportement de leurs composantes de base [47]. Ces mêmes difficultés sont présentes au niveau des phases de spécification et de vérification du processus de développement des logiciels. Au meilleur de nos connaissances, la spécification modulaire et la vérification modulaire sont faiblement couvertes et constituent un champ de recherche très intéressant. De même, les interactions entre aspects est un sérieux problème dans la communauté des aspects. Pour faire face à ces problèmes, nous avons choisi d’utiliser la théorie des catégories et les techniques des spécifications algébriques. Pour apporter une solution aux problèmes ci-dessus cités, nous avons utilisé les travaux de Wiels [110] et d’autres contributions telles que celles décrites dans le livre [25]. Nous supposons que le système en développement est déjà décomposé en aspects et classes. La première contribution de notre thèse est l’extension des techniques des spécifications algébriques à la notion d’aspect. Deuxièmement, nous avons défini une logique, LA , qui est utilisée dans le corps des spécifications pour décrire le comportement de ces composantes. La troisième contribution consiste en la définition de l’opérateur de tissage qui correspond à la relation d’interconnexion entre les modules d’aspect et les modules de classe. La quatrième contribution concerne le développement d’un mécanisme de prévention qui permet de prévenir les interactions indésirables dans les systèmes orientés aspect.

Impact of the ego-dystonic nature of obsessions on treatment outcome in eating disorders

Il s'agit d'une hypothèse largement répandue que l’égo-dystonie et l’égo-syntonie caractérisent les obsessions dans les troubles des conduites alimentaires (TCA) et que ces facteurs sont cliniquement pertinents pour la conceptualisation et le traitement des TCA. Cependant, les résultats empiriques sur ce sujet sont rares. Compte tenu du chevauchement reconnu entre les TCA, notamment l'anorexie et la boulimie (BN), et le trouble obsessionnel-compulsif (TOC) dans la phénoménologie et les caractéristiques psychologiques, un programme de thérapie cognitive basée sur les inférences (TBI) de 24 semaines, démontré efficace dans le traitement des TOC, a été adapté pour traiter les TCA. La recherche sur le TOC suggère que la transformation des pensées intrusives en obsessions est liée à la mesure dans laquelle les pensées intrusives menacent des perceptions fondamentales du soi et de l’identité. Cette thèse a pour objectif d'examiner le lien entre l’égo-dystonie et les TCA. Pour se faire, nous avons exploré le lien entre la nature égo-dystone des obsessions chez les patients souffrant d'un TCA et la peur de l'image de soi. Nous avons également étudié la relation entre la sévérité des symptômes TCA et l’égo-dystonie dans les obsessions. En outre, nous avons investigué les différences dans la présence de pensées égo-dystones et de peur face à son identité entre des sujets non-cliniques et des personnes atteintes d’un TCA. Enfin, nous avons comparé le degré d’égo-dystonie dans les pensées de personnes atteintes d’un TCA à celui dans les pensées d’individus souffrant d’un TOC. L’égo-dystonie dans les pensées a été mesurée par l'Ego Dystonicity Questionnaire (EDQ) et le degré de peur face à l’identité a été mesuré par le Fear of Self Questionnaire (FSQ) d’une part dans un échantillon de femmes souffrant d’un TCA (n = 57) et d’autre part dans un échantillon de participantes non-cliniques (n = 45). Les résultats révèlent que l’égo-dystonie et la peur face à l’identité étaient fortement corrélées à la fois dans l’échantillon clinique et non-clinique. Les scores de l’EDQ n’étaient pas significativement corrélés à la sévérité des symptômes TCA à l'exception de la sous-échelle d’irrationalité de l’EDQ qui était fortement associée à la sévérité des comportements compulsifs compensatoires. Les participantes souffrant d'un TCA avaient des scores significativement plus élevés à l’EDQ et au FSQ que les sujets non-cliniques. Ensuite, une étude de cas décrit l’application du programme de thérapie cognitive TBI pour une femme de 35 ans avec un diagnostic de BN. La pathologie TCA s’est significativement améliorée au cours de la TBI et six mois suivant la thérapie. Cette étude de cas met en évidence l'importance de cibler les idées surévaluées, les doutes et le raisonnement face au soi et à l’identité dans le traitement psychologique pour les TCA. Enfin, l’objectif final de cette thèse était d’examiner les changements au niveau (1) des symptômes TCA, (2) du degré d’égo-syntonie dans les obsessions, et (3) des mesures de peur face à l’identité, de motivation, d’humeur et d’anxiété au cours de la TBI et au suivi post six mois. L’égo-dystonie, la peur face à l’identité, les symptômes TCA et le stade motivationnel ont été mesurés chez 15 femmes souffrant de BN au cours du traitement et six mois après la TBI. Quatre vingt pourcent de l’échantillon, soit 12 des 15 participantes, ont démontré une diminution cliniquement significative des symptômes TCA et 53% ont cessé leurs comportements compensatoires au suivi post six mois. Les retombées cliniques relatives au traitement des TCA sont discutées.

KAM: Automatic Planning and Interpretation of Numerical Experiments Using Geometrical Methods

KAM is a computer program that can automatically plan, monitor, and interpret numerical experiments with Hamiltonian systems with two degrees of freedom. The program has recently helped solve an open problem in hydrodynamics. Unlike other approaches to qualitative reasoning about physical system dynamics, KAM embodies a significant amount of knowledge about nonlinear dynamics. KAM's ability to control numerical experiments arises from the fact that it not only produces pictures for us to see, but also looks at (sic---in its mind's eye) the pictures it draws to guide its own actions. KAM is organized in three semantic levels: orbit recognition, phase space searching, and parameter space searching. Within each level spatial properties and relationships that are not explicitly represented in the initial representation are extracted by applying three operations ---(1) aggregation, (2) partition, and (3) classification--- iteratively.

Learning Commonsense Categorical Knowledge in a Thread Memory System

If we are to understand how we can build machines capable of broad purpose learning and reasoning, we must first aim to build systems that can represent, acquire, and reason about the kinds of commonsense knowledge that we humans have about the world. This endeavor suggests steps such as identifying the kinds of knowledge people commonly have about the world, constructing suitable knowledge representations, and exploring the mechanisms that people use to make judgments about the everyday world. In this work, I contribute to these goals by proposing an architecture for a system that can learn commonsense knowledge about the properties and behavior of objects in the world. The architecture described here augments previous machine learning systems in four ways: (1) it relies on a seven dimensional notion of context, built from information recently given to the system, to learn and reason about objects' properties; (2) it has multiple methods that it can use to reason about objects, so that when one method fails, it can fall back on others; (3) it illustrates the usefulness of reasoning about objects by thinking about their similarity to other, better known objects, and by inferring properties of objects from the categories that they belong to; and (4) it represents an attempt to build an autonomous learner and reasoner, that sets its own goals for learning about the world and deduces new facts by reflecting on its acquired knowledge. This thesis describes this architecture, as well as a first implementation, that can learn from sentences such as ``A blue bird flew to the tree'' and ``The small bird flew to the cage'' that birds can fly. One of the main contributions of this work lies in suggesting a further set of salient ideas about how we can build broader purpose commonsense artificial learners and reasoners.

Elucidación del término “competitividad nacional” y análisis de su medición

El presente trabajo contiene un análisis profundo sobre el concepto de Competitividad Nacional y la pertinencia de su medición. El principal objetivo del estudio es aclarar la esencia de tan trascendental y utilizado término, así como la lógica imperante en los más reconocidos índices de medición de la competitividad de las naciones a nivel mundial. En el capítulo 1 se presentan los primeros pasos en el proceso de elucidación, metodología que se eligió para examinar a fondo el término; incluye la revisión histórica del concepto y las posiciones de reconocidas personalidades en el campo entorno a la definición del mismo. El segundo capítulo contiene un razonamiento personal sobre la naturaleza del término y lo que significa ser competitivo como país y, continuando con la metodología del capítulo anterior, se extraen las ideas clave y comunes de los autores citados para concluir con una propuesta de definición de Competitividad Nacional. El tercer capítulo es una presentación de los índices de medición del Foro Económico Mundial (Reporte Global de Competitividad) y de la escuela de negocios IMD (Anuario Mundial de Competitividad), para culminar esta sección con un análisis comparativo entre ambos. El cuarto capítulo es un análisis crítico sobre la validez de estos índices. Por último, el lector encontrará las conclusiones y reflexiones finales de la investigación.

La insuficiencia de las disposiciones del pensamiento para cubrir la brecha del pensamiento crítico a la acción crítica

En esta tesis se evalúan las disposiciones del pensamiento crítico; se demuestra la circularidad de sus enunciados y, consecuencia de ello, su insuficiencia para cubrir la brecha que va de las habilidades del pensamiento crítico a la acción crítica.

La insuficiencia de las disposiciones del pensamiento para cubrir la brecha entre pensamiento crítico y acción crítica

En este artículo se evalúan las disposiciones del pensamiento crítico; se demuestra la circularidad de sus enunciados y, consecuencia de ello, su insuficiencia para cubrir la brecha que va de las habilidades del pensamiento crítico a la acción crítica.

Tipos de lógica utilizadas en la toma de decisiones estratégicas de marketing

Para el administrador el proceso de la toma de decisiones es uno de sus mayores retos y responsabilidades, ya que en su desarrollo se debe definir el camino más acertado en un sin número de alternativas, teniendo en cuenta los obstáculos sociales, políticos y económicos del entorno empresarial. Para llegar a la decisión adecuada no hay que perder de vista los objetivos y metas propuestas, además de tener presente el proceso lógico, detectando, analizando y demostrando el porqué de esa elección. Consecuentemente el análisis que propone esta investigación aportara conocimientos sobre los tipos de lógica utilizados en la toma de decisiones estratégicas al administrador para satisfacer las demandas asociadas con el mercadeo para que de esta manera se pueda generar y ampliar eficientemente las competencia idóneas del administrador en la inserción internacional de un mercado laboral cada vez mayor (Valero, 2011). A lo largo de la investigación se pretende desarrollar un estudio teórico para explicar la relación entre la lógica y la toma de decisiones estratégicas de marketing y como estos conceptos se combinan para llegar a un resultado final. Esto se llevara a cabo por medio de un análisis de planes de marketing, iniciando por conceptos básicos como marketing, lógica, decisiones estratégicas, dirección de marketing seguido de los principios lógicos y contradicciones que se pueden llegar a generar entre la fundamentación teórica

Conflict resolution in overlapping information fields for context-based activity design

Norms are a set of rules that govern the behaviour of human agent, and how human agent behaves in response to the given certain conditions. This paper investigates the overlapping of information fields (set of shared norms) in the Context State Transition Model, and how these overlapping fields may affect the choices and actions of human agent. This paper also includes discussion on the implementation of new conflict resolution strategies based on the situation specification. The reasoning about conflicting norms in multiple information fields is discussed in detail.)

Televised Whorf: cognitive restructuring in advanced foreign language learners as a function of audio-visual media exposure

The encoding of goal-oriented motion events varies across different languages. Speakers of languages without grammatical aspect (e.g., Swedish) tend to mention motion endpoints when describing events, e.g., “two nuns walk to a house,”, and attach importance to event endpoints when matching scenes from memory. Speakers of aspect languages (e.g., English), on the other hand, are more prone to direct attention to the ongoingness of motion events, which is reflected both in their event descriptions, e.g., “two nuns are walking.”, and in their non-verbal similarity judgements. This study examines to what extent native speakers of Swedish (n = 82) with English as a foreign language (FL) restructure their categorisation of goal-oriented motion as a function of their English proficiency and experience with the English language (e.g., exposure, learning). Seventeen monolingual native English speakers from the United Kingdom (UK) were engaged for comparison purposes. Data on motion event cognition were collected through a memory-based triads matching task, in which a target scene with an intermediate degree of endpoint orientation was matched with two alternative scenes with low and high degrees of endpoint orientation, respectively. Results showed that the preference among the Swedish speakers of L2 English to base their similarity judgements on ongoingness rather than event endpoints was correlated with their use of English in their everyday lives, such that those who often watched television in English approximated the ongoingness preference of the English native speakers. These findings suggest that event cognition patterns may be restructured through the exposure to FL audio-visual media. The results thus add to the emerging picture that learning a new language entails learning new ways of observing and reasoning about reality.

Transreal arithmetic as a consistent basis for paraconsistent logics

Paraconsistent logics are non-classical logics which allow non-trivial and consistent reasoning about inconsistent axioms. They have been pro- posed as a formal basis for handling inconsistent data, as commonly arise in human enterprises, and as methods for fuzzy reasoning, with applica- tions in Artificial Intelligence and the control of complex systems. Formalisations of paraconsistent logics usually require heroic mathe- matical efforts to provide a consistent axiomatisation of an inconsistent system. Here we use transreal arithmetic, which is known to be consis- tent, to arithmetise a paraconsistent logic. This is theoretically simple and should lead to efficient computer implementations. We introduce the metalogical principle of monotonicity which is a very simple way of making logics paraconsistent. Our logic has dialetheaic truth values which are both False and True. It allows contradictory propositions, allows variable contradictions, but blocks literal contradictions. Thus literal reasoning, in this logic, forms an on-the- y, syntactic partition of the propositions into internally consistent sets. We show how the set of all paraconsistent, possible worlds can be represented in a transreal space. During the development of our logic we discuss how other paraconsistent logics could be arithmetised in transreal arithmetic.

Formulation of a tropical town energy budget (t-TEB) scheme

This work describes the tropical town energy budget (t-TEB) scheme addressed to simulate the diurnal occurrence of the urban heat island (UHI) as observed in the Metropolitan Area of Rio de Janeiro (MARJ; -22A degrees S; -44A degrees W) in Brazil. Reasoning about the tropical urban climate have guided the scheme implementation, starting from the original equations from Masson (Bound-Lay Meteorol 94:357-397, 2000). The modifications include (a) local scaling approaches for obtaining flux-gradient relationships in the roughness sub-layer, (b) the Monin-Obukhov similarity framework in the inertial sub-layer, (c) increasing aerodynamic conductance toward more unstable conditions, and (d) a modified urban subsurface drainage system to transfer the intercepted rainwater by roofs to the roads. Simulations along 2007 for the MARJ are obtained and compared with the climatology. The t-TEB simulation is consistent with the observations, suggesting that the timing and dynamics of the UHI in tropical cities could vary significantly from the familiar patterns observed in mid-latitude cities-with the peak heat island intensity occurring in the morning than at night. The simulations are suggesting that the thermal phase shift of this tropical diurnal UHI is a response of the surface energy budget to the large amount of solar radiation, intense evapotranspiration, and thermal response of the vegetated surfaces over a very humid soil layer.