Description logics (DLs) are a family of knowledge representation languages to describe concepts in a given domain. While we can define the semantics of description logics using, for example, a translation into first-order logic, so far the proof-theoretic nature of DL has not been well investigated. In this thesis, we develop a proof theory for a constructive version of Description Logic, specifically Attributive Language with Complement (ALC), in two steps: First, we define a natural deduction system for ALC and develop a sequent calculus formulation, for which we prove cut-admissibility. We build on prior work on constructive description logic by de Paiva [2006] and modal logic by Simpson [1994], which ensures the consistency of the proposed systems for ALC. In addition, we prove soundness and completeness of this system with respect to known Kripke semantics. The study of these properties provides further evidence that it is appropriate to consider description languages as logics. Second, we adapt recent work by Andreoli [1992] on focusing systems for a variety of non-classical logics to the setting of constructive description logics. Exploiting the invertibility of certain inference rules, we design a focusing calculus suitable for backwards search, and prove its correctness via cut-admissibility. This proof-theoretic study lays the foundation for the development of a practical proof search strategy for constructive description logics. / Les logiques descriptives (DLs) sont une famille de langues de representation de connaissance pour décrire les concepts dans un domaine donné. Pendant que nous pouvons définir la sémantique de logiques descriptives en utilisant, par exemple, une traduction dans la logique du premier ordre, pour l'instant la nature théorique de preuve de DL n'a pas été bien enquêtée. Dans cette thèse, nous développons une théorie de preuve pour une version constructive de la logique descriptive, en "Attributive Language with Complement" (ALC ), en deux étapes: Premièrement, nous définissons un système de déduction naturel pour ALC et développons une formulation de calcul de séquent, pour laquelle nous prouvons l'admissibilité de coupure. Nous tirons parti du travail préalable sur la logique descriptive constructive par de Paiva [2006] et la logique modale par Simpson [1994], qui garantit la cohérence des systèmes proposés pour ALC. En plus, nous prouvons la solidité et complétude de ce système par rapport aux sémantiques Kripke connues. L'étude de ces propri étés fournissent plus d'indices que c'est approprié à considérer les langues descriptives comme des logiques propres. Deuxièmement, nous adaptons le travail récent par Andreoli [1992] sur les systèmes concentrés pour une variété de logiques non-classiques au cadre de logiques descriptives constructives. Le fait d'exploiter l'invertibility de certaines règles d'inférences, nous concevons un calcul concentré convenable à recherche reculons et prouvez son exactitude par l'admissibilité de coupure. Cette étude sur une théorie de preuve pose la fondation pour le développement d'une stratégie de recherche de preuves pratiques.

Application frameworks provide a general design that connects together the different parts of a program and that free developers from low-value activities. In the course of a framework's evolution, changes ranging from a simple function renaming to major modifications of the design can break client programs that depend on the framework. Finding suitable replacements for framework elements that were accessed by a client program and deleted as part of the framework's evolution can be a challenging task. We present a recommendation system, SemDiff, that suggests adaptations to client programs by analyzing how a framework was adapted to its own changes. In a study of the evolution of a large open-source framework and three client programs, our approach recommended relevant adaptive changes with a high level of precision, and detected non-trivial changes typically undiscovered by current changes detection techniques. / Les cadres d'applications fournissent un design général qui relie les différentes parties d'un programme et qui libère les développeurs des tâches à faible valeur ajoutée. Durant l'évolution d'un cadre d'applications, des changements allant d'un simple renommage d'une fonction à des modifications majeures du design peuvent briser les programmes clients qui dépendent du cadre d'applications. Trouver un remplacement adéquat pour les éléments du cadre d'applications qui étaient accédés par le programme client et qui ont été supprimés durant l'évolution du cadre d'applications peut s'avérer être une tâche difficile. Nous présentons un système de recommandations, SemDiff, qui suggère des adaptations aux programmes clients en analysant comment un cadre d'applications a été adapté à ses propres modifications. Dans une étude sur l'évolution d'un grand cadre d'applications en code source libre et de trois programmes clients, notre système a recommandé des adaptations pertinentes avec un haut degré de précision. Notre système a aussi détecté des changements non triviaux qui sont typiquement ignorés par les techniques de détection de changements courantes.

We offer an alternative method for type checking expressions in an extension of Hindley and Milner’s lambda calculus with generalized algebraic data types. The approach foregoes all mention of type equalities and unifiers and only applies type conversions at case statements in a deterministic fashion. What we introduce is a method for finding out the appropriate types of pattern bound variables within a type derivation and how to convert them back so that they are valid types in the context of the enclosing expression. Everything is done locally so scoping is no longer an issue. The system is proven sound and complete. An implementation of the system is discussed. / Ce document propose une methode alternative de verification du type dans une extension du systeme de typage de Hindley et Milner avec des types de donnees algebriques generalises. Cette methode n’utilise pas d’unificateur et d’egalite de type. De plus, elle ne convertit les types qu’a l’expression de case, et ce de maniere deterministique. Tout est fait localement dans ce systeme. Le systeme est prouve complet et correcte et une implementation est decrite.

Natural Montmorillonite was modified with thermally stable phosphonium surfactants to produce new organoclays for the production of polymer nanocomposites. The organoclays were characterized to determine thermal stability, basal spacing, and the surface energy at room temperature and at the processing temperature. Polystyrene (PS)/organoclay nanocomposites were prepared by melt compounding, using three different PS resins. Experimental data were obtained to elucidate the influences of temperature and molecular weight and structure of the surfactant on the surface energy of the organoclays. The phosphonium-based organoclays exhibited better thermal stability than commercially available ammonium-based organoclays. The basal spacing was similar to that found in commercially available organoclays. Transmission electron microscopy (TEM) showed that the degree of dispersion of the various organoclays in nanocomposites was related to the Hamaker constant of the organoclay at the processing temperature. Significant improvement in the degree of dispersion was realized, when blends of polystyrene with a styrene- maleic anhydride (SMA) copolymer were used. It appeared that delamination in the SMA systems was achieved directly without undergoing an intermediate intercalated structure. The influence of organoclay concentration on flexural modulus of PS- organoclay nanocomposites was determined, using the Halpin-Tsai and Hui-Shai models. The predictions were in good agreement with experimental results. The modulus of PS nanocomposites correlated well with the work adhesion at room temperature, in agreement with the equation of Shang. Barrier properties showed reasonable agreement with the predictions of models reported in literature. However, the values of aspect ratios predicted by the models were quite different from those observed experimentally. The permeability of nanocomposites to oxygen correlated with both the Hamaker constant A131 at the processing temperature / De la montmorillonite naturelle a été modifiée avec des surfactants de phosphonium qui sont thermiquement stables pour objectif de produire de nouvelles organoargiles pour la production de nanocomposites polymériques. Les organoargiles ont été caractérisées pour déterminer la stabilité thermique, l'espacement basal et l'énergie superficielle à température ambiante et à la température de préparation. Des nanocomposites de polystyrène (PS) et organoargile ont été préparés en fondant le PS, avec trois différentes résines de PS. On a évalué l'influence de la température, de la masse molaire et de la structure des surfactants sur l'énergie superficielle des organoargiles. Les organoargiles préparées avec des surfactants de phosphonium ont démontré une meilleure stabilité thermique que les organoargiles commerciales préparées avec des surfactants d'ammonium. L'espacement basal a été similaire à celui des organoargiles commerciales. La microscopie électronique en transmission a démontré que le degré de dispersion des organoargiles dans les nanocomposites est en relation avec la constante de Hamaker de l'organoargile à la température de préparation. Le degré de dispersion de l'argile a été amélioré quand un mélange de polystyrène avec un copolymère de styrène et d'anhydride maléique (SAM) a été employé. Apparemment, la delamination dans les systèmes de SAM a été réussie directement sans avoir une structure intercalée intermédiaire. On a déterminé l'influence de la concentration d'argile sur les propriétés mécaniques des nanocomposites de PS en utilisant les modèles de Halpin-Tsai et Hui-Shai. Les prédictions ont été en accord avec les résultats expérimentaux. Les modules des nanocomposites de PS sont bien corrélés avec le travail d'adhésion à la température ambiante, selon l'équation de Shang. Les propriétés de barrière ont été mesurées et sont en accord avec les prédictions des$

With the launch of World of Warcraft in 2004, Massively Multiplayer Online Games (MMOGs) really came into their own as millions of people started playing worldwide. Providing scalability to such a large audience while maintaining a consistent gameplay experience is a diffcult task which many companies face in an industry where only few succeed. This thesis focuses on the issues of how a MMOG can be scaled to support more concurrent players and how consistency can be maintained in a Distributed Multi-Server Environment (DMSE). As a basis for investigation the notion of "Subgames" (i.e. games within games) was introduced. As smaller, more flexible game units, subgames reduce scalability problems but raise consistency concerns by requiring modular game actions in a distributed environment to function. This is addressed through a new transactional protocol and action framework which abstracts and solves consistency issues while creating an infrastructure which allows for scalability. A complete solution is illustrated using these techniques through the design of general game mechanics and subgames. The approach here further enables scalability of MMOGs in a DMSE and provides a general framework for the further investigation of MMOG consistency and scalability through subgame instances. / La popularité des jeux massivement multi-joueurs en ligne ( MMOGs ) a grandement augmenté avec l'arrivée du jeu World of Warcraft, qui est joué par des millions de personnes à travers le monde. Cependant, ce type d'application nécessite des infrastructures extensibles pour accommoder des milliers de joueurs, tout en offrant une expérience de jeu consistante. Ceci représente un grand obstacle que plusieurs compagnies doivent affronter, mais qui est surmonté par peu. Cette thèse aborde les problèmes reliés à la croissance du nombre de joueurs simultanés, tout en discutant comment maintenir un environnement distribué multi- serveurs ( DMSE ) consistant. La notion de sous-jeux ( un jeu qui se déroule l'intérieur d'un autre jeu ) a été utilisée pour mieux étudier le problème. En tant qu'unités de jeu plus petits et flexibles, les sous-jeux facilitent la croissance, mais augmentent les problèmes de concurrence puisque leur bon fonctionnement nécessite des actions modulaires dans un environnement distribué. Ces défis sont adressés par un nouveau protocole transactionnel et un cadre d'applications d'actions qui font abstraction et règlent les problèmes de consistance, tout en offrant une infrastructure qui permet une certaine croissance. Une solution, où les mécanismes de jeux et de sous-jeux sont adaptés en conséquence, illustre les techniques proposées dans cette thèse. Ces techniques permettent une plus grande croissance pour les jeux MMOGs dans un DMSE, tout en fournissant des outils de sous-jeux qui permettent l'étude des défis de consistance et de croissance.

Modeling 3D object classes requires accounting for intra-class variations in an object's appearance under different viewpoints, scale and illumination conditions. Therefore, detecting instances of 3D object classes in the presence of background clutter is difficult. This thesis presents a novel approach to model generic 3D object classes and an algorithm to detect multiple instances of an object class in an arbitrary image. Motivated by the parts-based representation, the proposed approach divides the object into different spatial regions. Each spatial region is associated with an object part whose appearance is represented by a dense set of overlapping SIFT features. The distribution of these features is then described in a lower dimensional space using supervised Locally Linear Embedding. Each object part is essentially represented by a spatial cluster in the embedding space. For viewpoint invariance, the view-sphere comprising the 3D object is divided into a discrete number of view segments. Several spatial clusters represent the object in each view segment. This thesis provides a framework for representing these clusters in either single or multiple embedding spaces. A novel aspect of the proposed approach is that all object parts and the background class are represented in the same lower dimensional space. Thus the detection algorithm can explicitly label features in an image as belonging to an object part or background. Additionally, spatial relationships between object parts are established and employed during the detection stage to localize instances of the object class in a novel image. It is shown that detecting objects based on measuring spatial consistency between object parts is superior to a bag-of-words model that ignores all spatial information. Since generic object classes can be characterized by shape or appearance, this thesis has formulated a method to combine these attributes to enhance the object model. Class-specific local contour featur / La modélisation de classes d'objets 3D nécessite la prise en compte des variations à l'intérieur d'une même classe de l'apparence d'un objet sous différents points de vue, échelles et conditions d'illumination. Par conséquent, la détection de tels objets en présence d'un arrière-plan complexe est difficile. Cette thèse présente une approche nouvelle pour la modélisation générique de classes d'objets 3D, ainsi qu’un algorithme pouvant détecter plusieurs objets d'une classe dans une image.Motivé par la représentation par parties, l'approche proposée divise l'objet en différentes régions spatiales. Chaque région est associée à la partie d'un objet dont l'apparence est représentée par un ensemble dense de caractéristiques SIFT superposées. La distribution de ces caractéristiques est alors projetée dans un espace dimensionnel inférieur à l'aide d'un algorithme supervisé de Locally Linear Embedding. Chaque partie de l'objet est essentiellement représentée par un regroupement spatial dans l'espace englobant. Pour l'invariance de point de vue, la sphère contenant l'objet 3D est divisée en un nombre discret de segments. Plusieurs regroupements spatiaux représentent l'objet dans chaque segment. Cette thèse propose une manière de représenter ces regroupements aussi bien dans des espaces englobants uniques que multiples. Un aspect innovateur de l'approche proposée est que toutes les parties d'objets et les éléments d'arrière-plan sont représentés dans le même espace dimensionnel inférieur. Ainsi, l'algorithme de détection peut explicitement étiqueter des éléments d'une image comme appartenant à une partie d'objet ou à l'arrière-plan. De plus, les relations spatiales entre les parties d'un objet sont déterminées pendant l'étape de détection et employées pour localiser des éléments d'une classe d'objet dans une nouvelle image. Il est démontré que la détection d'objets basée sur la mesure de la consistanc

This thesis introduces a maximum entropy approach to model surface reflectance spectra. A reflectance spectrum is the amount of light, relative to the incident light, reflected from a surface at each wavelength. While the color of a surface can be in 3D vector form such as RGB, CMY, or YIQ, this thesis takes the surface reflectance spectrum to be the color of a surface. A reflectance spectrum is a physical property of a surface and does not vary with the different interactions a surface may undergo with its environment. Therefore, models of reflectance spectra can be used to fuse camera sensor responses from different images of the same surface or multiple surfaces of the same scene. This fusion improves the spectral estimates that can be obtained, and thus leads to better estimates of surface colors. The motivation for using a maximum entropy approach stems from the fact that surfaces observed in our everyday life surroundings typically have broad and therefore high entropy spectra. The maximum entropy approach, in addition, imposes the fewest constraints as it estimates surface reflectance spectra given only camera sensor responses. This is a major advantage over the widely used linear basis function spectral representations, which require a prespecified set of basis functions. Experimental results show that surface spectra of Munsell and construction paper patches can be successfully estimated using the maximum entropy approach in the case of three different surface interactions with the environment. First, in the case of changes in illumination, the thesis shows that the spectral models estimated are comparable to those obtained from the best approach which computes spectral models in the literature. Second, in the case of changes in the positions of surfaces with respect to each other, interreflections between the surfaces arise. Results show that the fusion of sensor responses from interreflection / Cette thèse introduit une approche par entropie maximale pour la modélisation des spectres de réflectance de surface. Un spectre de réflectance est la quantité de lumière, relative à la lumière incidente, réfléchie d'une surface à chaque longueur d'onde. Bien que la couleur d'une surface puisse prendre la forme d'un vecteur 3D tel que RGB, CMY ou YIQ, cette thèse prend le spectre de réflectance de surface comme étant la couleur d'une surface. Un spectre de réflectance est une propriété physique d'une surface et ne varie pas avec les différentes interactions que peut subir une surface avec son environnement. Par conséquent, les modèles de spectres de réflectance peuvent être utilisés pour fusionner les réponses de senseurs de caméra provenant de différentes images d'une même surface ou de multiples surfaces de la même scène. Cette fusion améliore les estimés spectraux qui peuvent être obtenus et mène donc à de meilleurs estimés de couleurs de surfaces.La motivation pour l'utilisation d'une approche par entropie maximale provient du fait que les surfaces observées dans notre environnement habituel ont typiquement un spectre large et donc à haute entropie. De plus, l'approche par entropie maximale impose le moins de contraintes puisqu'elle estime les spectres de réflectance de surface à l'aide seulement des réponses de senseurs de caméra. Ceci est un avantage majeur par rapport aux très répandues représentations spectrales par fonctions de base linéaires qui requièrent une série pré-spécifiée de fonctions de base.Les résultats expérimentaux montrent que les spectres de surface de taches de surface de Munsell et de papier de construction peuvent être estimés avec succès en utilisant l'approche par entropie maximal dans le cas de trois différentes interactions de surfaces avec l'environnement. D'abord, dans le cas de changements dans l'illumination, la t

Modal logics were formalized in the early to mid-20th century to pin down the notion of truth qualified by modalities such as "necessity", "possibility", and "belief", which arise in philosophy and natural languages. They have since outgrown their philosophical trappings and have found applications in type systems and as description languages in many domains of computer science and artificial intelligence. Although they frequently exhibit redundancies in their proof spaces, analytic tableau systems in the style of Smullyan have emerged as popular proof formalisms for modal logics. Inspired by previous work on matrix characterizations by Bibel, Andrews, and Wallen, we propose a new characterization of validity for a family of multimodal logics with interacting accessibility relations which avoids the redundancies common in tableau systems. Our goal is not to produce a high-performance theorem prover for multimodal logics, but to present a fresh way of understanding and establishing multimodal logical validity. / Les logiques modales ont été formalisées vers le milieu du 20ième siècle avec le but de comprendre la notion de vérité qualifiée par des modes tels que "la nécessité", "la possibilité", et "la croyance", qui proviennent de la philosophie et des langages naturels. Ces modes, depuis évolués au-delà de leurs origines philosophiques, trouvent plusieurs applications dans la sémantique statique des langages de programmation et chez les logiques de description de plusieurs domaines de l'informatique et de l'intelligence artificielle. Bien que leurs espaces démonstrationnels présentent des redondances, les systèmes de tableaux analytiques sont un formalisme de démonstration populaire. Nous proposons une nouvelle caractérisation de validité pour une famille de logiques multimodales définies avec des relations d'accessibilité interagissantes qui évite les redondances présentes chez les systèmes de tableaux. Nos innovations sont inspirées par les caractérisations matricielles présentées auparavant par Bibel, Andrews, et Wallen. Notre but n'est pas de produire un démonstrateur automatique de théorèmes de haute performance, mais de présenter une façon originale de comprendre et concevoir la validité logique multimodale.

This thesis presents a novel idea for object allocation, cache line reservation (CLR), whose goal is to reduce data cache misses. Certain objects are allocated from "reserved" cache lines, so that they do not evict other objects that will be needed later. We discuss what kinds of allocations can benefit from CLR, as well as sources of overhead. Prototypes using CLR were implemented in the IBM® J9 Java™ virtual machine (JVM) and its Testarossa just-in-time (JIT) compiler. A performance study of our prototypes was conducted using various benchmarks. CLR can offer a benefit in specialized microbenchmarks when allocating long-lived objects that are accessed in infrequent bursts. In other benchmarks such as SPECjbb2005 and SPECjvm2008, we show that CLR can reduce cache misses when allocating a large number of short-lived objects, but not provide a performance improvement due to the introduced overhead. We measure and quantify this overhead in the current implementation and suggest areas for future development. CLR is not limited to Java applications, so other static and dynamic compilers could benefit from it in the future. / Cette thèse présente une nouvelle idée pour l'attribution d'objet, réservation de ligne d'antémémoire (RLA), dont le but est de réduire les échecs d'accès à l'antémémoire. Certains objets sont alloués à partir d'une antémémoire de réserve, de manière à éviter l'éviction d'autres objets ultérieurement requis. Nous discutons les types d'allocation qui peuvent bénéficier de RLA, ainsi que les sources de coûts indirects. Les prototypes que nous avons développé qui font usage de RLA furent créés utilisant la machine virtuelle IBM® J9 Java™ et son compilateur juste-a-temps Testarossa. Une étude de performance de nos prototypes fut conduite avec plusieurs tests de performance. RLA peut offrir un bénéfice pour des microtests de performance spécialisés dans les cas où des objets de longue vie sont lus en rafales infréquentes. Dans d'autres tests que SPECjbb2005 et SPECjvm2008, nous démontrons que RLA peut réduire les échecs d'accès a l'antémémoire dans les cas d'allocation d'un grand nombre d'objets de court temps de vie, mais n'offre pas d'amélioration de la performance vue l'introduction de coûts indirects. Nous mesurons et quantifions ces coûts dans notre implémentation courante et suggérons des domaines de développement futurs. RLA n'est pas limité aux applications Java, ce qui permet à d'autres compilateurs statiques comme dynamiques d'en tirer profit dans l'avenir.

This thesis concerns the relationship between four graph invariants: omega, chi_f, chi, and Delta. These are the clique number, the fractional chromatic number, the chromatic number, and the maximum degree, respectively. Trivially omega <= chi_f <= chi <= Delta + 1. We seek to improve the upper bound on chi. We are motivated by a conjecture of Reed, which essentially states that chi is at most the average of its trivial upper and lower bounds: Conjecture. For any graph, chi <= (Delta + 2 + omega)/2. We call this the Main Conjecture, and propose a Local Strengthening based on the closed neighbourhood of a single vertex: Conjecture. For any graph G, chi <= max{v in V(G)} (d(v) + 2 + omega(G[N(v)]) + 1) / 2. We begin by showing that much of the early evidence supporting the Main Conjecture also supports the Local Strengthening. In particular, the variant of the Local Strengthening obtained by replacing chi by chi_f holds, as does the Local Strengthening when the stability number is two. Guided by the first of these results we look towards line graphs, for which chi_f and chi agree asymptotically. We prove the Main Conjecture for line graphs, then we seek to generalize this result. To do this we use recent results of Chudnovsky and Seymour, who characterized the structure of all claw-free graphs. We refine their results by introducing a graph reduction on certain types of homogeneous pairs of cliques that preserves the chromatic number. Thus we need only consider the problem of colouring _skeletal_ claw-free graphs, which cannot be reduced. The structure of skeletal claw-free graphs is simpler than that of general claw-free graphs. We generalize two results from line graphs to the class of quasi-line graphs. Namely, that the Main Conjecture holds, and that chi_f and chi agree asymptotically. We then consider all claw-free graphs. We prove the Main Conjecture for all claw-free graphs and we prove the Local / Cette thèse a pour sujet la relation entre quatre invariants de graphes : omega, chi_f, chi, et Delta.Il s'agit respectivement du nombre de clique, du nombre chromatique fractionnaire,du nombre chromatique, et du degré maximum. Ces paramètres vérifient trivialementl'encadrement suivant : omega <= chi_f <= chi <= Delta+1, dans lequel on cherche ça améliorerla borne supérieure sur chi. Une des principales motivations pour ce travail est uneconjecture de Reed, qui dit essentiellement que chi est au plus la moyenne de ses bornesinférieures et supérieures triviales.Conjecture. Pour tout graph, chi <= (Delta + 2 + omega)/2.On appelle cet énoncé la Conjecture Principale, et on propose un RenforcementLocal basé sur le voisinage de chaque sommet.Conjecture. Pour tout graphe G, chi <= max{v dans V(G)} (d(v) + 2 + omega(G[N(v)]) + 1) / 2.On commence par montrer que la plupart des arguments en faveur de la ConjecturePrincipale incitent également à croire que le Renforcement Local est vrai. Enparticulier, la borne donnée par le Renforcement Local vaut pour chi_f et le RenforcementLocal peut être montré lorsque le nombre de stabilité vaut deux.Guidé par ces premiers pas, on s'intéresse aux graphes adjoints, pour lesquels chi_fet chi sont asymptotiquement équivalents. On montre la Conjecture Principale dansle cas des graphes adjoints et on cherche ensuite à généraliser ce résultat.Pour cela on utilise des résultats récents de Chudnovsky et Seymour, qui ontcaractérisé la structure les graphes sans griffes. On affine ces résultats en introduisantla notion de graphes squelettes. Dans les problèmes auxquels on s'intéresse,on peut facilement se ramener au cas des graphes squelettes, et la structure desgraphes squelettes sans griffes est plus simple que celle des graphes sans griffes engénéral.On étend deux résultats des graphes adjoints aux graphes quasi-adjoints : onmontre que la Conj