Filtern
Erscheinungsjahr
Dokumenttyp
- Dissertation (249)
- Masterarbeit (93)
- Ausgabe (Heft) zu einer Zeitschrift (84)
- Bachelorarbeit (45)
- Diplomarbeit (27)
- Wissenschaftlicher Artikel (22)
- Studienarbeit (11)
- Konferenzveröffentlichung (10)
- Habilitation (4)
- Sonstiges (2)
- Buch (Monographie) (1)
- Preprint (1)
Sprache
- Englisch (549) (entfernen)
Schlagworte
- Pestizid (8)
- Pflanzenschutzmittel (6)
- Software Engineering (6)
- Internet of Things (5)
- Biodiversität (4)
- Bluetooth (4)
- Bodenchemie (4)
- Landwirtschaft (4)
- Semantic Web (4)
- ecotoxicology (4)
Institut
- Fachbereich 4 (116)
- Institut für Informatik (85)
- Fachbereich 7 (78)
- Institut für Wirtschafts- und Verwaltungsinformatik (53)
- Institut für Computervisualistik (52)
- Institute for Web Science and Technologies (50)
- Institut für Management (30)
- Institut für Integrierte Naturwissenschaften, Abt. Biologie (24)
- Institut für Umweltwissenschaften (23)
- Fachbereich 8 (20)
In the new epoch of Anthropocene, global freshwater resources are experiencing extensive degradation from a multitude of stressors. Consequently, freshwater ecosystems are threatened by a considerable loss of biodiversity as well as substantial decrease in adequate and secured freshwater supply for human usage, not only on local scales, but also on regional to global scales. Large scale assessments of human and ecological impacts of freshwater degradation enable an integrated freshwater management as well as complement small scale approaches. Geographic information systems (GIS) and spatial statistics (SS) have shown considerable potential in ecological and ecotoxicological research to quantify stressor impacts on humans and ecological entitles, and disentangle the relationships between drivers and ecological entities on large scales through an integrated spatial-ecological approach. However, integration of GIS and SS with ecological and ecotoxicological models are scarce and hence the large scale spatial picture of the extent and magnitude of freshwater stressors as well as their human and ecological impacts is still opaque. This Ph.D. thesis contributes novel GIS and SS tools as well as adapts and advances available spatial models and integrates them with ecological models to enable large scale human and ecological impacts identification from freshwater degradation. The main aim was to identify and quantify the effects of stressors, i.e climate change and trace metals, on the freshwater assemblage structure and trait composition, and human health, respectively, on large scales, i.e. European and Asian freshwater networks. The thesis starts with an introduction to the conceptual framework and objectives (chapter 1). It proceeds with outlining two novel open-source algorithms for quantification of the magnitude and effects of catchment scale stressors (chapter 2). The algorithms, i.e. jointly called ATRIC, automatically select an accumulation threshold for stream network extraction from digital elevation models (DEM) by assuring the highest concordance between DEM-derived and traditionally mapped stream networks. Moreover, they delineate catchments and upstream riparian corridors for given stream sampling points after snapping them to the DEM-derived stream network. ATRIC showed similar or better performance than the available comparable algorithms, and is capable of processing large scale datasets. It enables an integrated and transboundary management of freshwater resources by quantifying the magnitude of effects of catchment scale stressors. Spatially shifting temporal points (SSTP), outlined in chapter 3, estimates pooled within-time series (PTS) variograms by spatializing temporal data points and shifting them. Data were pooled by ensuring consistency of spatial structure and temporal stationarity within a time series, while pooling sufficient number of data points and increasing data density for a reliable variogram estimation. SSTP estimated PTS variograms showed higher precision than the available method. The method enables regional scale stressors quantification by filling spatial data gaps integrating temporal information in data scarce regions. In chapter 4, responses of the assumed climate-associated traits from six grouping features to 35 bioclimatic indices for five insect orders were compared, their potential for changing distribution pattern under future climate change was evaluated and the most influential climatic aspects were identified (chapter 4). Traits of temperature preference grouping feature and the insect order Ephemeroptera exhibited the strongest response to climate as well as the highest potential for changing distribution pattern, while seasonal radiation and moisture were the most influential climatic aspects that may drive a change in insect distribution pattern. The results contribute to the trait based freshwater monitoring and change prediction. In chapter 5, the concentrations of 10 trace metals in the drinking water sources were predicted and were compared with guideline values. In more than 53% of the total area of Pakistan, inhabited by more than 74 million people, the drinking water was predicted to be at risk from multiple trace metal contamination. The results inform freshwater management by identifying potential hot spots. The last chapter (6) synthesizes the results and provides a comprehensive discussion on the four studies and on their relevance for freshwater resources conservation and management.
In scientific data visualization huge amounts of data are generated, which implies the task of analyzing these in an efficient way. This includes the reliable detection of important parts and a low expenditure of time and effort. This is especially important for the big-sized seismic volume datasets, that are required for the exploration of oil and gas deposits. Since the generated data is complex and a manual analysis is very time-intensive, a semi-automatic approach could on one hand reduce the time required for the analysis and on the other hand offer more flexibility, than a fully automatic approach.
This master's thesis introduces an algorithm, which is capable of locating regions of interest in seismic volume data automatically by detecting anomalies in local histograms. Furthermore the results are visualized and a variety of tools for the exploration and interpretation of the detected regions are developed. The approach is evaluated by experiments with synthetic data and in interviews with domain experts on the basis of real-world data. Conclusively further improvements to integrate the algorithm into the seismic interpretation workflow are suggested.
In dieser Dissertation wird eine Verfahrensweise für die formale Spezifikation und Verifikation von Benutzerschnittstellen unter Sicherheitsaspekten vorgestellt. Mit dieser Verfahrensweise können beweisbar sichere Benutzerschnittstellen realisiert werden. Die Arbeit besteht aus drei Teilen. Im ersten Teil wird eine Methodologie für die formale Beschreibung von Mensch-Maschine-Interaktion entwickelt. Im zweiten Teil werden gängige Computersicherheitskonzepte für die Mensch-Maschine-Interaktion angepasst und mit den im ersten Teil entwickelten Methoden formalisiert. Dabei wird ein generisches formales Modell von Mensch-Maschine-Interaktion erstellt. Im dritten Teil wird die Methodologie, die in den ersten beiden Teilen entwickelt wurde, an einem sicheren Email-Client als exemplarischen Anwendungsprogramm demonstriert.
Introduction:
In March 2012 a secessionist-Islamist insurgency gained momentum in Mali and quickly took control of two-thirds of the state territory. Within weeks radical Islamists, drug smugglers and rebels suddenly ruled over a territory bigger than Germany. News of the abuse of the population and the introduction of harsh Sharia law spread soon, and word got out that the Malian Army had simply abandoned the land. The general echo of the IC was surprise, a reaction that was, as this research will show, as unfunded as it was unconstructive*. When Malian state structures collapsed, the world watched in shock, even though the developments couldhave been anticipated –and prevented. Ultimately, the situation had to be resolved by international forces (most notably French troops), who are still in Mali at the time of writing (Arieff 2013a: 5; Lohmann 2012: 3; Walther and Christopoulos 2015: 514f.; Shaw 2013: 204; Qantara, Interview, 2012;L’Express, Mali, 2015; Deutscher Bundestag, MINUSMA und EUTM Mali, 2016; UN, MUNISMA, 2016; Boeke and Schuurmann 2015: 801; Chivvis 2016: 93f.).
This research will show that the developments in Mali in 2012 have been developing for a long time and could have been avoided. In doing so, it will also show why state security can never be analyzed or consolidated in an isolated manner. Instead, it is necessary to take into account regional dynamics and developments in order to find a comprehensive approach to security in individual states. Once state failure occurs, not only does the state itself fail, but the surrounding region equally failed to prevent the failure.
Weak states are a growing concern in many world regions, particularly in Africa. As international intervention often proves unsustainable for various reasons*, the author believes that states which cannot stabilize themselves need a regional agent to support them. This regional agent should be a Regional Security Complex (RSC) asdefined by Barry Buzan and Ole Waever (Buzan and Waever 2003). As the following analysis will show, Mali is a case in point. The hope is that this study will help avoid similar failures in the future by making a strong case for the establishment of RSC’s.
…
Die aus nachwachsenden Rohstoffen hergestellten biologisch abbaubaren Polymere Polymilchsäure (polylactic acid, PLA) und Polyhydroxybuttersäure (polyhydroxybutyrate, PHB) wurden im Rahmen dieser Arbeit mit hydrierten amorphen Kohlenstoffschichten (amorphous hydrogenated carbon, a-C:H) bei unterschiedlichen Winkeleinstellungen mit verschiedenen Dicken beschichtet. Ähnlich wie herkömmliche Polymere haben Biopolymere oft ungeeignete Oberflächeneigenschaften für industrielle Zwecke, z.B. eine geringe Härte. Für manche Anwendungen ist es daher notwendig und vorteilhaft, die Oberflächeneigenschaften von Biopolymeren unter Beibehaltung der Haupteigenschaften des Trägermaterials zu modifizieren. Eine geeignete Oberflächenmodifikation ist das Aufbringen von dünnen a-C:H Schichten. Ihre Eigenschaften hängen wesentlich vom sp²- und sp³-Hybridisierungsverhältnis der Kohlenstoffatome und dem Gehalt an Wasserstoffatomen ab. Das sp²/sp³-Verhältnis sollte in der vorliegenden Arbeit durch Variation der Beschichtungsgeometrie gesteuert werden. Da Beschichtungen bei 0°, direkt vor der Plasmaquelle, einen höheren Anteil an sp³ und indirekt (180°) beschichtete ein höheren Anteil an sp² aufweisen, wird in dieser Arbeit gezeigt, dass es möglich ist, das sp²/sp³ -Verhältnis zu kontrollieren. Dazu werden die einzelnen Proben in den Winkeln 0, 30, 60, 90, 120, 150 und 180° vor der Plasmaquelle platziert und mit einer Dauer von 2.5, 5.0, 7.5 und 10.0 Minuten beschichtet. Für den Winkeln 0° ergaben sich die Schichtdicken von 25, 50, 75 und 100 nm. Die a-C:H Schichten wurden alle mit Radiofrequenzplasma-unterstützter chemischer Gasphasenabscheidung und Acetylen als C und H Quelle abgeschieden, nachdem sie 10 Minuten lang mit einem Sauerstoffplasma vorbehandelt worden waren. Nach dieser O₂-Behandlung und der a-C:H Abscheidung werden die Oberflächen mit makroskopischen und mikroskopischen Messmethoden untersucht und die Daten anschließend analysiert. Die Oberflächenmorphologie wird mit Hilfe der Rasterelektronenmikroskopie und der Rasterkraftmikroskopie erfasst. Auf diese Weise können auch Informationen über die Stabilität der Schicht und die Oberflächenrauhigkeit gesammelt werden. Mit Kontaktwinkelmessungen (contact angle, CA) wird nicht nur die Benetzbarkeit, sondern auch die Kontaktwinkelhysterese durch Auf- und Abpumpen des Tropfenvolumens bestimmt. Durch Messung des CA von verschiedenen Flüssigkeiten und deren Vergleich werden die freie Oberflächenenergie (surface free energy, SFE) und ihre polaren und dispersiven Bestandteile bestimmt. Die Veränderungen der Barriereeigenschaften werden durch Wasserdampftransmissionstests (water vapor transmission rate, WVTR) überprüft. Die chemische Analyse der Oberfläche erfolgt zum einen durch Fourier-Transformations-Infrarotspektroskopie mit spiegelnder Reflexion und zum anderen durch Synchrotron unterstützte Techniken wie der Nahkanten-Röntgenabsorptionsfeinstruktur und der Röntgen-Photoelektronenspektroskopie. Bei der Analyse der Oberflächen nach der O₂ Behandlung, von der zunächst angenommen wurde, dass sie nur der Reinigung und Aktivierung der Oberfläche für die a-C:H Beschichtung dient, wurde festgestellt, dass die Veränderungen drastischer sind als ursprünglich angenommen. Wird PLA zum Beispiel bei 0° für 10 Minuten behandelt, steigt die Rauheit um das Fünffache. Mit zunehmendem Winkel verringert sich diese wieder, bis sie bei 180° wieder dem Ausgangswert entspricht. Bei PHB hingegen wird durchgehend ein ähnlicher Wert gemessen. Für beide Polymere lässt sich zeigen, dass der polare Anteil der SFE zunimmt. In der WVTR ist bei PLA eine Abnahme der Permeabilität und bei PHB ein Anstieg des Ausgangswertes zu beobachten. Die chemische Oberflächenanalyse zeigt, dass die O₂ Behandlung kaum Auswirkungen auf die Oberflächenbindungen hat. Insgesamt kann in dieser Arbeit gezeigt werden, dass sich die O₂ Behandlung auf die Eigenschaften der Oberfläche auswirkt und nicht ausschließlich als Reinigungs- und Aktivierungsprozess betrachtet werden kann. Bei direkter a-C:H Beschichtung (bei 0°) ist sowohl bei PLA als auch bei PHB ein Schichtversagen bei 10.0 Minuten aufgrund von Eigenspannung zu beobachten. Dies ist bei PHB in geringerem Maße auch bei 30° zu erkennen. Die Durchlässigkeit der Polymere wird bei einer fünf minütigen Beschichtung um 47% reduziert und auch die Schicht bei 10.0 Minuten führt diesen Effekt trotz auftretender Risse weiter. Die Aufbringung von a-C:H Schichten zeigt für beide Polymertypen bei direkter Beschichtung eine Dominanz von sp³-Bindungen. Mit zunehmendem Winkel nimmt diese ab und bei indirekten Beschichtungen werden sp²-Bindungen dominierend. Dieses Ergebnis ist für alle Schichtdicken ähnlich, nur der Winkel, bei dem der Wechsel der dominanten Bindung stattfindet, ist unterschiedlich. Es wird gezeigt, dass es möglich ist, die Oberflächeneigenschaften durch eine winkelabhängige Beschichtung zu steuern und somit das Verhältnis sp²/sp³ zu kontrollieren.
Studies have shown that runoff and spray-drift are important sources of nonpoint-source pesticide pollution of surface waters. Owing to this, public concern over the presence of pesticides in surface and ground water has resulted in intensive scientific efforts to find economical, yet environmentally sound solutions to the problem. The primary objective of this research was to assess the effectiveness of vegetated aquatic systems in providing buffering between natural aquatic ecosystems and agricultural landscape following insecticide associated runoff and spray-drift events. The first set of studies were implemented using vegetated agricultural ditches, one in Mississippi, USA, using pyrethroids (bifenthrin, lambda-cyhalothrin) under simulated runoff conditions and the other in the Western Cape, South Africa using the organophosphate insecticide, azinphos-methyl (AZP), under natural runoff and spray-drift conditions. The second set of studies were implemented using constructed wetlands, one in the Western Cape using AZP under natural spray-drift conditions and the other in Mississippi, USA using the organophosphate MeP under simulated runoff conditions. Results from the Mississippi-ditch study indicated that ditch lengths of less than 300 m would be sufficient to mitigate bifenthrin and lambda-cyhalothrin. In addition, data from mass balance calculations determined that the ditch plants were the major sink (generally > 90%) and/or sorption site for the rapid dissipation of the above pyrethroids from the water column. Similarly, results from the ditch study in South Africa showed that a 180 m vegetated system was effective in mitigating AZP after natural spray drift and low flow runoff events. Analytical results from the first wetland study show that the vegetated wetland was more effective than the non-vegetated wetland in reducing loadings of MeP. Mass balance calculations indicated approximately 90% of MeP mass was associated with the plant compartment. Ninety-six hours after the contamination, a significant negative acute effect of contamination on abundances was found in 8 out of the 15 macroinvertebrate species in both wetland systems. Even with these toxic effects, the overall reaction of macroinvertebrates clearly demonstrated that the impact of MeP in the vegetated wetland was considerably lower than in the non-vegetated wetland. Results from the constructed wetland study in South Africa revealed that concentrations of AZP at the inlet of the 134 m wetland system were reduced by 90% at the outlet. Overall, results from all of the studies in this thesis indicate that the presence of the plant compartment was essential for the effective mitigation of insecticide contamination introduced after both simulated and natural runoff or spray-drift events. Finally, both the vegetated agricultural drainage ditch and vegetated constructed wetland systems studied would be effective in mitigating pesticide loadings introduced from either runoff or spray-drift, in turn lowering or eliminating potential pesticide associated toxic effects in receiving aquatic ecosystems. Data produced in this research provide important information to reduce insecticide risk in exposure assessment scenarios. It should be noted that incorporating these types of best management practices (BMPs) will decrease the risk of acute toxicity, but chronic exposure may still be an apparent overall risk.
Bei einigen Arzneimittel (z.B. Antibiotika, Kontrastmittel, Betablocker) wird ein Teil des Wirkstoffs unmetabolisiert ausgeschieden und gelangt so über das Abwasser in kommunale Kläranlagen. Studien haben gezeigt, dass viele dieser Wirkstoffe durch eine konventionelle Abwasserbehandlung nicht effektiv abgebaut werden und somit in Oberflächengewässern nachweisbar sind. Eines der effektivsten Verfahren zur Entfernung organischer Mikroverunreinigungen und Mikroorganismen ist die Umkehrosmose. Ein bedeutender Nachteil dieses Verfahrens ist die Entsorgung der anfallenden Konzentrate, die erhöhte Konzentrationen von Mikroverunreinigungen und Mikroorganismen enthalten können. Dabei ist nicht auszuschließen, dass eine direkte Einleitung dieser Konzentrate das Ökosystem eines Gewässers schädigt. Um dieses Risiko zu minimieren, wäre eine gesonderte Behandlung des Konzentrats vor der Einleitung sinnvoll. In der hier vorliegenden Arbeit wurde die Ozonung als mögliches Oxidationsverfahren untersucht. Die untersuchten Konzentratproben stammen aus einer Kläranlage, in der der Ablauf nach Umkehrosmosebehandlung in das Grundwasser infiltriert wird. Durch die Untersuchungen konnte gezeigt werden, dass durch die angewendeten Ozondosen die ausgewählten Arzneistoffe weitgehend oxidiert wurden, obwohl das Umkehrosmosekonzentrat einen sehr hohen TOC "Gehaltes von bis zu 46 mg/L aufwies. Zur Vorbeugung von Membranfouling wird Membrananlagenzuläufen, in diesem Fall dem Kläranlagenablauf, häufig Chlor zugesetzt. Eine Vergleichsstudie mit vorchlorierten und nicht vorchlorierten Kläranlagenabläufen zeigte einen Anstieg der Ozonstabilität nach der Chlorierung. Daraus resultierte aber auch eine Abnahme an OH-Radikalen. Die höhere Ozonstabilität könnte dazu führen, dass über eine direkte Ozonreaktion die Oxidation von Stoffen mit einer höheren Geschwindigkeitskonstante zweiter Ordnung bevorzugt würde. Der Abbau der Stoffe, die hauptsächlich über OH-Radikale oxidiert werden, würde dann gleichzeitig herabgesetzt. Für die Wirkstoffgruppe der Betablocker, die permanent in Kläranlagenabläufen nachweisbar ist, wurden die Geschwindigkeitskonstanten mit Ozon- sowie OH-Radikalen ermittelt. Untersucht wurden Acebutolol, Atenolol, Metoprolol und Propranolol. Betablocker enthalten zwei funktionelle Gruppen, die reaktiv gegenüber Ozon sind, zum einen ein sekundäres Amin und zum anderen einen aktivierten aromatischen Ring. Die Amingruppe ist dafür verantwortlich, dass die Geschwindigkeit der Ozonreaktion pH-Wert abhängig ist, da nur das deprotonierte Amin schnell mit Ozon reagieren kann. Die Geschwindigkeitskonstante für die Reaktion von Acebutolol, Atenolol and Metoprolol mit Ozon liegt bei etwa 2000 M-1 s-1, wo hingegen Propranolol mit ~1.0 105 M-1 s-1 etwa zwei Größenordnungen schneller reagiert. Die Konstanten für die Reaktionen mit OH-Radikalen liegen bei 0.5-1.0 × 1010 M-1 s-1. Die während der Ozonreaktion von Metoprolol und Propranolol gebildeten Oxidationsprodukte (OPs) wurden über HPLC-Tandem-MS identifiziert. Die Ozonreaktionen führten zur Bildung 23 OPs im Fall des Metoprolols und etwa 30 OPs beim Propranolol. Um die Auswirkung des pH-Wertes sowie der OH-Radikalreaktion auf die OP-Bildung zu untersuchen, wurden die Experimente bei pH 3 und 8, sowie mit und ohne Zugabe des Radikalfängers tert-Butanol durchgeführt. Die Menge der gebildeten OH-Radikale wurde durch den Zusatz von para-Chlorbenzoesäure ermittelt. Metoprolol: Der Einfluss des protonierten und des nicht protonierten Metoprolols auf die Menge der gebildeten OH-Radikale wurde über einen Vergleich der gemessenen para-Chlorbenzoesäureabnahme mit modellierten Werten ermittelt (Model: Acuchem). Es lassen sich dabei bessere Übereinstimmungen erzielen, wenn die Modelannahmen bei der primären Ozonreaktion des nicht protonierten Moleküls auf einer stöichiometrischen Bildung eines OH-Radikalvorproduktes (•O2-) basieren. Die Modellierung der Reaktion der protonierten Spezies unterstützt ebenfalls die These der Bildung des Vorproduktes •O2-, allerdings in unterstöichiometrischer Menge. Die Untersuchung eines Abwassers und eines Kläranlagenablaufs, die mit 10 μmol/L Metoprolol versetzt wurden, zeigte eine OP-Bildung ähnlich der bei pH 8 ohne Radikalfängerzugabe. Dies deutet auf einen signifikanten Einfluss der OH-Radikalreaktion für die Bildung der OP in realer Abwassermatrix hin. Propranolol: Das primäre OP der Ozonreaktion des Propranolols (OP-291) wird über einen Angriff am Naphthalenring gebildet, der zu einer Ringöffnung und der Bildung zweier Aldehydfunktionen führt. OP-291 wird vermutlich über eine OH-Radikalreaktion weiter zu OP-307 oxidiert, welches anschließend zu OP-281 weitereagiert. Durch die mittels Massenspektrometrie identifizierten chemischen Strukturen der OPs, können die vorgeschlagenen Bildungsreaktionen sowohl über direkte Ozonreaktion als auch über OH-Radikalreaktion bestätigt werden. Als Fazit kann festgestellt werden, dass eine Ozonung eines Kläranlagenablaufes zu der Bildung einer Vielzahl von OPs führt, die alle ein unbekanntes toxikologisches Potential haben (z.B. Bildung von Aldehydfunktionen).
This minor thesis shows a way to optimise a generated oracle to achieve shorter runtimes. Shorter runtimes of test cases allows the execution of more test cases in the same time. The execution of more test cases leads to a higher confidence in the software-quality. Oracles can be derived from specifications. However specifications are used for different purposes and therefore are not necessarily executable. Even if the are executable it might be with only a high runtime. Those two facts come mostly from the use of quantifiers in the logic. If the quantifier-range is not bounded, respectively if the bounds are outside the target language-datatype-limits, the specification is too expressive to be exported into a program. Even if the bounds inside the used datatype-limits, the quantification is represented as a loop which leads to a runtime blowup, especially if quantifiers are nested. This work explains four different possibilities to reduce the execution time of the oracle by manipulating the quantified formular whereas this approach is only applicable if the quantified variables are of type Integer.
E-KRHyper is a versatile theorem prover and model generator for firstorder logic that natively supports equality. Inequality of constants, however, has to be given by explicitly adding facts. As the amount of these facts grows quadratically in the number of these distinct constants, the knowledge base is blown up. This makes it harder for a human reader to focus on the actual problem, and impairs the reasoning process. We extend E-Hyper- underlying E-KRhyper tableau calculus to avoid this blow-up by implementing a native handling for inequality of constants. This is done by introducing the unique name assumption for a subset of the constants (the so called distinct object identifiers). The obtained calculus is shown to be sound and complete and is implemented into the E-KRHyper system. Synthetic benchmarks, situated in the theory of arrays, are used to back up the benefits of the new calculus.
In einigen Bereichen des automatischen Theorembeweisens benötigt man das Wissen, dass Konstanten paarweise ungleich sind. Um dieses zu erreichen, fügt man Fakten, die dieses Wissen explizit angeben, zu den Wissensbasen hinzu. Wenn man diese Eigenschaft für viele Konstanten definieren muss, wird die Klauselmenge der Wissensbasen schnell sehr umfangreich und wegen der vielen - eigentlich irrelevanten - Ungleichheiten kann man den Blick auf das eigentlich formalisierte Problem verlieren. Da die Größe der Wissensbasis in vielen Fällen Einfluss auf die Geschwindigkeit hat, ist es auch aus diesem Grund sinnvoll, die Anzahl dieser Fakten gering zu halten. Die unique name assumption erlaubt auf die Einführung der Ungleichheits-Fakten zu verzichten, da sie festlegt, dass zwei Konstanten genau dann gleich sind, wenn ihre Interpretationen identisch sind. Auf diesem Wege lässt sich das Aufblähen von Wissensbasen mit Ungleichheits-Fakten verhinde. In dieser Arbeit wird der E-Hyper-Tableau-Kalkül erweitert um die unique name assumption nutzen zu können. Der in dieser Arbeit entwickelte Kalkül ist vollständig und korrekt, was durch formale Beweise in dieser Arbeit belegt wird. Um zu zeigen, dass die native Behandlung von Ungleichheiten dem Einführen von Ungleichheits-Fakten überlegen ist, wird der Kalkül in den Theorembeweiser E-KRHyper implementieren. Der Theorembeweiser E-KRHyper ist ein etabliertes System und basiert in seiner ursprünglichen Version auf dem E-Hyper-Tableau. Mit systematischen Tests wird dann gezeigt, dass die entwickelte Implementierung des erweiterten Kalküls nie schlechter ist, als der original E-KRHyper, diesen aber in einigen Fällen in der Ausführungsgeschwindigkeit deutlich übertrifft.
ZUSAMMENFASSUNG
Gebäude und Infrastrukturen prägen das Bild unserer Kulturlandschaften und erbringen essentielle Dienstleistungen für die menschliche Gesellschaft. Sie wirken sich jedoch auch unweigerlich auf die natürliche Umwelt aus, z.B. durch die strukturelle Veränderung von Lebensräumen. Überdies gelten sie aufgrund der Freisetzung chemischer Inhaltsstoffe aus den eingesetzten Baumaterialien als potentielle Verursacher negativer Umweltauswirkungen. Galvanische Anoden und organische Beschichtungen, die an Stahlbauwerken regelmäßig zum Schutz vor Korrosion zum Einsatz kommen, sind als Baumaterialien für die Verkehrsinfrastruktur von besonderer Bedeutung. In direktem Kontakt mit einem Wasserkörper oder indirekt über den Abfluss nach einem Niederschlagsereignis können zahlreiche Chemikalien in aquatische Lebensräume emittiert werden und eine Gefahr für Wasserorganismen darstellen. Zur Beurteilung der Umweltverträglichkeit von Bauprodukten existiert bislang kein einheitlicher Untersuchungs- und Bewertungsansatz. Zudem stellen galvanische Anoden und organische Beschichtungen aufgrund ihrer Zusammensetzung besondere Herausforderungen an deren ökotoxikologische Charakterisierung. Ziel der vorliegenden Arbeit war es daher, die Gefährdung der aquatischen Umwelt durch galvanische Anoden und Korrosionsschutzbeschichtungen mithilfe ökotoxikologischer Untersuchungen zu beurteilen und standardisierte Bewertungsverfahren für diese Materialien zu entwickeln.
Die Untersuchung des möglichen Umwelteinflusses durch die Anwendung von Anoden an Offshore-Anlagen erfolgte auf drei trophischen Ebenen. Um eine möglichst realistischste und zuverlässige Abschätzung zu gewährleisten, wurden die Experimente in natürlichem Meerwasser und unter natürlichen pH-Bedingungen durchgeführt. Zudem erfolgte die Exposition gegenüber dem Anodenmaterial und deren Hauptbestandteilen Zink und Aluminum unter Simulation eines Worst-Case-Szenarios. Das untersuchte Anodenmaterial verursachte eine schwache Hemmung des Algenwachstums; auf die getesteten Leuchtbakterien und Flohkrebse zeigte es keine akute Toxizität. Allerdings wurde eine Erhöhung der Aluminium- und Indiumgehalte in den Krebsen festgestellt. Auf Grundlage dieser Ergebnisse wurde keine direkte Gefahr für marine Organismen durch den Einsatz galvanischer Aluminium-Anoden identifiziert. Eine Anreicherung von Metallen in Krebstieren und ein daraus resultierender Eintrag ins marine Nahrungsnetz kann jedoch nicht ausgeschlossen werden.
Die Umweltverträglichkeit organischer Beschichtungssysteme wurde exemplarisch für eine Auswahl relevanter Produkte auf Basis von Epoxidharzen (EP) und Polyurethanen bewertet. Dazu wurden beschichtete Probeplatten schrittweise über 64 Tage ausgelaugt. Die gewonnenen Eluate wurden systematisch auf ihre ökotoxikologischen Effekte (akute Toxizität gegenüber Algen und Leuchtbakterien, mutagene und estrogenartige Wirkungen) und chemische Zusammensetzung analysiert. Dabei zeigten sich insbesondere die EP-basierten Beschichtungen durch die Verursachung erheblicher bakterieller Toxizität und estrogenartiger Wirkung auffällig. Als primärer Urheber dieser Effekte wurde das kontinuierlich freigesetzte 4-tert-Butylphenol identifiziert, dessen Konzentration in allen Proben die predicted no effect concentration für Süßwasser überschritt. Gleichzeitig hat sich gezeigt, dass die Gesamttoxizität nicht durch den Gehalt an 4-tert-Butylphenol in den Produkten bestimmt wird, sondern vom Freisetzungsmechanismus dieser Verbindung aus den untersuchten Polymeren abhängig ist. Diese Ergebnisse deuten darauf hin, dass eine Optimierung der Zusammensetzung, beispielsweise aufgrund einer besseren Polymerisation der Inhaltsstoffe, zu einer Reduzierung von Emissionen und damit zu einer verminderten Belastung der Umwelt führen kann.
Regen, Temperaturwechsel und Sonneneinstrahlung können zur Verwitterung polymerer Korrosionsschutzbeschichtungen führen. Um den Einfluss lichtbedingter Alterung auf die Ökotoxizität von Deckbeschichtungen zu erfassen, wurde die Emissionen und damit verbundene negative Auswirkungen von UV-bestrahlten und unbehandelten EP-basierten Produkten miteinander verglichen. Nach statischer Auslaugung stand dabei die Untersuchung estrogenartiger und bakterien-toxischer Wirkungen im Fokus, die sowohl im klassischen Mikrotiterplattenformat als auch in Kopplung mit Dünnschichtplatten detektiert wurden. Beide untersuchten Materialien zeigten nach Bestrahlung eine signifikante Abnahme der ökotoxikologischen Effekte bei gleichzeitiger Verringerung der Freisetzung von 4-tert-Butylphenol. Jedoch wurden auch Bisphenol A und verschiedene Strukturanaloga als photolytische Abbauprodukte der Polymere nachgewiesen, die ebenfalls zur beobachteten Wirkung beitrugen. Die Identifizierung bioaktiver Inhaltsstoffe konnte dabei durch die erfolgreiche Kombination der in-vitro-Bioassays mit chemischen Analysen im Sinne einer effektgeleiteten Analytik unterstützt werden. Die vorliegenden Ergebnisse liefern wichtige Hinweise für die Beurteilung der generellen Eignung von Deckbeschichtungen auf Basis von Epoxidharzen.
Das im Rahmen der vorliegenden Studie entwickelte Untersuchungskonzept konnte erfolgreich auf eine Auswahl relevanter Baumaterialien angewendet werden. Die gezielte Anpassung einzelner Standardmethoden erlaubte dabei eine individuelle Produktbewertung. Gleichzeitig wurde sowohl die Zweckmäßigkeit der angewendeten ökotoxikologischen Methoden für die Untersuchung von Materialien unbekannter und komplexer Zusammensetzung bestätigt als auch die Basis für eine systematische Bewertung der Umweltverträglichkeit von Korrosionsschutzprodukten geschaffen. Vor dem Hintergrund der Europäischen Bauprodukteverordnung kann der gewählte Ansatz dem einfachen Vergleich verschiedener Baumaterialien z.B. innerhalb einer Produktgruppe dienen und damit die Auswahl umweltverträglicher Produkte vereinfachen und zur Optimierung einzelner Rezepturen beitragen.
Die Verwendung physiologischer Indikatoren, welche die Reaktion von Organismen auf Veränderungen ihrer Umwelt widerspiegeln, bietet ein großes Potenzial für ökologische Studien. Durch die Analyse des physiologischen Zustandes von Organismen ermöglichen diese Indikatoren eine schnellere Erfassung von Veränderungen in aquatischen Ökosystemen als es durch die Betrachtung ökologischer Indikatoren, wie z. B. der Struktur der Benthosgemeinschaft oder des Reproduktionserfolges einzelner Arten, möglich ist. Dieser Zeitvorteil kann sowohl die Effektivität der Habitatbewertung als auch experimenteller Studien in der aquatischen Ökologie erhöhen. In diesem Zusammenhang konzentriert sich die vorliegende Arbeit auf physiologische Messgrößen, wie die Konzentration von Energiespeicherstoffen, den zellulären Energiestatus (Adenylate Energy Charge) oder die Stoffwechselaktivität in vivo, die den energetischen Zustand oder den aktuellen Energieverbrauch von Organismen charakterisieren, sowie auf das RNA:DNA-Verhältnis als Wachstumsindikator. Obwohl diese Indikatoren in der marinen Ökologie, und in jüngerer Zeit auch in der Ökotoxikologie, regelmäßig verwendet werden, haben sie in der limnischen Ökologie bisher wenig Anwendung gefunden. Um die Anwendung physiologischer Indikatoren in diesem Bereich zu verstärken verfolgt die Dissertation zwei Ziele. Zum einen verdeutlicht sie das Potenzial der einzelnen physiologischen Indikatoren, zum anderen stellt sie Grundlagenwissen zu ausgewählten ökophysiologischen Aspekten einheimischer und gebietsfremder Arten der Ordnung Amphipoda bereit, die als Schlüsselarten aquatischer Lebensräume als besonders geeignet für die Bestimmung physiologischer Indikatoren angesehen werden. In diesem Sinne werden in Kapitel 2 sowohl die grundlegenden Annahmen, als auch die theoretischen und methodischen Grundlagen für die Bestimmung physiologischer Indikatoren aufgezeigt und ihre Anwendbarkeit in Fallstudien verdeutlicht. Die durchgeführten Experimentalstudien (Kapitel 3−5) liefern Informationen zu (i) den art- und geschlechtsspezifischen Unterschieden in der saisonalen Variation des energetischen Zustandes natürlicher Gammarus Populationen (G. fossarum, G. pulex), (ii) den Unterschieden in der Stoffwechsel- und Bewegungsaktivität verschiedener Amphipoda-Arten (G. fossarum, G. roeselii und D. villosus), sowie (iii) den direkten Auswirkungen von Ammoniak auf die Physiologie und die Bewegungsaktivität von D. villosus. In Kapitel 6 werden abschließend die grundlegenden Schlussfolgerungen aus den durchgeführten Feld- und Laborstudien, sowie ihre Relevanz und Auswirkungen für die Anwendung physiologischer Indikatoren in der limnischen Ökologie diskutiert.
Das Ziel dieser Masterarbeit war es ein CRM System für das Assist Team der CompuGroup Medical zu entwickeln, welches Open Innovation in die Entwicklung der Minerva 2.0 Software integriert. Um dies zu erreichen wurden CRM Methoden mit Social Networ- king Systemen kombiniert, basierend auf der Forschung von Lin und Chen (2010, S. 11 – 30). Um die definierten Ziele zu erreichen wurde Literatur analysiert, wie ein CRM System und eine Online Community erfolgreich implementiert werden können und dies auf die Entwicklung der Minerva Community angewendet. Dabei wurde sich an den Design Science Richtlinien von Hevner u. a. (2004, S. 75 – 104) orientiert. Das fertige Produkt wurde basierend auf Kunden- und Managementanforderungen entworfen und wurde an- schließend aus Kunden- und Firmenperspektive evaluiert.
The model evolution calculus
(2004)
The DPLL procedure is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas. The recent FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without resorting to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice. In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful litfing of the DPLL procedure, the new calculus contains a more systematic treatment of universal literals, one of FDPLL's optimizations, and so has the potential of leading to much faster implementations.
The Living Book is a system for the management of personalized and scenario specific teaching material. The main goal of the system is to support the active, explorative and selfdetermined learning in lectures, tutorials and self study. The Living Book includes a course on 'logic for computer scientists' with a uniform access to various tools like theorem provers and an interactive tableau editor. It is routinely used within teaching undergraduate courses at our university. This paper describes the Living Book and the use of theorem proving technology as a core component in the knowledge management system (KMS) of the Living Book. The KMS provides a scenario management component where teachers may describe those parts of given documents that are relevant in order to achieve a certain learning goal. The task of the KMS is to assemble new documents from a database of elementary units called 'slices' (definitions, theorems, and so on) in a scenario-based way (like 'I want to prepare for an exam and need to learn about resolution'). The computation of such assemblies is carried out by a model-generating theorem prover for first-order logic with a default negation principle. Its input consists of meta data that describe the dependencies between different slices, and logic-programming style rules that describe the scenario-specific composition of slices. Additionally, a user model is taken into account that contains information about topics and slices that are known or unknown to a student. A model computed by the system for such input then directly specifies the document to be assembled. This paper introduces the elearning context we are faced with, motivates our choice of logic and presents the newly developed calculus used in the KMS.
Hyper tableaux with equality
(2007)
In most theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equality in the hyper tableau calculus. It is based on splitting of positive clauses and an adapted version of the superposition inference rule, where equations used for paramodulation are drawn (only) from a set of positive unit clauses, the candidate model. The calculus also features a generic, semantically justified simplification rule which covers many redundancy elimination techniques known from superposition theorem proving. Our main results are soundness and completeness, but we briefly describe the implementation, too.
We aim to demonstrate that automated deduction techniques, in particular those following the model computation paradigm, are very well suited for database schema/query reasoning. Specifically, we present an approach to compute completed paths for database or XPath queries. The database schema and a query are transformed to disjunctive logic programs with default negation, using a description logic as an intermediate language. Our underlying deduction system, KRHyper, then detects if a query is satisfiable or not. In case of a satisfiable query, all completed paths -- those that fulfill all given constraints -- are returned as part of the computed models. The purpose of our approach is to dramatically reduce the workload on the query processor. Without the path completion, a usual XML query processor would search the database for solutions to the query. In the paper we describe the transformation in detail and explain how to extract the solution to the original task from the computed models. We understand this paper as a first step, that covers a basic schema/query reaÂsoning task by model-based deduction. Due to the underlying expressive logic formalism we expect our approach to easily adapt to more sophisticated problem settings, like type hierarchies as they evolve within the XML world.
Die Arbeit geht von der grundlegenden Annahme aus, dass spezifische kulturelle Bedingungen psychopathologische Effekte haben können, die interpersonale Gewalt begünstigen. Ziel der Studie war die Klärung der Frage, ob die Häufigkeit von Tötungsdelikten (abhängige Variable) mit bestimmten Einstellungen, Überzeugungen, Werthaltungen und Ausprägungen auf kulturellen Merkmalsdimensionen zusammenhängt. Um diese Frage zu klären, wurden unabhängige Variablen ausgewählt, von denen sechs sich auf die Wichtigkeit von Religion (Religiosität), Kontroll- und Machtorientierung (Omnipotenz), die kategorische Unterscheidung von Gut und Böse (Absolutismus), Nationalstolz (Nationalismus), Akzeptanz von Wettbewerb (Wettbewerbsorientierung) und Befürwortung von Autorität und Strafe (Autoritarismus) beziehen. Die zur Messung dieser Variablen relevanten Daten wurden dem World Values Survey entnommen. Für zwei weitere Kulturdimensionen, Kollektivismus und Machtdistanz, wurden die Ergebnisse der Studien von Hofstede verwendet. Als neunte unabhängige Variable diente das Bruttonationaleinkommen. Mittels multipler Imputation wurden die 7% fehlender Messwerte durch Schätzwerte ergänzt, so dass die Daten von 82 Staaten für die Analysen zur Verfügung standen.rnErgebnisse: Eine schrittweise multiple Regression ergab für Omnipotenz (β = .44, P < .01) und Bruttonationaleinkommen (ß = -.27, P < .01) die stärksten Regressionseffekte auf die Tötungsrate als abhängige Variable. Die neun unabhängigen Variablen luden auf zwei Faktoren, soziökonomischer Entwicklungsstand (SED) und psychokultureller Faktor (Psy-Cul), die negativ korreliert waren (-.47). Psy-Cul wurde als Indikator für Narzismus und als Mediator des Effekts von SED auf Tötungsrate interpretiert. Hierarchische Clusteranalysen auf der Basis der beiden Faktoren ergaben eine klare Unterscheidung zwischen drei Gruppen von Nationen: westliche Nationen, Entwicklungsnationen und postkommunistische Nationen.
Diese Arbeit beschreibt die Implementation eines Pfadplanungs-Algorithmus für Seriengespannfahrzeuge mithilfe von Maschinellen Lernalgorithmen. Zu diesem Zwecke wird ein allgemeiner Überblick über genetische Algorithmen gegeben, alternative Ansätze werden ebenfalls kurz erklärt. Die Software die zu diesem Zwecke entwickelt wurde basiert auf der EZSystem Simulationssoftware der AG Echtzeitsysteme der Universität Koblenz-Landau, sowie auf der von Christian Schwarz entwickelten Pfadkorrektursoftware, die ebenfalls hier beschrieben wird. Diese enthält auch eine Beschreibung des, zu Simulationszwecken, verwendeten Fahrzeugs. Genetische Algorithmen als Lösung von Pfadplanungsproblemen in komplexen Szenarien werden dann, basierend auf der entwickelten Simulationssoftware, evaluiert und diese Ergebnisse werden dann mit alternativen, nicht-maschinellen Lernalgorithmen, verglichen. Diese werden ebenfalls kurz erläutert.