Refine
Document Type
- Article (8)
- Monograph/Edited Volume (2)
- Doctoral Thesis (1)
- Master's Thesis (1)
- Other (1)
- Postprint (1)
Keywords
- Ohrid-Prespa region (2)
- Relevanz (2)
- Theorembeweisen (2)
- Unifikation (2)
- chlorophyll a (2)
- nutrients (2)
- perialpine lakes (2)
- relevance (2)
- theorem (2)
- water temperature (2)
Institute
- Institut für Informatik und Computational Science (4)
- Department Erziehungswissenschaft (2)
- Institut für Ernährungswissenschaft (2)
- Institut für Umweltwissenschaften und Geographie (2)
- Zentrum für Qualitätsentwicklung in Lehre und Studium (ZfQ) (2)
- Hasso-Plattner-Institut für Digital Engineering GmbH (1)
- Institut für Biochemie und Biologie (1)
- Institut für Geowissenschaften (1)
- Institut für Physik und Astronomie (1)
Birth weight variation is influenced by fetal and maternal genetic and non-genetic factors, and has been reproducibly associated with future cardio-metabolic health outcomes. In expanded genome-wide association analyses of own birth weight (n = 321,223) and offspring birth weight (n = 230,069 mothers), we identified 190 independent association signals (129 of which are novel). We used structural equation modeling to decompose the contributions of direct fetal and indirect maternal genetic effects, then applied Mendelian randomization to illuminate causal pathways. For example, both indirect maternal and direct fetal genetic effects drive the observational relationship between lower birth weight and higher later blood pressure: maternal blood pressure-raising alleles reduce offspring birth weight, but only direct fetal effects of these alleles, once inherited, increase later offspring blood pressure. Using maternal birth weight-lowering genotypes to proxy for an adverse intrauterine environment provided no evidence that it causally raises offspring blood pressure, indicating that the inverse birth weight-blood pressure association is attributable to genetic effects, and not to intrauterine programming.
Classical methods to analyze the surface composition of atmosphereless planetary objects from an orbiter are IR and gamma ray spectroscopy and neutron backscatter measurements. The idea to analyze surface properties with an in-situ instrument has been proposed by Johnson et al. (1998). There, it was suggested to analyze Europa's thin atmosphere with an ion and neutral gas spectrometer. Since the atmospheric components are released by sputtering of the moon's surface, they provide a link to surface composition. Here we present an improved, complementary method to analyze rocky or icy dust particles as samples of planetary objects from which they were ejected. Such particles, generated by the ambient meteoroid bombardment that erodes the surface, are naturally present on all atmosphereless moons and planets. The planetary bodies are enshrouded in clouds of ballistic dust particles, which are characteristic samples of their surfaces. In situ mass spectroscopic analysis of these dust particles impacting onto a detector of an orbiting spacecraft reveals their composition. Recent instrumental developments and tests allow the chemical characterization of ice and dust particles encountered at speeds as low as 1 km/s and an accurate reconstruction of their trajectories. Depending on the sampling altitude, a dust trajectory sensor can trace back the origin of each analyzed grain with about 10 km accuracy at the surface. Since the detection rates are of the order of thousand per orbit, a spatially resolved mapping of the surface composition can be achieved. Certain bodies (e.g., Europa) with particularly dense dust clouds, could provide impact statistics that allow for compositional mapping even on single flybys. Dust impact velocities are in general sufficiently high at orbiters about planetary objects with a radius > 1000 km and with only a thin or no atmosphere. In this work we focus on the scientific benefit of a dust spectrometer on a spacecraft orbiting Earth's Moon as well as Jupiter's Galilean satellites. This 'dust spectrometer' approach provides key chemical and isotopic constraints for varying provinces or geological formations on the surfaces, leading to better understanding of the body's geological evolution.
We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem prover and especially the functionality of the educational fragment. This currently supports working with terms of the untyped lambda calculus and addresses both undergraduate students and researchers. We show how the tool can be used to support the students' understanding of functional programming and discuss general problems related to the process of building theorem proving software that aims at supporting both research and education.
This document presents an axiom selection technique for classic first order theorem proving based on the relevance of axioms for the proof of a conjecture. It is based on unifiability of predicates and does not need statistical information like symbol frequency. The scope of the technique is the reduction of the set of axioms and the increase of the amount of provable conjectures in a given time. Since the technique generates a subset of the axiom set, it can be used as a preprocessor for automated theorem proving. This technical report describes the conception, implementation and evaluation of ARDE. The selection method, which is based on a breadth-first graph search by unifiability of predicates, is a weakened form of the connection calculus and uses specialised variants or unifiability to speed up the selection. The implementation of the concept is evaluated with comparison to the results of the world championship of theorem provers of the year 2012 (CASC J6). It is shown that both the theorem prover leanCoP which uses the connection calculus and E which uses equality reasoning, can benefit from the selection approach. Also, the evaluation shows that the concept is applyable for theorem proving problems with thousands of formulae and that the selection is independent from the calculus used by the theorem prover.
This document presents a formula selection system for classical first order theorem proving based on the relevance of formulae for the proof of a conjecture. It is based on unifiability of predicates and is also able to use a linguistic approach for the selection. The scope of the technique is the reduction of the set of formulae and the increase of the amount of provable conjectures in a given time. Since the technique generates a subset of the formula set, it can be used as a preprocessor for automated theorem proving. The document contains the conception, implementation and evaluation of both selection concepts. While the one concept generates a search graph over the negation normal forms or Skolem normal forms of the given formulae, the linguistic concept analyses the formulae and determines frequencies of lexemes and uses a tf-idf weighting algorithm to determine the relevance of the formulae. Though the concept is built for first order logic, it is not limited to it. The concept can be used for higher order and modal logik, too, with minimal adoptions. The system was also evaluated at the world championship of automated theorem provers (CADE ATP Systems Competition, CASC-24) in combination with the leanCoP theorem prover and the evaluation of the results of the CASC and the benchmarks with the problems of the CASC of the year 2012 (CASC-J6) show that the concept of the system has positive impact to the performance of automated theorem provers. Also, the benchmarks with two different theorem provers which use different calculi have shown that the selection is independent from the calculus. Moreover, the concept of TEMPLAR has shown to be competitive to some extent with the concept of SinE and even helped one of the theorem provers to solve problems that were not (or slower) solved with SinE selection in the CASC. Finally, the evaluation implies that the combination of the unification based and linguistic selection yields more improved results though no optimisation was done for the problems.
Proteins and peptides play a predominant role in biochemical reactions of living cells. In these complex environments, not only the constitution of the molecules but also their three-dimensional configuration defines their functionality. This so-called secondary structure of proteins is crucial for understanding their function in living matter. Misfolding, for example, is suspected as the cause of neurodegenerative diseases such as Alzheimer’s and Parkinson’s disease. Ultimately, it is necessary to study a single protein and its folding dynamics. Here, we report a first step in this direction, namely ultrasensitive detection and discrimination of in vitro polypeptide folding and unfolding processes using resonant plasmonic nanoantennas for surface-enhanced vibrational spectroscopy. We utilize poly-l-lysine as a model system which has been functionalized on the gold surface. By in vitro infrared spectroscopy of a single molecular monolayer at the amide I vibrations we directly monitor the reversible conformational changes between α-helix and β-sheet states induced by controlled external chemical stimuli. Our scheme in combination with advanced positioning of the peptides and proteins and more brilliant light sources is highly promising for ultrasensitive in vitro studies down to the single protein level.
The majority of cases of community-acquired pneumonia are caused by Streptococcus pneumoniae and most studies on pneumococcal host interaction are based on cell culture or animal experiments. Thus, little is known about infections in human lung tissue.
Cyclooxygenase-2 and its metabolites play an important regulatory role in lung inflammation. Therefore, we established a pneumococcal infection model on human lung tissue demonstrating mitogen-activated protein kinase (MAPK)-dependent induction of cyclooxygenase-2 and its related metabolites.
In addition to alveolar macrophages and the vascular endothelium, cyclooxygenase-2 was upregulated in alveolar type II but not type I epithelial cells, which was confirmed in lungs of patients suffering from acute pneumonia. Moreover, we demonstrated the expression profile of all four E prostanoid receptors at the mRNA level and showed functionality of the E prostanoid(4) receptor by cyclic adenosine monophosphate production. Additionally, in comparison to previous studies, cyclooxygenase-2/prostaglandin E-2 related pro- and anti-inflammatory mediator regulation was partly confirmed in human lung tissue after pneumococcal infection.
Overall, cell type-specific and MAPK-dependent cyclooxygenase-2 expression and prostaglandin E-2 formation in human lung tissue may play an important role in the early phase of pneumococcal infections.
Alles auf Anfang!
(2019)
Im Zuge der Bologna-Reform ist an Hochschulen vieles in Bewegung gekommen. Studium und Lehre sind stärker ins Blickfeld gerückt. Dabei kommt der Studieneingangsphase besondere Bedeutung zu, werden doch hier die Weichen für ein erfolgreiches Studium gestellt. Deshalb ist es verständlich, dass die Hauptanstrengungen der Hochschulen auf den Studieneingang gerichtet sind – ganz nach dem Motto: „Auf den Anfang kommt es an!“. Konsens herrscht dahingehend, dass der Studieneingang neu zu gestalten ist, doch beim „Wie?“ gibt es unterschiedliche Antworten. Zugleich wird immer deutlicher, dass eine wirksame Neugestaltung der Eingangsphase nur mit einer umfassenden Reform des Studiums gelingen kann.
Ziel des vierten Bandes der Potsdamer Beiträge zur Hochschulforschung ist es, eine Zwischenbilanz der Debatte zum Studieneingang zu ziehen. Auf der Basis empirischer Studien werden unterschiedliche Perspektiven auf den Studieneingang eingenommen und Empfehlungen zur Optimierung des Studieneingangs abgeleitet. Die zahlreichen Untersuchungsergebnisse Potsdamer Forschergruppen werden durch weitere nationale sowie internationale Perspektiven ergänzt. Der Band richtet sich an alle, die sich für die Entwicklung an Hochschulen interessieren.
Model-derived relationships between chlorophyll a (Chl-a) and nutrients and temperature have fundamental implications for understanding complex interactions among water quality measures used for lake classification, yet accuracy comparisons of different approaches are scarce. Here, we (1) compared Chl-a model performances across linear and nonlinear statistical approaches; (2) evaluated single and combined effects of nutrients, depth, and temperature as lake surface water temperature (LSWT) or altitude on Chl-a; and (3) investigated the reliability of the best water quality model across 13 lakes from perialpine and central Balkan mountain regions. Chl-a was modelled using in situ water quality data from 157 European lakes; elevation data and LSWT in situ data were complemented by remote sensing measurements. Nonlinear approaches performed better, implying complex relationships between Chl-a and the explanatory variables. Boosted regression trees, as the best performing approach, accommodated interactions among predictor variables. Chl-a-nutrient relationships were characterized by sigmoidal curves, with total phosphorus having the largest explanatory power for our study region. In comparison with LSWT, utilization of altitude, the often-used temperature surrogate, led to different influence directions but similar predictive performances. These results support utilizing altitude in models for Chl-a predictions. Compared to Chl-a observations, Chl-a predictions of the best performing approach for mountain lakes (oligotrophic-eutrophic) led to minor differences in trophic state categorizations. Our findings suggest that both models with LSWT and altitude are appropriate for water quality predictions of lakes in mountain regions and emphasize the importance of incorporating interactions among variables when facing lake management challenges.