No / In recent decades, sustainable investing has caught on with investors, and it has now become the norm. In the age of start-ups, with scant information on the sustainability aspects of an asset, it becomes harder to pursue sustainable investing. To this end, this paper proposes a sustainable financial portfolio selection approach in an intuitionistic fuzzy framework. We present a comprehensive three-stage methodology in which the assets under consideration are ethically screened in Stage-I. Stage-II is concerned with cal- culating the sustainability scores, based on various social, environmental, and economic (SEE) criteria and an evaluation of the return and risk of the ethical assets. Intuitionistic fuzzy set theory is used to gauge the linguistic assessment of the assets on several SEE criteria from multiple decision-makers. A novel intuitionistic fuzzy multi-criteria group decision-making technique is applied to calculate the sustainability score of each asset. Finally, in Stage-III, an intuitionistic fuzzy multi-objective financial portfolio selection model is developed with maximization of the satisfaction degrees of the sustainabil- ity score, return, and risk of the portfolio, subject to several constraints. The ε-constraint method is used to solve this model, which yields various efficient, sustainable financial portfolios. Subsequently, investors can choose the portfolio best suited to their preferences from this pool of efficient, sustainable financial portfolios. A detailed empirical illustration and a comparison with existing works are given to substantiate and validate the proposed approach. / Institution of Eminence, University of Delhi, Delhi-110007 under Faculty Research Program

In this paper, we prove that it is consistent with ZFC that GCH holds and that every pair of normal Aronszajn trees contain club isomorphic subtrees.

As soon as Bennett and Gill first demonstrated that, relative to a randomly chosen oracle, P is not equal to NP with probability 1, the random oracle hypothesis began piquing the interest of mathematicians and computer scientists. This was quickly disproven in several ways, most famously in 1992 with the result that IP equals PSPACE, in spite of the classes being shown unequal with probability 1. Here, we propose what could be considered strengthening of the random oracle hypothesis, using a stricter notion of what it means for a set to be 'large'. In particular, we suggest using largeness with respect to the Ramsey forcing notion. In this new context, we demonstrate that the set of oracles separating NP and coNP is 'not small', and obtain similar results for the separation of PSPACE from PH along with the separation of NP from BQP. In a related set of results, we demonstrate that these classes are all of the same descriptive complexity. Finally we demonstrate that this strengthening of the hypothesis turns it into a sufficient condition for unrelativized relationships, at least in the three cases considered here.

Velleman beweist die Konsistenz der Existenz vereinfachte Gap 2 Moraste (ein Begriff gleichwertig zu den ursprünglichen Morasten, geschafft von Jensen). Wir haben einen noch einfachen Begriff des vereinfachten Morastes in der Dissertation vorgeschlagen, Details aufgefüllt und wesentlich auch einen verschiedenen Beweis des Satzes erfunden und zwar in beide Stufe des Forcingverfahrens. Wir benötigen auch keine Squarefunktionereihenfolge (die ganz Kohärenzvoraussetzung fehlt aber ist linear und konfinal) sondern ein ``erratendes'' Verfahren für Sequenze, das nicht fest ist und nicht die ganze Kohärenzbedigung erfüllt wie bei Velleman. Wir hoffen, wir haben so eingelegt die Basis für einen zukunftigen Beweis des allgemeines Falls n in ZFC. / Velleman proved the consistency of the existence of simplified gap 2 morasses (equivalent to the concrete morasses defined by Jensen) using a two stage forcing. We give an essentially different proof of the same result and fill up some details from Velleman's paper which were not clear or imcomplete. In fact the proof uses a simpler definition of simplified gap 2 morasses. We have also eliminated the use of square-like sequences in the second stage, employing a ``guessing'' procedure for sequences which are not fixed and do not satisfy full coherence requirement. With these steps we hope to have laid the foundation for a future proof of gap n morasses in ZFC.

Specification plays a vital role in software engineering to facilitate the development of highly dependable software. The importance of specification in software development is to serve, amongst others, as a communication tool for stakeholders in the software project. The specification also adds to the understanding of operations, and describes the properties of a system. Various techniques may be used for specification work. Z is a formal specification language that is based on a strongly-typed fragment of Zermelo-Fraenkel set theory and first-order logic to provide for precise and unambiguous specifications. Z uses mathematical notation to build abstract data, which is necessary for a specification. The role of abstraction is to describe what the system does without prescribing how it should be done. Diagrams, on the other hand, have also been used in various areas, and in software engineering they could be used to add a visual component to software specifications. It is plausible that diagrams may also be used to reason in a semi-formal way about the properties of a specification. Many diagrammatic languages are based on contours and set theory. Examples of these languages are Euler-, Spider-, Venn- and Pierce diagrams. Euler diagrams form the foundation of most diagrams that are based on closed curves. Diagrams, on the other hand, have also been used in various areas, and in software engineering they could be used to add a visual component to software specifications. It is plausible that diagrams may also be used to reason in a semi-formal way about the properties of a specification. Many diagrammatic languages are based on contours and set theory. Examples of these languages are Euler-, Spider-, Venn- and Pierce diagrams. Euler diagrams form the foundation of most diagrams that are based on closed curves. The purpose of this research is to demonstrate the extent to which diagrams can be used to represent a Z specification. A case study is used to transform the specification modelled with Z language into a diagrammatic specification. Euler, spider, Venn and Pierce diagrams are combined for this purpose, to form one diagrammatic notation that is used to transform a Z specification / School of Computing / M. Sc. (Information Systems)

No description available.

Fuzzy relational databases deal with imprecise data or fuzzy information in a relational database. The purpose of this fuzzy database implementation is to retrieve images by using fuzzy queries whose common-language descriptions are defined by the consensus of a particular user community. The fuzzy set, which is presentation of fuzzy attribute values of the images, is determined through membership function. This paper compares two methods of constructing membership functions, the Direct Rating and New Random Proportional, to determine which method gives maximum users satisfaction with minimum feedback from the community. The statistical analysis of results suggests the use of Direct Rating method. Moreover, the analysis shows that the performance of the New Random Proportional method can be improved with the inclusion of a "Not" modifier. This paper also identifies and analyzes issues that are raised by different versions of the database system.

The GUHA method is one of the oldest methods of exploratory data analysis, which is regarded as part of the data mining or knowledge discovery in databases (KDD) scienti_c area. Unlike many other methods of data mining, the GUHA method has firm theoretical foundations in logic and statistics. In scope of the method, finding interesting knowledge corresponds to finding special formulas in satisfactory rich logical calculus, which is called observational calculus. The main topic of the thesis is application of the "fuzzy paradigm" to the GUHA method By the term "fuzzy paradigm" we mean approaches that use many-valued membership degrees or truth values, namely fuzzy set theory and fuzzy logic. The thesis does not aim to cover all the aspects of this application, it emphasises mainly on: - Association rules as the most prevalent type of formulas mined by the GUHA method - Usage of fuzzy data - Logical aspects of fuzzy association rules mining - Comparison of the GUHA theory to the mainstream fuzzy association rules - Implementation of the theory using the bit string approach The thesis throughoutly elaborates the theory of fuzzy association rules, both using the theoretical apparatus of fuzzy set theory and fuzzy logic. Fuzzy set theory is used mainly to compare the GUHA method to existing mainstream approaches to formalize fuzzy association rules, which were studied in detail. Fuzzy logic is used to define novel class of logical calculi called logical calculi of fuzzy association rules (LCFAR) for logical representation of fuzzy association rules. The problem of existence of deduction rules in LCFAR is dealt in depth. Suitable part of the proposed theory is implemented in the Ferda system using the bit string approach. In the approach, characteristics of examined objects are represented as strings of bits, which in the crisp case enables efficient computation. In order to maintain this feature also in the fuzzy case, a profound low level testing of data structures and algoritms for fuzzy bit strings have been carried out as a part of the thesis.

O presente trabalho centra-se no estudo da narrativa do romance O Castelo, escrito em 1922, pelo escritor tcheco Franz Kafka. Por meio da análise formal da obra em questão, objetiva-se estabelecer relações entre aspectos presentes na narrativa que possuam associações metafóricas a temas vigentes no cotidiano do autor e, conseqüentemente, do homem moderno, e que possuam conotação negativa, tais como o poder, simbolizado pela burocracia, pela divinização, e pelo espaço. Partindo dessa premissa, propõe-se relacionar esses temas à teoria dos conjuntos da matemática, na qual um conjunto maior contém um conjunto menor, esse atuando por sua vez como um subconjunto daquele. Propõe-se aqui fazer uma analogia do conjunto poder e seu enfoque negativo como poder com o subconjunto burocracia, este intimamente ligado àquele, e que possui intersecção com os subconjuntos divinização e espaço. Por fim, ressaltar-se-á a universalidade da obra de Kafka, que possibilita a efetuação de analogias temáticas das mais diversas, não só as aqui expostas em forma de conjuntos e subconjuntos, pelo fato de seu texto ser multifacetado no tocante a temas. / This monograph focuses on analyzing the narrative of The Castle, a novel written by the Czech author Franz Kafka, in 1922. It aims at establishing a connection between certain aspects within the text which may have a metaphorical association with themes related to not only the authors life experiences, but also any other modern mans. It will be centered on a formal analysis of the novel and on metaphorical aspects within the narrative, which may have a negative connotation linked with power, represented by bureaucracy, divinization and space. Afterwards, we will propose a relation of such themes to the set theory from Mathematics, in which a greater set contains a smaller set, also known as a subset. We aim at drawing an analogy of power as a set and its negative connotation with the bureaucratic subset, which are intimately connected. Bureaucracy intersects the two other subsets called divinization and space. Eventually, we will focus on the universality of Kafkas work, which enables the drawing of many other thematic analogies, not only the ones discussed in this set theory proposed in this monograph, due to the fact that Kafkas work is multifaceted in terms of themes.

Cette thèse présente des techniques efficaces pour déléguer des obligations de preuves TLA+ dans des démonstrateurs automatiques basées sur la logique du premier ordre non-sortée et multi-sortée. TLA+ est un langage formel pour la spécification et vérification des systèmes concurrents et distribués. Sa partie non-temporelle basée sur une variante de la théorie des ensembles Zermelo-Fraenkel permet de définir des structures de données. Le système de preuves TLAPS pour TLA+ est un environnement de preuve interactif dans lequel les utilisateurs peuvent vérifier de manière déductive des propriétés de sûreté sur des spécifications TLA+. TLAPS est un assistant de preuve qui repose sur les utilisateurs pour guider l’effort de preuve, il permet de générer des obligations de preuve puis les transmet aux vérificateurs d’arrière-plan pour atteindre un niveau satisfaisant d’automatisation. Nous avons développé un nouveau démonstrateur d’arrière-plan qui intègre correctement dans TLAPS des vérificateurs externes automatisés, en particulier, des systèmes ATP et solveurs SMT. Deux principales composantes constituent ainsi la base formelle pour la mise en oeuvre de ce nouveau vérificateur. Le premier est un cadre de traduction générique qui permet de raccorder à TLAPS tout démonstrateur automatisé supportant les formats standards TPTP/ FOF ou SMT-LIB/AUFLIA. Afin de coder les expressions d’ordre supérieur, tels que les ensembles par compréhension ou des fonctions totales avec des domaines, la traduction de la logique du premier ordre repose sur des techniques de réécriture couplées à une méthode par abstraction. Les théories sortées telles que l’arithmétique linéaire sont intégrés par injection dans la logique multi-sortée. La deuxième composante est un algorithme pour la synthèse des types dans les formules (non-typées) TLA+. L’algorithme, qui est basé sur la résolution des contraintes, met en oeuvre un système de type avec types élémentaires, similaires à ceux de la logique multi-sortée, et une extension avec des types dépendants et par raffinement. Les informations de type obtenues sont ensuite implicitement exploitées afin d’améliorer la traduction. Cette approche a pu être validé empiriquement permettant de démontrer que les vérificateurs ATP/SMT augmentent de manière significative le développement des preuves dans TLAPS / This thesis presents effective techniques for discharging TLA+ proof obligations to automated theorem provers based on unsorted and many-sorted first-order logic. TLA+ is a formal language for specifying and verifying concurrent and distributed systems. Its non-temporal fragment is based on a variant of Zermelo-Fraenkel set theory for specifying the data structures. The TLA+ Proof System TLAPS is an interactive proof environment in which users can deductively verify safety properties of TLA+ specifications. While TLAPS is a proof assistant that relies on users for guiding the proof effort, it generates proof obligations and passes them to backend verifiers to achieve a satisfactory level of automation. We developed a new back-end prover that soundly integrates into TLAPS external automated provers, specifically, ATP systems and SMT solvers. Two main components provide the formal basis for implementing this new backend. The first is a generic translation framework that allows to plug to TLAPS any automated prover supporting the standard input formats TPTP/FOF or SMT-LIB/AUFLIA. In order to encode higher-order expressions, such as sets by comprehension or total functions with domains, the translation to first-order logic relies on term-rewriting techniques coupled with an abstraction method. Sorted theories such as linear integer arithmetic are homomorphically embedded into many-sorted logic. The second component is a type synthesis algorithm for (untyped) TLA+ formulas. The algorithm, which is based on constraint solving, implements one type system for elementary types, similar to those of many-sorted logic, and an expansion with dependent and refinement types. The obtained type information is then implicitly exploited to improve the translation. Empirical evaluation validates our approach: the ATP/SMT backend significantly boosts the proof development in TLAPS