Higher-order logic (HOL) offers a simple syntax and semantics for representing and reasoning about typed mathematical concepts. There are many state-of-the-art automated theorem provers for HOL. But the type system of HOL lacks advanced features where types may depend on terms. This is useful as many mathematical notions are inherently dependent typed. Dependent type theory offers such a rich type system but has rather substantial conceptual differences to HOL and isn’t supported as well by automated theorem provers. We introduce a dependently typed extension DHOLP of HOL that supports dependent types while retaining the style and conceptual framework of HOL. Moreover, we describe one translation from DHOLP and a second one from one of its fragments to HOL and prove the soundness and completeness of the translations. We implement both translations within the MMT system—a system for formalizing mathematics—where they are combined with a HOL prover into an automated theorem prover for DHOLP. Finally, we formalize basic set theory notions in DHOLP and outline how such a formalization can be combined with a recent translation of the language of the Mizar proof assistant to MMT to obtain an automated theorem prover for problems in the language of the Mizar proof assistant.
Weniger anzeigenPhosphate homeostasis is essential for survival in eucaryotes. It is mediated by inositol phosphates, which are synthesized by a sequence of kinases. One such kinase in humans is diphosphoinositol pentakisphosphate kinase 2 (PPIP5K2). However, the exact mechanism of phosphate homeostasis in general and PPIP5K2 specifically are still subject to research. To date knockouts and mutations are used for research, but an inhibitor for PPIP5K2 is heavily sought after. Bartsch and Fiedler, who carry out research concerning PPIP5K2, performed a high-throughput screening of 60 000 compounds revealing a single ATP-competitive inhibitor. With an IC50 of 15:5 M the affinity is comparably poor. The presented thesis aims at utilizing computer-aided drug design (CADD) methods to identify additional and ideally more potent PPIP5K2 ligands. We employed the binding mode of the lead compound to perform a pharmacophore-based virtual screening. A second approach deriving pharmacophore features from the PPIP5K2 apo structure was included to broaden the chemical space of potential active compounds further. We wrapped the pharmacophore screenings in a pipeline with additional CADD methods to evaluate the screening hits in more detail. Hits not fitting the binding pocket were discarded first. Then we used molecular docking to place the molecules in the binding pocket and filtered them based on matching the respective pharmacophore hypothesis and on the binding affinity score. Selected hits were simulated using molecular dynamics (MD) and the stability was evaluated by calculating the root-mean-square deviation (RMSD) and fluctuation (RMSF). We identified nine candidates from the lead-based screening and eight from the apo structure-based screening. All candidates conform to their respective pharmacophore, score sufficiently high and are stable in MD simulations. Proposed candidates were handed over to our collaboration partners at FMP and will be tested invitro. If confirmed active, these compounds will aid building a library of PPIP5K2 ligands to be used in research and for further virtual screening and lead optimization campaigns.
Weniger anzeigenGegen ein allgemein-abstraktes Verständnis ist der spezifisch akademische Antisemitismus zu bestimmen, der sich als Ideologie an das akademische Feld anpasst: So wird Wissenschaftsfreiheit als defensives Individualrecht und die wissenschaftliche Form beansprucht, während sich antisemitische Ressentiments und Wissenschaftsfeindlichkeit zeigen. Die Bedrohung für die Wissenschaftsfreiheit ist aus seiner irrationalen, antagonistischen und spaltenden Logik zu begreifen. Denn er geht mit Täter-Opfer-Umkehr, Leugnungen und weiteren sozialen Abwehrhandlungen einher, die Antisemitismuskritik erschweren und einen verschwörerischen ‚jüdischen‘ Feind imaginieren, der ‚Kritik‘ unterdrücke. Antisemitisch Agierende profitieren von einer organisationskulturellen Neutralität in den deutschen Universitäten, die selten Sanktionen folgen lassen – wenn sie das Problem überhaupt benennen. Denn die institutionelle Selbstregulierung und ihr Ideal der Wissenschaftsfreiheit scheitern an einem systemisch reproduzierten Antisemitismus und einer spiegelbildlichen Selbstidealisierung: Die zumeist liberalen Theorien (hier: Elif Özmen) der Wissenschaftsfreiheit gründen auf den Dualismen wissenschaftlich/ unwissenschaftlich und wissenschaftlich /ideologisch, mit der das Ideologische ausgeblendet wird. Während Özmen auf der Trias von Rechtsstaat, demokratischer Gesellschaft und akademischer Selbstregulierung vertraut, zieht sie keine Konsequenz aus ihrer Erfahrung, dass die meisten Professor:innen bei "Vorfällen“ schweigen. In ihrem Zweckrationalismus, Pragmatismus und Formalismus blendet Özmen von der real unvernünftigen Gesellschaft ab, die systemisch pathisch-projektive Bedürfnisstrukturen, entsprechende Deutungsmuster und mit Alltagsgewalt verbundene strukturelle Angstregime reproduziert. Für Jüdinnen und Juden gehören Universitäten zu jenen Regimen, da im akademischen Milieu mit dem „progressiven“ Ticket, das auf bestimmten schützenswerten, rigiden Gruppenidentitäten gründet, die Widerstandskraft gegen jede Form des Antisemitismus (insb. israelbezogen) schwindet. Indirekt können humanistische Kernmissionen der Akademie (A. Rosenfeld) und ihre Strukturprinzipien (R. K. Merton) Schlimmeres verhindern. Allerdings wäre eine kritische Theorie skeptisch, da jene humanen Missionen und Prinzipien im Antisemitismus als einer „Ontologie der Reklame“ (Adorno) verhöhnt würden. Mehr noch, die ‚Grenzen der Aufklärung‘ stecken in der Wissenschaftsfreiheit selbst: Unter der formalrechtlichen Freiheit kann sich der antisemitische Wahn in wissenschaftlichen Meinungen ‚frei‘ äußern und reproduzieren – das ist der ‚Antagonismus im freien wissenschaftlichen Meinen‘ (in Anlehnung an Adorno). Eine kritische Theorie zielt auf eine antinomische Moralkritik unter den Bedingungen des herrschenden Allgemeinen, die jede sozial und von vernünftigen Zwecken abstrahierende Ethik zur schlechten Unendlichkeit verleiten. Die formale Freiheit zur Wissenschaft bedarf mündiger Subjekte, die diese in bewusster gesellschaftlicher Negativität entfalten und Verfolgte unterstützen. Nicht zuletzt würden sie sich gegen instrumentalisierende Praxisanweisungen stellen und für den Vorrang des zu erkennenden Objekts eintreten, von dem keine unliebsamen Erscheinungen subjektiv abzuwehren sind.
Weniger anzeigenDie Masterarbeit setzt sich materialsemantischen und materialästhetischen Aspekten der Bronzetür des Bohemund-Mausoleums in Canosa di Puglia (12. Jahrhundert) auseinander. Grundlegend sind hierfür die Ergebnisse einer Restaurierung der Tür in den 2000er Jahren. Zudem untersucht die Arbeit topographische Zusammenhänge der Tür und des Mausoleums und stellt so Überlegungen zu möglichen Rezipient:innen an.
Berlín es reconocida como una de las ciudades más inclusivas y diversas de Alemania, de ahí que se considere como la capital de lo queer-trans*. Aspecto que motivó mi interés personal y académico por comprender de qué manera se inscriben las diferentes identidades en este espacio diaspórico creado en Berlín, y como esta comunidad queertrans* latinoamericana, logra configurarse en un espacio donde ser Queer hace parte de la normalidad. Desde un enfoque interseccional y de género logro profundizar en estas dinámicas y comprender los contextos en que surge la agencia de la diáspora queer y trans* latinx, en relación con su construcción identitaria y su posicionamiento en este nuevo entorno como resultado de su proceso migratorio. Utilizando una metodología cualitativa, exploré los significados otorgados a las prácticas y relaciones migratorias, así como los itinerarios y puntos de inflexión que moldean su experiencia. Se concluye que la agencia surge en contextos de constreñimiento, se caracteriza por ser adaptativa, centrándose en el cuerpo como un espacio de significado y en la interacción constante con el entorno. La creación de un espacio diaspórico, constituye igualmente, una forma de agencia colectiva que proporciona seguridad y les ayuda a enfrentar la pérdida y la expatriación. La capacidad reflexiva y la adaptación al entorno son evidentes, lo que les permite deconstruirse y recrear sus identidades a partir de la configuración de espacios seguros para expresar sus creatividades y resistencias.
Weniger anzeigenThe work illuminates various perspectives on the ontology of technical artifacts from analytical metaphysics, formal ontology, and cognitive sciences. At its core lies the question of how the functions of artifacts can be conceptualized depending on the material constitution of intentionally designed objects.
Vor dem Hintergrund, dass sich das Schulbildungssystem hin zu einem Ganztagsschulbetrieb wandelt und Lehrer*innen zunehmend zu den ersten persönlichen Ansprechpersonen für Schüler*innen zählen, kommt den Lehrkraft-Lernenden-Beziehungen eine immer größer werdende Bedeutung zu. Viele Lehrer*innen fühlen sich jedoch in Hinblick auf ihren Beratungsauftrag für Schüler*innen und deren Eltern oft überfordert und nicht gut ausgebildet und vermeiden Beratungsgespräche. Als ein wesentlicher Gelingens-Faktor bei Beratungsgesprächen wird die professionelle Haltung und eine entsprechende Selbstwirksamkeit eingeschätzt. Die Methode der Gewaltfreien Kommunikation (GFK) nach Marshall Rosenberg wird als eine Methode empfohlen, die sich besonders gut für Konfliktlösungen eignet. In dieser Arbeit wird untersucht, inwiefern sich die Anwendung der GFK-Methode auf die Haltung und das Selbstwirksamkeitserleben von beratenden Lehrer*innen bei schulischen Konflikt-und Beratungsgesprächen auswirkt. Dazu wurden vier Lehrerinnen interviewt, die von sich angaben eine Ausbildung als Beratungslehrerin absolviert zu haben und die GFK-Methode bei Konflikt- und Beratungsgesprächen anzuwenden. Die Interviewpartnerinnen berichteten, dass sich die Verwendung der GFK positiv auf die professionelle Haltung und das Selbstwirksamkeitserleben auswirkt und beschrieben eine Zunahme an Handlungsfähigkeit in Hinblick auf Konflikt- und Beratungsgespräche.
Weniger anzeigenTerahertz (THz) spectral range covers frequencies from 0.1 to 50 THz [1]. Due to its photon energy, THz radiation is a powerful tool for low-energy excitations. The excitation of spin-waves [2], phonons [3; 4], and ionization of excitons [5] are possible. Additionally, ultrafast spin dynamics can be investigated by the study of THz emission [6]. There are multiple sources to generate THz radiation. Firstly, photoconductive antennas, which are used for linear THz spectroscopy with limited bandwidth <6 THz [7; 8]. Secondly, organic crystals with a bandwidth from 1-10 THz and a major detriment of having gaps in their emission spectrum [9]. Thirdly, the lithium niobate crystal (LiNbO3) with a bandwidth of 0.1-2.5 THz creates high peak amplitudes for non-linear THz spectroscopy [10; 11]. Lastly, the spintronic terahertz emitter covers a range of 0.3-15 THz [12] and was recently improved to match its peak amplitude to the commonly used LiNbO3 [13]. With regards to detection, usually, electro-optic sampling (EOS) using a pump-probe scheme is utilized [14]. With this, a multi-shot approach is used by which the timing between the THz pump and probe is modified to measure the temporal change in the refractive index of the material, which is proportional to the THz amplitude [15]. This approach has some disadvantages. The shot-to-shot fluctuations (noise) of the multiple sampling pulses may easily exceed small signal amplitudes. Therefore, a long averaging time is necessary to obtain an acceptable signal-to-noise ratio. The single-shot EOS (SEOS) could overcome these drawbacks because it requires only one probe pulse to measure the time-resolved change in the refractive index of the material over the whole duration of the THz pulse [17]. This work showcases the successful implementation of a single-shot approach for broadband THz detection. The efficacy of this approach was ascertained through a comparison with the established multi-shot EOS (MEOS) methodology. Furthermore, to gain deeper insights into the underlying dynamics at play, theoretical modeling of the SEOS technique was also carried 3 out. Collectively, these investigations provide a comprehensive understanding of the advantages and limitations offered by the SEOS approach in THz detection.
Weniger anzeigenSprechen heißt handeln: Auf dem Hintergrund der linguistischen Pragmatik und eines dynamischen Kulturbegriffes untersucht die Arbeit, inwiefern Instagram als heutzutage von Studierenden meistbenutztes soziales Medium eingesetzt werden kann, um die kommunikativ-pragmatische Kompetenz von DaF-Lernenden zu fördern. Kern dieser Masterarbeit ist der Vorschlag kursbegleitender Projekte (Speech acts - Sprechakte, (un)höflich), die DaF-Lernenden pragmatische Aspekte wie Illokutionen und Sozialdeixis näherbringen sowie ihre alltäglichen Lebenserfahrungen zu Beispielen authentischer Kommunikation in der Fremdsprache verwandeln.
Weniger anzeigenDie vorliegende Masterarbeit untersucht Adaptionen literarischer Texte für DaF-Lerner*innen, wie sie beispielsweise von Klett, Hueber und anderen Lehrbuchverlagen herausgegeben werden. Solche Lernmaterialien eignen sich sowohl zum selbstgesteuerten Lernen als auch zum gemeinsamen Lernen in Sprachkursen. Sie haben das besondere Potential, ein eigenes Leseerlebnis in der Zielsprache zu schaffen, bei dem Lerner*innen sich als relativ selbstständige Lesende der Zielsprache erfahren, während sie gleichzeitig fast nebenbei ihre zielsprachlichen Fähigkeiten und ihr kulturelles Wissen ausbauen (s.a. Schüler/Gadow 2019: o.S.). In der vorliegenden Masterarbeit werden Kriterien für die sprachliche, literarische und didaktische Gestaltung dieser Lernmaterialien erarbeitet und anschließend auf drei exemplarisch ausgewählte Adaptionen angewendet. Der Schwerpunkt liegt dabei auf der Erarbeitung der Kriterien für die sprachliche Gestaltung.
Weniger anzeigenThe involvement of non-academic actors in research has become a key characteristic of sustainability studies. As part of this trend, modellers increasingly turn to Participatory Modelling to incorporate stakeholders' knowledge, perceptions, norms, and values in the development of formalized, shared representations of social-ecological systems. While stakeholder participation has been shown to have many advantages, its limits are not adequately discussed in the contemporary Participatory Modeling literature. In particular, there is a lack of engagement with insights from fields that have a long participatory research tradition, such as development studies. To address this gap, the thesis employs Fuzzy Cognitive Mapping (FCM), a widely employed form of PM, in a case study in Peru, aiming to map the socio-ecological drivers, impacts, and related adaptation strategies in the context of Harmful Algal Blooms involving diverse groups of local stakeholders. Subsequently, the thesis critically reflects on the participatory knowledge production process, drawing on sociology and development studies literature. By identifying and discussing the limitations of the participatory approach within this specific case study, the thesis aims to contribute to the development of best practices specific to FCM.
Weniger anzeigenGiovanni Pontano (1426–1503) was one of the most prominent poets of neo-latin erotic poetry. Focilla is a female character of his late work 'Hendecasyllables' or 'Baiae' whom he dedicated 10 poems to. This work analyses her devices of agency and power by applying a close-reading approach. Each of the ten poems is summarized, analyzed in form and style and interpreted. Following this, the poems are put in context with each other and references to other poems are investigated. Finally, a biographical perspective is taken for a critical interpretation of Focilla's character under additional aspects.
Weniger anzeigenFree logics are a family of logics that are free of any existential assumptions. This family can roughly be divided into positive, negative, neutral and supervaluational free logic whose semantics differ in the way how nondenoting terms are treated. While there has been remarkable work done concerning the definition of free first-order logic, free higher-order logic has not been addressed thoroughly so far. The purpose of this thesis is, firstly, to give a notion and definition of free higher-order logic based on simple type theory and, secondly, to propose faithful shallow semantical embeddings of free higher-order logic into classical higher order logic found on this definition. Such embeddings can then effectively be utilized to enable the application of powerful state-of-the-art higher-order interactive and automated theorem provers for the formalization and verification and also the further development of increasingly important free logical theories.
Weniger anzeigenAutomated theorem proving (ATP) has long been a significant field in computer science, aiming to develop algorithms for finding formal proofs automatically. With the advent of proof assistants in mathematical research and, more generally, formal methods, these systems will become increasingly relevant for mathematicans, too. Over the years, researchers have explored various approaches to tackle the inherent challenges of ATP, resulting in two paradigms being heavily researched currently: Satisfiability Modulo Theories (SMT) solving and Machine Learning (ML)....
Weniger anzeigenBased on ethnographic research, this thesis analyses the lives of women living with complex forms of trauma and their experiences of the feeling-facilitating practices of Trauma Center Trauma-Sensitive Yoga (TCTSY) in Berlin. Positioning the research in psychological anthropology, the author investigates affected and marginalized perspectives by firstly, asking what women living with trauma experience in TCTSY settings, and how their actions of feeling and making choices are initiated and sustained. Secondly, by scrutinising the question of what can be learned from TCTSY and participants’ experiences regarding their everyday life with trauma more generally. The thesis enquires into healing practices and expert discourses and zeroes in on questions such as how far an ethnographic analysis of TCTSY can influence or alter dominant understandings of trauma and trauma healing. The author argues for an understanding of trauma which is more rooted in the experiences of trauma survivors and proposes the approach of “trauma-as-ongoing-lived-experience-in-context”. Moreover, the detailed analysis of the TCTSY practice and spatial emplacement as fluid and dynamic affective arrangement that considers socialities, affects, subjectivities, spaces and the arrangement of objects and feelings within them, gives indications of what healing and empowering contexts can look like in the wake of (complex) trauma.
Weniger anzeigen