Mathematical definitions provide a precise, unambiguous way to formulate concepts. They also provide a common language between disciplines. Thus, they are the basis for a well-founded scientific discussion. In addition, mathematical definitions allow for deeper insights into the defined subject based on mathematical theorems that are incontrovertible under the given definition. Besides their value in mathematics, mathematical definitions are indispensable in other sciences like physics, chemistry, and computer science. In computer science, they help to derive the expected behavior of a computer program and provide guidance for the design and testing of software. Therefore, mathematical definitions can be used to design and implement advanced algorithms. One class of widely used algorithms in computer science is the class of particle-based algorithms, also known as particle methods. Particle methods can solve complex problems in various fields, such as fluid dynamics, plasma physics, or granular flows, using diverse simulation methods, including Discrete Element Methods (DEM), Molecular Dynamics (MD), Reproducing Kernel Particle Methods (RKPM), Particle Strength Exchange (PSE), and Smoothed Particle Hydrodynamics (SPH). Despite the increasing use of particle methods driven by improved computing performance, the relation between these algorithms remains formally unclear. In particular, particle methods lack a unifying mathematical definition and precisely defined terminology. This prevents the determination of whether an algorithm belongs to the class and what distinguishes the class. Here we present a rigorous mathematical definition for determining particle methods and demonstrate its importance by applying it to several canonical algorithms and those not previously recognized as particle methods. Furthermore, we base proofs of theorems about parallelizability and computational power on it and use it to develop scientific computing software. Our definition unified, for the first time, the so far loosely connected notion of particle methods. Thus, it marks the necessary starting point for a broad range of joint formal investigations and applications across fields.:1 Introduction 1.1 The Role of Mathematical Definitions 1.2 Particle Methods 1.3 Scope and Contributions of this Thesis 2 Terminology and Notation 3 A Formal Definition of Particle Methods 3.1 Introduction 3.2 Definition of Particle Methods 3.2.1 Particle Method Algorithm 3.2.2 Particle Method Instance 3.2.3 Particle State Transition Function 3.3 Explanation of the Definition of Particle Methods 3.3.1 Illustrative Example 3.3.2 Explanation of the Particle Method Algorithm 3.3.3 Explanation of the Particle Method Instance 3.3.4 Explanation of the State Transition Function 3.4 Conclusion 4 Algorithms as Particle Methods 4.1 Introduction 4.2 Perfectly Elastic Collision in Arbitrary Dimensions 4.3 Particle Strength Exchange 4.4 Smoothed Particle Hydrodynamics 4.5 Lennard-Jones Molecular Dynamics 4.6 Triangulation refinement 4.7 Conway's Game of Life 4.8 Gaussian Elimination 4.9 Conclusion 5 Parallelizability of Particle Methods 5.1 Introduction 5.2 Particle Methods on Shared Memory Systems 5.2.1 Parallelization Scheme 5.2.2 Lemmata 5.2.3 Parallelizability 5.2.4 Time Complexity 5.2.5 Application 5.3 Particle Methods on Distributed Memory Systems 5.3.1 Parallelization Scheme 5.3.2 Lemmata 5.3.3 Parallelizability 5.3.4 Bounds on Time Complexity and Parallel Scalability 5.4 Conclusion 6 Turing Powerfulness and Halting Decidability 6.1 Introduction 6.2 Turing Machine 6.3 Turing Powerfulness of Particle Methods Under a First Set of Constraints 6.4 Turing Powerfulness of Particle Methods Under a Second Set of Constraints 6.5 Halting Decidability of Particle Methods 6.6 Conclusion 7 Particle Methods as a Basis for Scientific Software Engineering 7.1 Introduction 7.2 Design of the Prototype 7.3 Applications, Comparisons, Convergence Study, and Run-time Evaluations 7.4 Conclusion 8 Results, Discussion, Outlook, and Conclusion 8.1 Problem 8.2 Results 8.3 Discussion 8.4 Outlook 8.5 Conclusion

Software developers adapt to the fast-moving nature of software systems with agile development techniques. However, database developers lack the tools and concepts to keep the pace. Whenever the current database schema is evolved, the already existing data needs to be evolved as well. This is usually realized with manually written SQL scripts, which is error-prone and explains significant costs in software projects. A promising solution are declarative database evolution languages, which couple both schema and data evolution into intuitive operations. Existing database evolution languages focus on usability but do not strive for completeness. However, this is an inevitable prerequisite to avoid complex and error-prone workarounds. We present CODEL which is based on an existing language but is relationally complete. We precisely define its semantic using relational algebra, propose a syntax, and formally validate its relational completeness. Having a complete and comprehensive database evolution language facilitates valuable support throughout the whole evolution of a database. As an instance, we present VACO, a tool supporting developers with variant co-evolution. Given a variant schema derived from a core schema, VACO uses the richer semantics of CODEL to semi-automatically co-evolve this variant with the core.

European greenhouse gas (GHG) emissions have decreased by 24% between 1990 and 2019 according to a report by the European Commission. Yet, the Paris agreement set a target of 55% by 2030 to prevent the effects of climate change and prepare for carbon neutrality by 2050. Achieving this goal requires decarbonization efforts to be four times faster than current rates, and carbon accounting will play an essential role for identifying emission sources and developing emission reduction strategies. However, carbon accounting still suffers a lack of consistency and standardization due to different methods and incomplete scope, leading to confusion and incomparability. This thesis proposes a comprehensive and innovative methodology for carbon accounting that ensures transparency, comparability, accuracy, and completeness. Using an iterative approach and a unique representation for carbon architecture, the methodology covers crucial steps such as identifying emission sources, selecting emission factors, determining calculation methods, displaying results, and simulating emission reduction scenarios. A new reliability measurement is also introduced to assess the quality of each emission estimate. The methodology was successfully implemented in the concrete example of a company seeking to reduce the carbon impact of its activities. The limitations of the thesis are addressed in the conclusion. / Europeiska växthusgasutsläpp har minskat med 24% mellan 1990 och 2019 enligt en rapport från Europeiska kommissionen. Trots detta har Parisavtalet satt upp ett mål på 55% till år 2030 för att förhindra klimatförändringarnas effekter och förbereda för koldioxidneutralitet år 2050. För att uppnå detta mål krävs att avkolningsansträngningarna fyrdubblas i jämförelse med nuvarande takt, och koldioxidredovisning kommer att spela en avgörande roll för att identifiera utsläppskällor och utveckla strategier för utsläppsminskning. Dock lider koldioxidredovisning fortfarande av brist på konsekvens och standardisering på grund av olika metoder och ofullständig omfattning, vilket leder till förvirring och bristande jämförbarhet. Denna avhandling föreslår en omfattande och innovativ metodik för koldioxidredovisning som säkerställer transparens, jämförbarhet, noggrannhet och fullständighet. Genom att använda en iterativ ansats och en unik representation av koldioxidarkitektur täcker metoden viktiga steg såsom att identifiera utsläppskällor, välja utsläppsfaktorer, bestämma beräkningsmetoder, visa resultat och simulera scenarier för utsläppsminskning. En ny pålitlighetsmätning introduceras också för att bedöma kvaliteten på varje utslagsuppskattning. Metoden implementerades framgångsrikt i det konkreta exemplet med ett företag som sökte minska den koldioxidpåverkan av sina verksamheter. Begränsningarna med avhandlingen diskuteras i slutsatsen.

Matching concept descriptions against concept patterns was introduced as a new inference task in Description Logics (DLs) almost 20 years ago, motivated by applications in the Classic system. For the DL EL, it was shown in 2000 that the matching problem is NP-complete. It then took almost 10 years before this NP-completeness result could be extended from matching to unification in EL. The next big challenge was then to further extend these results from matching and unification without a TBox to matching and unification w.r.t. a general TBox, i.e., a finite set of general concept inclusions. For unification, we could show some partial results for general TBoxes that satisfy a certain restriction on cyclic dependencies between concepts, but the general case is still open. For matching, we solve the general case in this paper: we show that matching in EL w.r.t. general TBoxes is NP-complete by introducing a goal-oriented matching algorithm that uses non-deterministic rules to transform a given matching problem into a solved form by a polynomial number of rule applications. We also investigate some tractable variants of the matching problem.

[pt] Segerberg apresentou uma prova geral da completude para lógicas proposicionais. Para tal, um sistema de dedução foi definido de forma que suas regras sejam regras para um operador booleano arbitrário para uma dada lógica proposicional. Cada regra desse sistema corresponde a uma linha na tabela de verdade desse operador. Na primeira parte desse trabalho, mostramos uma extensão da ideia de Segerberg para lógicas proposicionais finito-valoradas e para lógicas não-determinísticas. Mantemos a ideia de definir um sistema de dedução cujas regras correspondam a linhas de tabelas verdade, mas ao invés de termos um tipo de regra para cada valor de verdade da lógica correspondente, usamos uma representação bivalente que usa a técnica de fórmulas separadoras definidas por Carlos Caleiro e João Marcos. O sistema definido possui tantas regras que pode ser difícil trabalhar com elas. Acreditamos que um sistema de cálculo de sequentes definido de forma análoga poderia ser mais intuitivo. Motivados por essa observação, a segunda parte dessa tese é dedicada à definição de uma tradução entre cálculo de sequentes e dedução natural, onde procuramos definir uma bijeção melhor do que as já existentes. / [en] Segerberg presented a general completeness proof for propositional logics. For this purpose, a Natural Deduction system was defined in a way that its rules were rules for an arbitrary boolean operator in a given propositional logic. Each of those rules corresponds to a row on the operator s truth-table. In the first part of this thesis we extend Segerbergs idea to finite-valued propositional logic and to non-deterministic logic. We maintain the idea of defining a deductive system whose rules correspond to rows of truth-tables, but instead of having n types of rules (one for each truth-value), we use a bivalent representation that makes use of the technique of separating formulas as defined by Carlos Caleiro and João Marcos. The system defined has so many rules it might be laborious to work with it. We believe that a sequent calculus system defined in a similar way would be more intuitive. Motivated by this observation, in the second part of this thesis we work out translations between Sequent Calculus and Natural Deduction, searching for a better bijective relationship than those already existing.

In dieser Arbeit studieren wir Lorentz-Mannigfaltigkeiten mit spezieller Holonomie, d.h. ihre Holonomiedarstellung wirkt schwach-irreduzibel aber nicht irreduzibel. Aufgrund der schwachen Irreduzibilität lässt die Darstellung einen ausgearteten Unterraum invariant und damit also auch eine lichtartige Linie. Geometrisch hat dies zur Folge, dass wir zwei parallele Unterbündel (die Linie und ihr orthogonales Komplement) des Tangentialbündels erhalten. Diese Arbeit nutzt diese und weitere Objekte um zu beweisen, dass kompakte Lorentzmannigfaltigkeiten mit Abelscher Holonomie geodätisch vollständig sind. Zudem werden Lorentzmannigfaltigkeiten mit spezieller Holonomie und nicht-negativer Ricci-Krümung auf den Blättern der Blätterung, induziert durch das orthogonale Komplement der parellelen Linie, und maximaler erster Bettizahl untersucht. Schließlich werden vollständige Ricci-flache Lorentzmannigfaltigkeiten mit vorgegebener voller Holonomie konstruiert. / In the present thesis we study dimensional Lorentzian manifolds with special holonomy, i.e. such that their holonomy representation acts indecomposably but non-irreducibly. Being indecomposable, their holonomy group leaves invariant a degenerate subspace and thus a light-like line. Geometrically, this means that, since being holonomy invariant, this line gives rise to parallel subbundles of the tangent bundle. The thesis uses these and other objects to prove that Lorentian manifolds with Abelian holonomy are geodesically complete. Moreover, we study Lorentzian manifolds with special holonomy and non-negative Ricci curvature on the leaves of the foliation induced by the orthogonal complement of the parallel light-like line whose first Betti number is maximal. Finally, we provide examples of geodesically complete and Ricci-flat Lorentzian manifolds with special holonomy and prescribed full holonomy group.

Made available in DSpace on 2016-04-27T17:27:11Z (GMT). No. of bitstreams: 1 Cassia Sampaio Sanctos.pdf: 875084 bytes, checksum: 3baa23ce43e41c748fa70bf983f30e20 (MD5) Previous issue date: 2015-05-11 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The thesis constitutes a critical review of Gödel´s doctoral dissertation which presents a proof for the completeness of first order logic. The introduction addresses the concepts of formalism, axiomatic method and completeness, thus the proof can be contextualized. The language for the restricted functional calculus is defined, with the corresponding syntax and semantics, and the original Gödel´s demonstration is updated. The appendix contains a translation of the referred dissertation, which is unprecedented in Portuguese / O trabalho constitui um comentário crítico da dissertação de doutorado de Gödel que apresenta uma prova de completude da lógica de primeira ordem. A introdução trata dos conceitos de formalismo, método axiomático e completude, para que seja possível contextualizar a prova. A linguagem para o cálculo funcional restrito é definida, com sua sintaxe e semântica, e a demonstração original de Gödel é atualizada. O apêndice contém a tradução da referida dissertação, que é inédita em língua portuguesa

La notion de T-radical d’un idéal permet à G.Cherlin de démontrer un Nullstellensatz dans les théories inductives d’anneaux. Nous proposons une analyse modèle-théorique de phénomènes connexes. En premier lieu, une réciproque de ce théorème nous conduit à une caractérisation des corps algébriquement clos, suggérant une version “positive” du travail de Cherlin, la théorie des idéaux T-radiciels. Ceux-ci se caractérisent par un théorème de représentation et sont associés à un théorème des zéros “positif”. Ces résultats se généralisent à la logique du premier ordre : grâce à la notion de classe spéciale, nous développons ensuite une théorie logique des idéaux. On peut encore parler d’idéaux premiers et radiciels, relativement à une classe de structures. Dans ce cadre, le théorème de représentation est une propriété intrinsèque des classes spéciales et le théorème des zéros une propriété de préservation logique, que nous appelons “complétude géométrique” et qui entretient des rapports étroits avec la modèle-complétude positive. Les algèbres basées en groupes de P.Higgins permettent d’appliquer ces résultats aux théories modèle-complètes de corps avec opérateurs additionnels. Dans certains cas “noethériens”, l’algèbre de coordonnées est un invariant algébrique des “variétés affines”. Enfin, il est possible à partir d’un ensemble de formules E de généraliser les classes spéciales et autres classes de structures. Notre théorie des idéaux logiques est de plus un cas particulier du phénomène de localisation étudié par M.Coste ; dans certaines situations, un bon choix de formules permet d’identifier les types complets d’une “algèbre” à des types de localisation / The notion of T-radical of an ideal allows G.Cherlin to prove a Nullstellensatz for inductive ring theories.We present here a model-theoretic analysis of closely related phenomena. At first, a reverse of this theorem leeds us to a characterization of algebraically closed fields, suggesting a “positive” version of Cherlin’s work, the theory of T-radical ideals. These are characterized by a representation theorem and associated to a “positive” Nullstellensatz. Those results are generalized to first order logic : thanks to the notion of special class, we then develop a logical theory of ideals. One may still speak about prime and radical ideals, relatively to a class of structures. In this setting, the representation theorem is an intrinsic property of special classes and the Nullstellensatz a logical preservation property, which we call “geometric completeness” and which is closely linked to positive model-completeness. The group-based algebras of P.Higgins allow us to apply these results to model-complete theories of fields with additional operators. In certain “noetherian” cases, the coordinate algebra is an algebraic invariant of “affine algebraic sets”. At last, it is possible from a set of formulas E to generalize special and other classes of structures. Moreover, our theory of logical ideals is a particular case of the localisation phenomenon studied by M.Coste ; in certain situations, a good choice of formulasleeds to an identification of the complete types of a given “algebra” with some localisation types

Jämförbarhet i hållbarhetsrapporten är en nödvändighet för att informationen ska vara användbar för användarna. För att främja jämförbar information ska svenska företag följa hållbarhetslagen som bygger på EU-direktivet om hållbarhetsrapportering. Till sin hjälp kan företagen tillämpa internationella frivilliga ramverk som exempelvis Global Reporting Initiative (GRI). I och med att det finns ett flertal frivilliga ramverk att tillämpa kan företagen välja ifall dem vill följa något ramverk, med det utgör inget krav, för att uppfylla hållbarhetslagen. Detta utrymme av frivillighet bidrar till den stora variation i antalet resultatindikatorer som företagen lämnar upplysningar om i hållbarhetsrapporten, vilket gör att informationen inte blir jämförbar. Denna studie vill bidra med kunskap till forskningsfältet genom att (1) kartlägga jämförbarheten i hållbarhetsrapporter i form av hur utförligt företagen noterade på Stockholmsbörsen Large Cap tillämpar resultatindikatorer till rapporteringskravets kategorier och (2) förklara och analysera sambandet mellan företagens branschtillhörighet, företagens andel kvinnor i styrelsen och utförlighetsnivån i hållbarhetsrapporter som omfattas av hållbarhetslagen. För att besvara studiens syfte genomfördes en kvantitativ innehållsanalys av samtliga företag som uppfyllde kriterierna för hållbarhetsrapportering och GRI:s ramverk på Stockholmsbörsen Large Cap. Resultatet visade att båda sambanden var relativt svaga. Sambandet för företagens branschtillhörighet visade sig något starkare jämfört med andelen kvinnor i styrelsen. Det tyder på att det finns andra underliggande faktorer som påverkar jämförbarheten i hållbarhetsrapporten. / The comparability in the sustainability report is a necessity to serve its main purpose, which is to be useful for the stakeholders. To encourage comparable information in the sustainability report, Swedish companies must comply with the national sustainability law, which is based on the EU directive of sustainability reporting. To comply with the national sustainability law companies can apply international voluntary frameworks such as Global Reporting Initiative (GRI), but there is no imperative requirement. All the voluntary frameworks may contribute to the observed differences of indicators disclosed in the sustainability reports, which makes the information not comparable. This study contributes to the field of research by (1) mapping the comparability in the sustainability reports of firms listed on the Stockholm Stock Exchange Large Cap by investigating the level of completeness for the reporting requirements categories and (2) explain and analyse the correlation between the company´s sector, board diversity and the level of completeness of firms that are covered by the national sustainability law. Therefore, a quantity content analysis was conducted on all companies in our sample. The findings display a weak relationship between the investigated variables. This suggest that there are other underlying factors that may affect the comparability in the sustainability reports.

We address the challenge of providing low-cost, universal access of useful information to people in different parts of the globe. We achieve this by following two strategies. First, we focus on the delivery of information through computerized devices and prototype new methods for making that delivery possible in a secure, low-cost, and universal manner. Second, we focus on the use of participatory media, such as blogs, in the context of news related content, and develop methods to recommend useful information that will be of interest to users. To achieve the first goal, we have designed a low-cost wireless system for Internet access in rural areas, and a smartphone-based system for the opportunistic use of WiFi connectivity to reduce the cost of data transfer on multi-NIC mobile devices. Included is a methodology for secure communication using identity based cryptography. For the second goal of identifying useful information, we make use of sociological theories regarding social networks in mass-media to develop a model of how participatory media can offer users effective news-related information. We then use this model to design a recommender system for participatory media content that pushes useful information to people in a personalized fashion. Our algorithms provide an order of magnitude better performance in terms of recommendation accuracy than other state-of-the-art recommender systems. Our work provides some fundamental insights into the design of low-cost communication systems and the provision of useful messages to users in participatory media through a multi-disciplinary approach. The result is a framework that efficiently and effectively delivers information to people in remote corners of the world.