Search

To study and get intuition on different types of relational algebras (groups, semigroups, and their ordered versions, quasigroups, fields, rings, MV-algebras, lattices, etc.), mathematicians resort to libraries of all models, up to isomorphism, of order n (for small values of n) of the classes of algebras they are interested in. These libraries allow experimentation such as forming and/or testing conjectures etc., to gain insights into the classes of algebras in question. Since an isomorphism partitions the set of all models into equivalence classes, so, only one representative element in each equivalence class is needed. The rest of them are redundant and are removed to make it easy to discern the structure of the algebras. To construct these libraries, we need first to find all models up to isomorphism of the classes of algebras of interest. Enumerating all finite models from first-order formulas up to isomorphism is a hard problem, even for algebras of small orders. The current best practice of finite model enumeration is to divide the job into two steps: first generate models according to the laws laid down by the first-order formula defining the class of algebra, then in the post-processing step, find only one representative model of each equivalence class of isomorphic models. An algebra of finite order n defined by a first-order formula can be represented by operation tables (also known as multiplication tables) of finite sizes. Traditional finite model enumerators such as Mace4 basically perform combinatorial search on these operation tables to find instances that satisfy, or equivalently, not violate, the rules laid down by the first-order formula. This is a hard problem. For example, there are n n 2 possible binary operation tables of size n × n with n possible values in each cell. That is, even to enumerate all models of order 4 defined with just one binary operation in its first-order formula, we are facing the task of checking 4 4 2 ≈ 4.3 billion possibilities. Traditional finite model enumerators also produce a lot of isomorphic models to the extent that isomorphism models often constitute over 99% of the outputs. This is a characteristics of algebras definable by FOL: any permutation on the domain elements of a model is a model. Finding non-isomorphic models is very computationally intensive. If we follow a simple brute-force approach, then, given m models, it may require in the worst case m(m −1)/2 comparisons of models to check for isomorphism. Each comparison of models of order n may require in the worst case n! checks because there are n! different permutations on n symbols. Thus, both of these two steps (generating models from FOL and removing isomorphic models) are resource-intensive. They prompt us to find better algorithms that also make optimal use of the available computing resources. The matter is further complicated by the fact that while modern-day generalpurpose computers are predominantly multi-core, harnessing parallelism for combinatorial search is surprisingly difficult. In this thesis, we propose the isomorphic cubes removal algorithm and the parallel cubes search algorithm to improve the speed of the traditional finite model enumerator. Searching the operation tables can be seen as searching a search tree. Any partial branch from the root (called a cube) can be searched in parallel with other branches, making full use of the computing resources available. Furthermore, some (isomorphic) cubes produce isomorphic models and hence only one of them needs to be searched. Removing isomorphic cubes not only speeds up the search process, but also reduces the number of isomorphic models that need to be removed in the post-processing step. These parallel algorithms are very scalable: more cubes can be generated if more computing resources are available. They also cope with big problems well: longer cubes are possible with higher orders of algebra; with longer cubes, more isomorphic cubes can be removed. To speed up the isomorphic models removal process, we propose the parallel invariant-based isomorphic model removal algorithms. We note that models with different sets of invariant vectors (ordered list of invariants) cannot be isomorphic. We put models into blocks in a hash-table using invariant vectors as the keys. Models across different blocks thus have different sets of invariant vectors and hence cannot be isomorphic. These blocks of models can be checked for isomorphism separately in parallel. The improvement in speed comes from (1) smaller block size means fewer pairs of models to compare for isomorphism, (2) the blocks can be processed in parallel, making full use of the computing resources available. These algorithms also cope with big problems well: models of higher orders give more different invariant vectors to spread out the models. These algorithms together often give an improvement of orders of magnitude in the performance of the traditional finite model enumerators. Better yet, these algorithms can be incorporated in many common finite model enumerators with minimal change in their code base. Furthermore, the proposed algorithms are proved to be correct. In any mathematical research, humans are the most important factor to be given considerations. Not all mathematicians are computer experts, and not all of them want to invest their valuable time in the tools of mathematics. Thus, the tools must be designed to be user-friendly, without a steep learning curve for the user to be able to use the tools effectively. We therefore develop a GAP package generator to automatically generate GAP package for algebras of small orders. The generator hides the technical details of the generation process, but gives users the ability to control many of the non-technical aspects such as the name and the definition (in FOL) of the algebra to be explored. The GAP package generator makes extensive use of the facilities provided by the GAP system, and the generated package complies with the latest GAP standards. A separate, standalone GAP package, Magmaut, is developed to provide functions to manipulate isomorphism and automorphism for algebras of type (2 m, 1 n). It supplements the generated GAP package of algebra of small orders with isomorphism-related functionality. With the tools provided by this project, mathematicians can generate the GAP packages of algebras of type (2 m, 1 n) of their interest, without being bogged down by the complexity that often comes with the tools that generate such GAP packages. In this thesis, we propose many parallel algorithms to take advantage of modern-day multi-core computers to enumerate finite models. We show some important applications of these algorithms in developing GAP packages to calculate different morphisms such as isomorphism and monomorphism etc., in generating GAP packages of algebras, and in counting the number of algebras of small orders. We also develop a user-friendly tool to help mathematicians to generate GAP packages of algebras (of type (2 m, 1 n)) of small orders. Para estudar e compreender diferentes tipos de álgebras relacionais (grupos, semigrupos e suas versões ordenadas, quasigrupos, corpos, anéis, MV- álgebras, reticulados, etc.), os matemáticos recorrem a bibliotecas de todos os modelos, a menos de isomorfismo, de ordem n (para pequenos valores de n) de classes de álgebras de seu interesse. Essas bibliotecas permitem experimentação, como formular e/ou testar conjeturas, etc., para obter intuição sobre as classes de álgebras em questão. Como um isomorfismo divide o conjunto de todos os modelos em classes de equivalência, apenas um elemento representativo em cada classe de equivalência é necessário. Os demais são redundantes e foram removidos para melhor se entender a estrutura das álgebras. Para construir essas bibliotecas, precisamos encontrar todos os modelos a menos de isomorfismo de classes de álgebras em que estamos interessados. Enumerar todos os modelos finitos de fórmulas de álgebras de primeira ordem a menos de isomorfismo é um problema difícil, mesmo para álgebras de ordens pequenas. Atualmente, a melhor estratégia de enumeração de modelos finitos é dividir o trabalho em duas fases: primeiro, gerir modelos de acordo com as leis estabelecidas pela fórmula de primeira ordem que definem a álgebra, depois, na etapa de pós-processamento, encontrar apenas um modelo representativo de cada classe de equivalência de modelos isomórficos. Uma álgebra de ordem finita não definida com fórmulas de primeira ordem, pode ser representada por tabelas de operações (também conhecidas como multiplicação) de tamanhos finitos. Os enumeradores de modelos finitos tradicionais, como Mace4, basicamente executam pesquisas combinatórias nessas tabelas de operação para encontrar instâncias que satisfaçam, ou equivalentemente, não violem as regras estabelecidas pela fórmula de primeira ordem. Isto constitui um enorme problema. Por exemplo, existem nn 2 possíveis tabelas de operações binárias de tamanho n × n com n valores possíveis em cada célula. Ou seja, mesmo para enumerar todos os modelos de ordem 4 para uma álgebra definida com apenas uma operação binária em sua fórmula de primeira ordem, estamos diante da tarefa de verificar 442 ≈ 4.3 mil milhões de possibilidades. Os enumeradores de modelos finitos tradicionais também produzem muitos modelos isomórficos na medida em que os modelos de isomorfismo geralmente constituem mais de 99% das saídas. Esta é uma característica das álgebras definíveis por FOL: qualquer permutação nos elementos de domínio de um modelo é um modelo. Encontrar modelos não isomórficos é computacionalmente muito dispendioso. Se seguirmos uma abordagem simples de força bruta, então, dados os modelos m, pode ser necessário, no pior caso, m (m − 1)/2 comparações de modelos para verificar o isomorfismo. Cada comparação de modelos de ordem n não pode exigir, no pior caso, n! verificações porque existem n! permutações diferentes nos símbolos n. Assim, essas duas etapas (gerar modelos de FOL e remover modelos isomórficos) consomem muitos recursos. Somos assim impelidos a encontrar algoritmos melhores que façam uso otimizado dos recursos de computação disponíveis. A questão é ainda mais complicada pelo fato de que, embora os computadores modernos de uso geral sejam predominantemente multi-core, aproveitar o paralelismo para a pesquisa combinatória é surpreendentemente difícil. Nesta tese, propomos o algoritmo de remoção de cubos isomórficos e o algoritmo de busca de cubos paralelos para melhorar a velocidade do enumerador de modelos finitos tradicional. A pesquisa nas tabelas de operações pode ser vista como uma pesquisa numa árvore de pesquisa. Qualquer ramo parcial da raiz (chamado cubo) pode ser pesquisado em paralelo com outros ramos, fazendo pleno uso dos recursos computacionais disponíveis. Além disso alguns cubos produzem modelos isomórficos e, portanto, apenas um deles precisa ser pesquisado. A remoção de cubos isomórficos não apenas acelera o processo de busca, mas também reduz o número de modelos isomórficos que precisam ser removidos na etapa de pós-processamento. Esses algoritmos paralelos são muito escaláveis: mais cubos podem ser gerados se mais recursos de computação estiverem disponíveis. Eles também lidam bem com grandes problemas: cubos mais longos são possíveis com ordens mais altas de álgebra; com cubos mais longos, cubos mais isomórficos podem ser removidos. Para acelerar o processo de remoção de modelos isomórficos, propomos os algoritmos de remoção de modelos isomórficos baseados em invariantes paralelos. Notamos que modelos com diferentes conjuntos de vetores invariantes não podem ser isomórficos. Colocamos modelos em blocos numa tabela de hash usando vetores invariantes como chaves. Modelos em diferentes blocos, portanto, têm diferentes conjuntos de vetores invariantes e, portanto, não podem ser isomórficos. Esses blocos de modelos podem ser verificados quanto ao isomorfismo, separadamente, em paralelo. A melhoria na velocidade obtém-se por (1) tamanho de bloco menor significa menos pares de modelos para comparar em termos de isomorfismo, (2) os blocos podem ser processados em paralelo, fazendo pleno uso dos recursos computacionais disponíveis. Esses algoritmos também lidam bem com grandes problemas: modelos de ordens mais altas fornecem mais vetores invariantes o que permite maior dispersão dos modelos. A junção desses algoritmos geralmente permite uma acentuada melhoria no desempenho dos enumeradores de modelos finitos tradicionais. Melhor ainda, esses algoritmos podem ser incorporados em muitos enumeradores de modelos finitos comuns com alterações mínimas no seu código base. Além disso, os algoritmos propostos são comprovadamente corretos. Em qualquer pesquisa matemática, o ser humano é o fator mais importante a ser considerado. Nem todos os matemáticos são especialistas em computação e nem todos querem investir o seu valioso tempo em ferramentas matemáticas. Assim, as ferramentas devem ser projetadas para serem fáceis de usar, sem uma curva de aprendizagem íngreme para que o utilizador possa usar as ferramentas de forma eficaz. Nesse sentido, desenvolvemos um gerador de pacotes GAP para gerar automaticamente pacotes GAP para álgebras de pequenas ordens. O gerador oculta os detalhes técnicos do processo de geração, mas dão aos utilizadores a capacidade de controlar muitos dos aspetos não técnicos, como o nome e a definição (em FOL) da álgebra a ser explorada. O gerador de pacotes GAP faz uso extensivo das facilidades fornecidas pelo sistema GAP, e o pacote gerado está em conformidade com os padrões GAP mais recentes. Um pacote GAP separado e autónomo, Magmaut, é desenvolvido para fornecer funções que permitam a manipulação de isomorfismos e automorfismos para álgebras do tipo (2m, 1n). Ele complementa o pacote GAP gerado para álgebra de pequenas ordens com funcionalidades relacionadas com o isomorfismo. Com as ferramentas fornecidas por este projeto, os matemáticos podem gerar os pacotes GAP de álgebras do tipo (2m, 1n) de seu interesse, sem se prenderem à complexidade que muitas vezes vem com as ferramentas que geram tais pacotes GAP. Nesta tese, propomos ainda muitos algoritmos paralelos para aproveitar os computadores multinúcleos modernos para enumerar modelos finitos de álgebras. Mostramos algumas aplicações importantes desses algoritmos no desenvolvimento de pacotes GAP para calcular diferentes morfismos como isomorfismo e monomorfismo etc., na geração de pacotes GAP de álgebras e na contagem do número de álgebras de pequenas ordens. Também desenvolvemos uma ferramenta de fácil utilização para ajudar os matemáticos a gerar pacotes GAP de álgebras (do tipo (2m, 1n)) de pequenas ordens.

Este trabajo nace del reto que supone enfrentarse a las redes neuronales invariantes a permutación y tamaño de entrada, que hasta la fecha es algo novedoso y poco explorado debido a su complejidad computacional. Sin embargo, estas redes neuronales son muy expresivas y hacen que sea posible trabajar a nivel de conjuntos (p.e. nubes de puntos 2D y 3D, tramas de vídeo, grafos, etc). Nuestra labor en este proyecto será la aportación de un framework que nos permita entender el funcionamiento de estas arquitecturas, desde la codificación los datos, hasta qué operaciones invariantes son las más efectivas en la actualidad. Por ello, se incluirá, aparte del código fuente, una serie de tutoriales (notebooks) con las diferentes variantes de estas arquitecturas y distintos conjuntos de datos. Cabe mencionar que en los tutoriales abordaremos tanto tareas de clasificación como de regresión con cada una de las variantes de las arquitecturas. Por último, aportaremos un método explicativo específico para estas arquitecturas: SetXAI, cuyo funcionamiento podrá ser tanto estático como dinámico (por épocas). SetXAI obtiene aquellos puntos de mayor criticidad, es decir, aquellos que nos aporten mayor información para la clasificación o regresión. Nuestros experimentos aportarán evidencia acerca de la capacidad de los puntos críticos para resumir los conjuntos de entrada y realizar por sí solos la tarea de clasificación o regresión.

Diese Arbeit besteht aus zwei Teilen. Im ersten Teil untersuchen wir das Erzwingen von topologischer Entropie f��r Reeb-Fl��sse auf geschlossenen 3-Mannigfaltigkeiten. Als Anwendung eines Strukturtheorems zeigen wir, dass es auf jeder kontakt-3-Mannigfaltigkeit transversale Knoten gibt, welche die topologische Entropie erzwingen. Au��erdem verallgemeinern wir ein Theorem von Denvir-Mackay f��r geod��tische Fl��sse auf \(\it{T}\)\(^{2} \) und \(\it{S}\)\(^{2} \) auf eine Klasse von Reeb-Fl��ssen auf \(\it{T} \)\(_{1} \)\(\it{T}\)\(^2 \) und \(\it {T}\)\(_{1}\)\(\it{S}\)\(^2 \). Im zweiten Teil untersuchen wir die Beziehung zwischen der mittleren Wirkung periodischer Punkte und der Calabi-Invariante f��r fl��chenerhaltende Scheibendiffeomorphismen mit negativer Calabi-Invariante., This thesis consists of two parts. In the first part, we explore forcing of topological entropy for Reeb flows on closed three-manifolds. As an application of a structural theorem, we show that on every contact 3-manifold, there exist transverse knots which force topological entropy. We also generalize a theorem of Denvir-Mackay for geodesic flows on \(\it{T}\)\(^2\) and \(\it{S}\)\(^2\) to a class of Reeb flows on \(\it{T}\)\(_{1}\)\(\it{T}\)\(^2\) und \(\it{T}\)\(_{1}\) \(\it{S}\)\(^2\). In the second part, we study the relation of the mean action of periodic orbits and the Calabi invariant for area-preserving disc diffeomorphisms with negative Calabi invariant.

Il tetto e il giardino: due invarianti che incarnano le idee del chiudere la costruzione verso il cielo e dell’accogliere la natura nella vita domestica e civile dell’uomo. Tali invarianti sono tradotte, in un trasferimento scalare di valori, nell’idea di coronamento di pietra della città greca – nell’Acropoli – e nel suolo vegetale della città medievale – nel Campo dei Miracoli di Pisa. Nell’idea del “tetto-giardino” di Le Corbusier, natura del suolo e artificio del coronamento evolvono in un’unica concezione plastica dell’edificio e della città. The roof and the garden; two constants that embody the idea of closing the construction in the direction of the sky and welcoming nature into the domestic and civil life of man. These constants are translated, in a scalar transfer of value, into the idea of the stone crowning of the Greek city – in the Acropolis – and in the green ground of the Medieval city – in the Campo dei Miracoli in Pisa. In Le Corbusier's idea of the “garden-roof” and the artifice of the crowning element evolve in a single plastic conception of the building and of the city., Firenze Architettura, Vol. 23 No. 2 (2019)

We describe normal forms and minimal models of Picard curves, discussing various arithmetic aspects of these. We determine all so-called special Picard curves over $\mathbb{Q}$ with good reduction outside 2 and 3, and use this to determine the smallest possible conductor a special Picard curve may have. We also collect a database of Picard curves over $\mathbb{Q}$ of small conductor., 34 pages

Las leyes Identidad de Género, Matrimonio Igualitario y Reproducción Asistida, promulgadas en nuestro país en los últimos años, causaron una profunda transformación en las políticas de identidad, visibilidad y respeto por las diferencias en la Argentina. El nuevo estatuto legal del matrimonio, que reconoce la posibilidad de sexualidades y familiaridades fuera de la biología y la heterosexualidad obligatoria, así como la libertad de elección del propio género, son una fuente de debates intelectuales a los cuales el psicoanálisis no ha escapado. En los desarrollos recientes sobre sexualidad humana, resuena con insistencia la crítica al falocentrismo del psicoanálisis, como si éste fuera un privilegio del hombre. Siempre se acusó al psicoanálisis de falocéntrico, pero en todo caso más bien se lo ha pensado como penecéntrico. ¿Pero por qué el falo sería el mejor símbolo de lo sexual para los dos sexos? ¿Es por la visibilidad del pene? Lo que Lacan valoriza es que si el falo puede adoptar un valor simbólico lo es debido a la detumescencia y no a su imagen turgente. The Gender Identity, Equal Marriage and Assisted Reproduction Laws, promulgated in our country in recent years, caused a profound transformation in identity policies, visibility and respect for differences in Argentina. The new legal status of marriage, which recognizes the possibility of sexualities and familiarities outside biology and compulsory heterosexuality, as well as the freedom to choose one's own gender, are a source of intellectual debates to which psychoanalysis has not escaped. In recent developments on human sexuality, the critique of the phallocentricism of psychoanalysis resounds insistently, as if it were a privilege of man. Psychoanalysis has always been accused of phallocentric, but in any case it has been thought more of as a peniscentric one. But why would the phallus be the best symbol of the sexual for the both sexes? Is it because of the visibility of the penis? What Lacan values is that if the phallus can adopt a symbolic value it is due to detumescence and not to its turgid image. The authentic dismantling of phallocentrism is not to oppose identities that re-inscribe it and are multiplied in genres, but to make the logic of non-everything appears. Fil: Frazzeto, Marcelo. Universidad Nacional de Rosario. Facultad de Psicología. Rosario; Argentina Fil: Frazzeto, Marcelo. Universidad Nacional de Rosario. Facultad de Psicología. Rosario; Argentina

We study a new combinatorial invariant, separation index. It pretends to size how much connected or not is a graph. Even if it can be define for any graph, on Burton et al. article and on this paper we study it only on 2-sphere triangulations. On section 3 we explain some necessary graph theory results for undertand the rest of the paper. Then on the section 4 we study the separation index, proving the most important results on the article of Burton et al. but also, we include new and original results like Lemma 4.14 and Theorem 4.15. On the following sections, we do an experimental study with the algorithmics implementations on Sage. Grado en Matemáticas

The house has one of the greatest powers of integration for the thoughts, memories and dreams of men. The house, in the life of an individual, overcome men contingencies and multiplies men advice for continuity. Without it, men would be a dispersed human being. The house is body and soul. It is the first world of the human being ... And always, in his dreams, “the house is a large cradle”, as said by Bachelard. There has been a clear evolution of the concept of housing over time. But after all, the house still remains as a reflection of its inhabitants. When a man makes a house his own, we can conclude, he has found what he can call his “morada”. This study is a reflection on the transformation of the house and what is maintained in the dwelling. La casa posee uno de los mayores poderes de integración para los pensamientos, los recuerdos y los sueños del hombre. La casa en la vida del hombre, suplanta contingencias, multiplica sus consejos de continuidad. Sin ella el hombre sería un ser disperso. Es cuerpo y alma. Es el primer mundo del ser humano... Y siempre, en sus sueños, la casa es una gran cuna, como nos dice Bachelard. Ha habido una evidente evolución del concepto de vivienda a lo largo del tiempo, pero aún así todas las moradas siguen siendo reflejo de sus habitantes. La casa y la morada son dos cosas distintas. Cuando un hombre hace suya una casa, encuentra su morada. Este estudio es una reflexión sobre la transformación de la casa y aquello que se mantiene en la morada.

Dentro de la teoría multidimensional de la ansiedad se ha desarrollado el Inventario de Ansiedad Estado Competitiva-2Revisado (csai- 2r) para evaluar la ansiedad somática, ansiedad cognitiva y autoconfi anza en el deporte. El propósito del presente estudio fue evaluar el modelo de medida trifactorial del csai-2r en sus escalas de intensidad y de dirección adaptadas al contexto mexicano, examinando su fi abilidad e invarianza factorial a través del género. Respondieron dichos instrumentos 454 deportistas universitarios (m = 21.15 años de edad; de=2.02). Los resultados ofrecieron apoyo al modelo de tres factores para la escala de intensidad, y confi rmaron su invarianza total en función del género. Para la escala de dirección resultó más adecuado un modelo de dos factores, y se confi rmó su invarianza parcial en función del género. En conclusión, el csai- 2r con ambas escalas de intensidad y dirección adaptadas al contexto mexicano puede ser utilizado para evaluar la ansiedad precompetitiva.

This PhD-Thesis deals with the calculation and application of a new class of invariants, that can be used to recognize patterns in tensor fields (i.e. scalar fields, vector fields und matrix fields), and by the composition of scalar fields with delta-functions also to point-clouds. In the first chapter an overview over already existing invariants is given. In the second chapter the general definition of the new invariants is given: starting with a tensor field a set of moment tensor is created via folding in tensor-product manner with different orders of the tensor product of the positional vector. From these, rotational invariant values are calculated via contraction of tensor products. An algorithm to get a complete and independent set of invariants from a given moment tensor set is described. Furthermore methods to make these sets of invariants invariant against translation, rotation, scaling, and affine transformation. In the third chapter, a method to optimize the calculation of these sets of invariants is described: every invariant can be modeled as undirected graph comprising multiple sub-graphs representing partially contracted tensor products of the moment tensors. The composition of the sets of invariants is optimized by a clever choice of the decomposition into sub-graphs, all paths creating a hyper-graph of sub-graphs where each node describes a composition step. Finally, C++-source-code is created, which optimized using the symmetry of the different tensors and tensor-products, and a comparison of the effort to other calculation methods of invariants is given. The fourth chapter describes the application of the invariants to object recognition in point-clouds from 3D-scans. To do this, the invariants of sub-sets of point-clouds are stored for every known object. Afterwards, invariants are calculated from an unknown point-cloud and tried to find them in the database to assign it to one of the known objects. Benchmarks using three 3D-object databases are made testing time and recognition rate. Diese Dissertation beschäftigt sich mit der Berechnung und Anwendung einer speziellen Klasse von Invarianten, die zum Wiedererkennen von Mustern in Tensorfeldern (also Skalarfeldern, Vektorfeldern und Matrixfeldern) benutzt werden können. Im ersten Kapitel wird ein Überblick Über existierende Invarianten gegeben. Im zweiten Kapitel wird die allgemeine Definition der Invarianten beschrieben: aus einem Tensorfeld wird über eine Tensorprodukt-Faltung mit verschiedenen Ordnungen des Tensorprodukts des Ortsvektors ein Satz von Momententensoren erzeugt, aus denen über Tensorproduktbildung und anschließende vollständige Kontraktion rotationsinvariante Werte berechnet werden. Es wird ein Algorithmus angegeben um einen vollständigen und unabhängigen Satz von diesen Invarianten zu erzeugen, außerdem Methoden, um translative, skalierungs-, und affine Invarianz zu erreichen. Im dritten Kapitel wird eine Methode zur Optimierung der Berechnung dieser Invarianten beschrieben: jede Invariante kann als ungerichteter Graph beschrieben werden, der sich aus mehreren Teilgraphen zusammensetzt, die teilweise kontrahierte Tensorprodukte der Ausgangstensoren darstellen. Es wird versucht, die Komposition der Invarianten Über die Teilgraphen durch geschickte Wahl der Kompositionspfade zu optimieren. Final wird dann C++-Quellcode erzeugt, der unter Ausnutzung der Symmetrie der Tensoren optimiert ist, und ein Vergleich der verschiedenen Berechnungsmethoden der Invarianten gegeben. Das vierte Kapitel beschreibt eine Anwendung der Invarianten auf die Objekterkennung in Punktewolken aus 3D-Scans. Hierbei werden zuerst in einer Datenbank fÜr jedes bekannte Objekt eine Menge von Invarianten aus Auschnitten ihrer Punktewolke gespeichert. Danach werden Invarianten aus einer unbekannten Punktewolke erzeugt und versucht, sie in der Datenbank wiederzufinden und die Punktewolke damit einem Objekt in der Datenbank zuzuordnen.

Una indagación en donde se utilizan algunas de las herramientas con las que hasta hoy se ha intentado estudiar el Romancero de tradición oral moderna y que son representativas de una delicadísima poética preceptuada a lo largo de muchos años por Menéndez Pidal, Diego Catalán y muchos otros. El estudio comparativo de versiones de un mismo poema nos permite establecer hasta qué punto renovación y conservación, los dos motores de este Romancero, afectan con sus diferentes tendencias la continuidad de la tradición, es decir, de las huellas de los romances viejos. El objetivo de este trabajo no es otro que mostrar un ejemplo sobre cuán útil puede sernos el método comparativo en el estudio de la poesía de tradición oral moderna. This is an investigation that makes use of some of the tools that have been employed, till now, in attempts to study the Romance of modern oral tradition, and that are representatives of a very delicate poetics as precepted by Menéndez Pidal, Diego Catalán and many others by many years. A comparative study of different versions of the same poem allows us to ascertain the degree to which renewal and preservation, two axes of this Romance, with their different tendencies, affect the continuity of tradition, that is to say, of the traces of old romances. The aim of this work is to show an example of how useful the comparative method can be for the study of poetry of modern oral tradition. Une recherche où l’on emploie certains outils par les biais desquels on a essayé d’étudier jusqu’au aujourd’hui le Recueil de « romances » espagnols de tradition orale moderne étant représentant d’une très délicate licence poétique étudié tout au long des années par Menéndez Pidal, Diego Catalán parmi d’autres. L’étude comparative de versions d’un poème nous permet d’établir à quel point la renovation et la préservation, les deux moteurs de ce recueil de romances espagnols, touchent avec leurs différentes tendances la continuité de la tradition, c’est-à dire, des traces des vieux romances. Le but de ce travail est de montrer un exemple de l’utilité de l’approche comparative lors de l’étude de la poésie de tradition orale moderne. Un’indagine dove si usano alcun dei metodi con cui è stato studiato il "Romancero" 1 della tradizione orale moderna e che possono essere ritrovati in una delicatissima poetica precettistica portata avanti nel corso degli anni da Menéndez Pidal, Diego Catalán e altri. Lo studio comparativo di diverse versioni dello stesso poema ci permette di stabilire che la rinnovazione e la conservazione,, i due motori di questo Romancero, condizionano, con le sue tendenze, la continuità della tradizione, cioè, le impronte dei vecchi "romances2". Lo scopo di quest’articolo è di dimostrare l’utilità della metodologia comparativa nello studio della poesia di tradizione orale. Foi feita uma indagação onde foramutilizadas algumas das ferramentas com as quaisaté hoje se tentou estudar oRomanceiro de tradição oral moderna e que representam uma delicadíssima poética estabelecidadurante muitos anos por Menéndez Pidal, Diego Catalán e muitos outros. O estudo comparativo de versões de um mesmo poema nos permite determinaraté que ponto a renovação y conservação, os dois motores deste Romanceiro, afetam com suas diferentes tendências a continuidade da tradição, isto é, as marcas dos romances antigos. O objetivo deste trabalho é mostrar um exemplo sobre a utilidadeque pode ter o método comparativo no estudo da poesia de tradição oral moderna.

Cette analyse structurale du mythe littéraire s'appuie sur les travaux de Claude Lévi-Strauss et montre la tension productive entre les notions de structure et de mythe littéraire, tension qui devient la source abondante de signifiants polyphoniques. This in-depth analysis of the structural law which shapes the literary myth is based on Claude Lévi-Strauss’s works, and shows that there exists a fruitful tension between the notions of structure and literary myth, a tension which becomes an abundant source of polyphonic meanings. Con la ayuda de los trabajos de C. Lévi-Strauss, G. Durand y J. Rousset, se intenta dar una brillante análisis de la ley estructural del mito literario. La noción de estructura y la de mito literario mantienen entre sí una tensión fecunda, fuente inagotable de la riqueza polifónica de los significados.

Cette analyse structurale du mythe littéraire s'appuie sur les travaux de Claude Lévi-Strauss et montre la tension productive entre les notions de structure et de mythe littéraire, tension qui devient la source abondante de signifiants polyphoniques.This in-depth analysis of the structural law which shapes the literary myth is based on Claude Lévi-Strauss’s works, and shows that there exists a fruitful tension between the notions of structure and literary myth, a tension which becomes an abundant source of polyphonic meanings.Con la ayuda de los trabajos de C. Lévi-Strauss, G. Durand y J. Rousset, se intenta dar una brillante análisis de la ley estructural del mito literario. La noción de estructura y la de mito literario mantienen entre sí una tensión fecunda, fuente inagotable de la riqueza polifónica de los significados.

Bei der Untersuchung gerahmter Mannigfaltigkeiten ist die Suche nach Repräsentanten der unendlichen Familien in den stabilen Homotopiegruppen der Sphären. Ein wichtiges Mittel hierzu ist die Berechnung der e- und f-Invariante. In dieser Arbeit werden diese Invarianten für komplexe Umrahmungen berechnet. Hierzu wird zunächst ein expliziter Lift der Einschränkung des J-Morphismus konstruiert. Über diesen Lift werden wiederum (U, fr)- und (U, fr)\(^{2}\)-Mannigfaltigkeiten konstruiert um so e- bzw. f-Invariante zu berechnen. Für die Berechnung der e-Invariante kann so die Umrahmung mit der e-Invariante höchster Ordnung bestimmt werden. Für die Berechnung der f-Invariante werden einige Beispiele berechnet.

Bei der Untersuchung gerahmter Mannigfaltigkeiten ist die Suche nach Repräsentanten der unendlichen Familien in den stabilen Homotopiegruppen der Sphären. Ein wichtiges Mittel hierzu ist die Berechnung der e- und f-Invariante. In dieser Arbeit werden diese Invarianten für komplexe Umrahmungen berechnet. Hierzu wird zunächst ein expliziter Lift der Einschränkung des J-Morphismus konstruiert. Über diesen Lift werden wiederum (U, fr)- und (U, fr)2- Mannigfaltigkeiten konstruiert um so e- bzw. f-Invariante zu berechnen. Für die Berechnung der e-Invariante kann so die Umrahmung mit der e-Invariante höchster Ordnung bestimmt werden. Für die Berechnung der f-Invariante werden einige Beispiele berechnet.

Many similarities can be found between geographical imagery and painting. Pictorial imagery can be analysed in terms of modelling. An equivalence between the plastic and pictorial languages has been found through chorematics. Le Christ Jaune by Gauguin provides the opportunity to test this transposition., L’image géographique et la peinture présentent beaucoup de similitudes. Il est possible d’analyser l’image picturale sous l’angle de la modélisation. Par l’intermédiaire de la chorématique une équivalence dans le langage plastique et pictural a été trouvée Le Christ jaune de Gauguin permet de tester cette transposition., La imagen geográfica y la pintura presentan muchas semejanzas. Es posible analizar la imagen pictórica desde el punto de vista de la modelización. Mediante la coremática se ha encontrado una equivalencia en el lenguaje plástico o pictórico. El Cristo amarillo de Gauguin permite poner a prueba dicha transposición., Germanaz Christian, Lebras Yvon. Tableaux et modèles: «vive la sintayse». In: Mappemonde, 1994/3. pp. 36-39.

Gizatullin Flächen sind algebraische affine normale Flächen über \(\bf C\) die sich durch eine bestimmte lineare Kette von Kurven vervollständigen (kompaktifizieren) lassen. Der kanonische Divisor ist der zu den 2-Formen assoziierte Divisor und heißt \(\bf Q\)-trivial, falls es eine natürliche Zahl \(\it n\) mit \(\textit {n\(\cdot\) \(K_{x}\sim0\)}\) gibt. Es wird unter Verwendung von gewichteten dualen Graphen bewiesen, dass jede Gizatullin Fläche \(\it X\) mit einem \(\bf Q\)-trivialem kanonischen Divisor eine effektive \(\bf C\)*-Wirkung zulässt. Aufgrund dieser lassen sich dann derartige Flächen mit Hilfe der sogenannten DPD-Darstellung präzise beschreiben. Im nicht-torischen Fall kann man schließlich ein Theorem von Flenner, Kaliman und Zaidenberg verwenden um zu zeigen, dass \(\it X\) äquivariant isomorph ist zu einer lokalen abgeschlossenen Untermenge eines projektiven gewichteten 3-dimensionalen Raumes \(\bf P\), die durch eine Gleichung der Form \(\it xy-Q(z,s)=0\) gegeben wird, wobei \(\textit {x, y, z, s}\) die Variablen von \(\bf P\) sind.

Existen evidencias de la correlación interespecífica de los parámetros poblacionales en peces. Es así, que se encuentran relaciones entre los parámetros de crecimiento del modelo de von Bertalanffy, mortalidad natural, edad y longitud de madurez. Estas relaciones han servido como herramientas prácticas para caracterizar la dinámica y la historia de vida de una población poco estudiada o estimar parámetros de vida que en otros casos son muy difíciles de obtener (e.g., mortalidad natural). Debido a que el valor de la razón entre la longitud de madurez y la longitud asintótica en peces (Lm/L∞ = 0,66) propuesto por Jensen no ha sido probado para peces de la costa de Chile, se evaluó el valor de esta constancia o invariante, entendiéndose como una característica que no cambia en la historia de vida de los animales. Se estimó el tamaño del efecto medio (invariante) y su homogeneidad, además de las variables que pueden estar moderando el tamaño del efecto. Con el fin de responder a las preguntas se realizó un meta-análisis de la constancia Lm/L∞ =0,66, se recopiló 148 valores de la invariante correspondiente a 10 familias de peces. Se encontraron diferencias significativas en estos parámetros entre especies de peces, por lo que los análisis se realizaron agrupando a nivel de familia. El valor de la media ponderado con el modelo de efectos aleatorios fue de 0,61. Cinco familias contienen el valor 0,66 siendo estas Merlucciidae, Nototheniidae, Ophidiidae, Scombridae y Trachichthyidae. La media de la familia Bramidae es de 0,69 y Carangidae, Clupeidae y Engraulidae fue de 0,46; 0,56 y 0,51, respectivamente, por debajo del valor de la invariante 0,66. Finalmente, se desprende que el valor teórico Lm / L∞ =0,66 propuesto por Jensen no es generalizable para todas las especies de peces comerciales del Pacífico sudeste.

Nosotros conocemos que dos clases homoclínicas diferentes contenidas en un conjunto hiperbólico son disjuntas. Además un conjunto transitivo singular-hiperbólico con orbitas periódicas densas y una única singularidad es transitivo o es unión de dos clases homoclínicas diferentes. De estos resultados se puede preguntar si dos clases homoclínicas diferentes contenidas en un conjunto singular hiperbólico son disjuntas o si la segunda alternativa no puede ocurrir. Aquí se da una respuesta negativa a la pregunta. / Abstract. We know that two different homoclinic classes contained in the hyperbolic set are disjoint. Moreover singular-hyperbolic attracting set whit dense periodic orbits and unique equilibrium is either transitive or the union of two different homoclinic classes. These results motivate the questions of if two different homoclinic classes contained in the same singular-hyperbolic set are disjoint or if second alternative in cannot. Here it give a negative the answer for both questions. Maestría

In this thesis, we introduce subsequence invariants, a new class of invariants for the specification and verification of systems. Unlike state invariants, which refer to the state variables of the system, subsequence invariants characterize the behavior of a concurrent system in terms of the occurrences of sequences of synchronization events. The first type of such invariants, pure subsequence invariants, are linear constraints over the possible numbers of such occurrences, where we allow every occurrence of a subsequence to be interleaved arbitrarily with other events. We then describe the more general class of phased subsequence invariants, in which additional restrictions can be placed on the events that may occur between those of a given sequence. In either case, subsequence invariants are preserved when a given process is composed with additional processes. subsequence invariants can therefore be computed individually for each process and then be used to reason about the full system. We present an efficient algorithm for the computation of subsequence invariants of finite-state systems. Our construction can be applied incrementally to obtain a growing set of invariants given a growing set of event sequences. We then address the problem of proving subsequence invariants of infinite-state systems. For this we use an abstraction refinement procedure that uses small, incrementally transformed graph-based abstractions. In order to explain the techniques we use, we first introduce a simpler version of this method for statebased properties, and then show how to verify subsequence invariants. Inhalt dieser Arbeit sind Subsequenzinvarianten, eine neue Klasse von Invarianten für die Systemspezifikation und -verifikation. Im Gegensatz zu zustandsbasierten Invarianten, die über den Zustandsvariablen des Systems definiert sind, beschreiben Subsequenzinvarianten das gewünschte Systemverhalten anhand des Auftretens verschiedener Synchronisationsfolgen. Wir beschreiben zunächst reine Subsequenzinvarianten, welche durch lineare Gleichungen auf den möglichen Häufigkeiten solcher Folgen von Events gegeben sind, zwischen denen jeweils beliebige andere Events autreten dürfen. Im Anschluss verallgemeinern wir diese zu Subsequenzinvarianten mit Phasen, in denen eine Synchronisationsfolge neben der eigentlichen Folge von Events auch durch Beschränkungen auf den dazwischen auftretenden Events gegeben sein kann. Beide Klassen von Invarianten bleiben gültig, wenn ein Prozess, für den sie gelten, mit beliebigen anderen Prozessen kombiniert wird. Sie können daher für jeden einzelnen Prozess berechnet und dann zur Verifikation des gesamten Systems verwendet werden. Wir präsentieren einen effizienten Algorithmus für die Berechnung von Subsequenzinvarianten auf Systemen mit endlichen Zustandsräumen. Diese Konstruktion kann auch inkrementell angewandt werden, wenn die Menge der betrachteten Subsequenzen allmählich wächst. Für die Berechnung von Subsequenzinvarianten für Systeme mit unendlichem Zustandsraum führen wir eine Methode ein, die auf dem Prinzip der Abstraktionsverfeinerung basiert. Unsere Version dieses Ansatzes zeichnet sich durch die Verwendung sehr kleiner, graphenbasierter Abstraktionen aus. Wir präsentieren zunächst eine einfachere Variante des Verfahrens für zustandsbasierte Fehlerbedingungen, an der sich die verwendeten Operationen leichter demonstrieren lassen, und beschreiben dann die Anpassungen für die Verifikation von Subsequenzinvarianten.

Im Zentrum dieser Arbeit steht die Operation der Gruppe Gamma:=SL_n(Z[1/m]) auf dem symmetrischen Raum M:=SL_n(R)/SO(n). Allgemeiner betrachten wir die Operation rho:Gamma->Isom(M) einer S-arithmetischen algebraischen Gruppe durch Isometrien auf dem zugehörigen symmetrischen Raum M. Die symmetrischen Räume sind Riemannsche Mannigfaltigkeiten mit nichtpositiver Krümmung und daher insbesondere CAT(0)-Räume. R. Bieri und R. Geoghegan haben für die Operation rho:G->Isom(M) einer abstrakten Gruppe G auf einem CAT(0)-Raum M die geometrischen Invarianten Sigma^k(rho) als Teilmenge des Randes von M eingeführt (vgl. [Robert Bieri and Ross Geoghegan, Connectivity properties of group actions on non-positively curved spaces, vol. 161, Memoirs of the AMS, no. 765, American Mathematical Society, 2003]). Die Fokusierung, die durch die geometrischen Invarianten erreicht wird, hat sich in vielen Fällen bewährt, in denen eine Operation durch Translationen auf dem euklidischen Raum zur Verfügung steht. Über die Invarianten von anderen CAT(0)-Operationen ist noch wenig bekannt. In der vorliegenden Arbeit berechnen wir nun die geometrischen Invarianten Sigma^k(rho) für die oben erwähnte Operation rho der S-arithmetischen Gruppe Gamma auf dem zugehörigen symmetrischen Raum M. Wir erhalten für die Gruppe SL_n(Z[1/m]) die folgende Invariante: Sigma^k(rho) ist der ganze Rand von M, falls k kleiner als s(n-1) ist; Sigma^k(rho) ist die Menge aller Randpunkte e von M, die nicht im Rand eines rational definierten flachen Unterraum von M liegen, falls k größer oder gleich s(n-1) ist. Hierbei ist s die Anzahl der verschiedenen Primteiler von m. Die obigen Resultate sind eine Verallgemeinerung derer in [Robert Bieri and Ross Geoghegan, Controlled Connectivity of SL_2(Z[1/m]), Geometriae Dedicata 99 (2003), 137--166]. Der Beweis, den wir geben, besteht aus einer Vereinfachung des Beweises von Bieri und Geoghegan, die dann auf die allgemeinere Situation angepasst werden konnte. Ein interessanter Aspekt ergibt sich, wenn wir für eine Operation rho auf M die Zahlen k betrachten, für die gilt: (*) Sigma^k(rho) ist der ganze Rand von M. Operiert die Gruppe Gamma mit diskreten Bahnen, dann ist (*) äquivalent zur Eigenschaft, daß die Punktstabilisatoren Gamma_a, für a aus M, vom Typ F_k sind. Die Eigenschaft (*) ist auch von Interesse für S-arithmetische Untergruppen einer linearen algebraischen Gruppe über einem Funktionenkörper. Wir zeigen, daß es hier eine naheliegende Operation rho' auf einem Bruhat-Tits Gebäude M' gibt, so daß Gamma' ein Punktstabilisator und damit die Eigenschaft (*) mit der Eigenschaft "Gamma' ist vom Typ F_k" zusammenfällt. Im Zahlkörperfall sind die Verhältnisse ganz anders. Unsere S-arithmetischen Gruppen operieren auf dem symmetrischen Raum M nicht mit diskreten Bahnen und sind durchwegs vom Typ F_k für alle k. Dagegen erlaubt unser Hauptresultat die Bestimmung der Zahlen k mit der Eigenschaft (*) und zeigt eine interessante Abhängigkeit von s=|S| und dem Rang r der algebraischen Gruppen (rho erfüllt (*) kIsom(M) of an S-arithmetic algebraic group Gamma by isometries on the respective symmetric space M. Symmetric spaces are non positively curved Riemannian manifolds. In particular, they are CAT(0)spaces. In [Robert Bieri and Ross Geoghegan, Connectivity properties of group actions on non-positively curved spaces, vol. 161, Memoirs of the AMS, no. 765, American Mathematical Society, 2003] the geometric invariants Sigma^k(rho) are introduced. These are subsets of the boundary of M associated to the action rho:G->Isom(M) of an abstract group G on a CAT(0) space M. Focusing on the geometric invariants has proved very useful, particularly in examples, where the group acts by translations on some euklidian space M. But the invariants of other CAT(0) actions are still relatively unknown. In the present paper we study the action of an S-arithmetic group on its symmetric space, as mentioned above. With s for the total number of different prime divisors of some non zero integer m, we get the following result on the group SL_n(Z[1/m]): If k=s(n-1) holds, then Sigma^k(rho) is the set of all boundary points, which are not in the boundary of any rationally defined flat subspace of M. This is a generalisation of [R. Bieri and R. Geoghegan, Controlled connectivity of SL_2(Z[1/m]), Geometriae Dedicata 99 (2003), 137--166]. The results are proved by a simplification of their proof, which could be adapted to this more general setup. Given some integer k, it is interesting to observe the following property of a group action rho: (*) Sigma^k(rho) is the whole boundary of M. If the action of Gamma on M has discrete orbits, then we have (*) equivalent to the property "Gamma_x is of type F_k", for the stabilizer Gamma_x of some point x of M. This property is also intersting in the following case: Let Gamma' be an S-arithmetic subgroup of a linear algebraic group over a number field. We show that there is an obvious action rho' of Gamma' on some Bruhat-Tits building M', with Gamma' the stabilizer of some point of M'. Thus, here (*) is equivalent to "Gamma' is of type F_k". In the number field case, we have a totally different situtauion. There the S-arithmetic groups do not have discrete orbits in the symmetric space M and they are of type F_k for all k. Nevertheless we can apply our main result to this situation to determine for which k the property (*) holds. We observe again an interesting dependence on s=|S| and the rank of the group r (namely (*) holds k

Program verification increases the degree of confidence that a program will perform correctly. Manual verification is an error-prone and tedious task. Its automation is highly desirable. The verification methodology reduces the reasoning about temporal properties of program computations to testing the validity of implication between auxiliary first-order assertions. The synthesis of such auxiliary assertions is the main challenge for automated tools. There already exist successful tools for the verification of safety properties. These properties require that some "bad'; states never appear during program computations. The tools construct invariants, which are auxiliary assertions for safety. Invariants are computed symbolically by applying techniques of abstract interpretation. Liveness properties require that some "good'; states will eventually appear in every computation. The synthesis of auxiliary assertions for the verification of liveness properties is the next challenge for automated verification tools. This dissertation argues that transition invariants can provide a new basis for the development of automated methods for the verification of liveness properties. We support this thesis as follows. We introduce a new notion of auxiliary assertions called transition invariant. We apply this notion to propose a proof rule for the verification of liveness properties. We provide a viable approach for the automated synthesis of transition invariants by abstract interpretation, which automates the proof rule. For this purpose, we introduce a transition predicate abstraction. This abstraction does not have an inherent limitation to preserve only safety properties. Most liveness properties of concurrent programs only hold under certain assumptions on non-deterministic choices made during program executions. These assumptions are known as fairness requirements. A direct treatment of fairness requirements in a proof rule is desirable. We specialize our proof rule for the direct accounting of two common ways of specifying fairness. Fairness requirements can be imposed either on program transitions or on sets of programs states. We treat both cases via abstract-transition programs and labeled transition invariants respectively. We have developed a basis for the construction of automated tools that can not only prove that a program never does anything bad, but can also prove that the program eventually does something good. Such proofs increase our confidence that the program will perform correctly. Programmverifikation stärkt unsere Überzeugung darin, dass ein Programm korrekt funktionieren wird. Manuelle Verifikation ist fehleranfällig und mühsam. Deren Automatisierung ist daher sehr erwünscht. Die allgemeine Vorgehensweise bei der Verifikation besteht darin, die temporale Argumentation über die Programmberechnungen auf die Überprüfung der Gültigkeit von Implikation zwischen Hilfsaussagen in Prädikatenlogik zu reduzieren. Die größte Herausforderung in der Automatisierung von Verifikationsmethoden liegt in der automatischen Synthese solcher Hilfsaussagen. Es gibt bereits erfolgreiche Werkzeuge für die automatische Verifikation von Safety-Eigenschaften.Diese Eigenschaften erfordern, dass keine ';unerwünschten" Programmzustände in Berechnungen auftreten. Die Werkzeuge synthetisieren Invarianten, die Hilfsaussagen für die Verifikation von Safety-Eigenschaften darstellen. Invarianten werden symbolisch, mit Hilfe von Techniken der abstrakten Interpretation berechnet. Liveness-Eigenschaften erfordern, dass bestimmte ';gute" Zustände irgendwann in jeder Berechnung vorkommen. Die Synthese von Hilfsaussagen für die Verifikation von Liveness-Eigenschaften ist die nächste Herausforderung für automatische Werkzeuge. Diese Dissertation vertritt die Auffassung, dass Transitionsinvarianten (engl.: transition invariants) eine neu Basis für die Entwicklung automatischer Methoden für die Verifikation von Liveness-Eigenschaften bereitstellen können. Wir unterstützen diese These wie folgt. Wir führen einen neuen Typ von Hilfsaussagen ein, der als Transitionsinvariante bezeichnet wird. Wir benutzen Transitionsinvariante, um eine Beweisregel für die Verifikation von Liveness-Eigenschaften zu entwickeln.Wir stellen einen praktikablen Ansatz für die Synthese von Transitionsinvarianten basierend auf der abstrakten Interpretation vor und automatisieren dadurch die Beweisregel. Zu diesem Zweck führen wir eine Transitionsprädikaten-Abstraktion (engl.: transition predicate abstraction) ein. Diese Abstraktion ist nicht darauf beschränkt, nur Safety-Eigenschaften erhalten zu können. Die meisten Liveness-Eigenschaften nebenläufiger Programme gelten nur unter bestimmten Annahmen bzgl. der nicht-deterministischen Wahl, die bei den Programmberechnungen getroffen wird. Diese Annahmen sind als Fairness-Anforderungen bekannt und deren direkte Berücksichtigung in einer Beweisregel ist wünschenswert. Wir spezialisieren unsere Beweisregel für die direkte Behandlung von zwei verbreiteten Arten von Fairness-Spezifikationen. Zum einem berücksichtigen wir die Fairness-Anforderungen an Programmübergänge durch abstrakte Transitionsprogramme (engl.: abstract-transition programs). Zum anderen werden die durch Zustandsmengen angegebenen Fairness-Anforderungen mit Hilfe von markierten Transitionsinvarianten (engl.: labeled transition invariants) behandelt. Wir haben eine Basis für die Entwicklung automatischer Werkzeuge bereitgestellt, die beweisen können, dass ein Programm nicht schadet und dass das Programm etwas Gutes bewirkt. Solche Beweise stärken unsere Überzeugung darin, dass das Programm korrekt funktionieren wird.

Preprint, [EN] The bosonic second invariant of SuperLiouville models in supersymmetric classical mechanics is described. [ES] El segundo campo cuántico de bosones invariante del modelo SuperLiouville es descrito en la mecanica clasica supersimétrica.