Filtern
Erscheinungsjahr
- 2013 (23) (entfernen)
Dokumenttyp
- Dissertation (10)
- Bachelorarbeit (4)
- Ausgabe (Heft) zu einer Zeitschrift (4)
- Masterarbeit (2)
- Konferenzveröffentlichung (1)
- Diplomarbeit (1)
- Habilitation (1)
Sprache
- Englisch (23) (entfernen)
Schlagworte
- Pflanzenschutzmittel (3)
- ABox (1)
- Abduktion <Logik> (1)
- Agrochemikalien (1)
- Bach (1)
- Boden (1)
- Bodenchemie (1)
- Bodenökologie (1)
- C++ (1)
- Calculus (1)
English prepositions take only a small proportion of the language but play a substantial role. Although prepositions are of course also frequently used in English textbooks for secondary school, students fail to incidentally acquire them and often show low achievements in using prepositions correctly. The strategy commonly employed by language instructors is teaching the multiple senses of prepositions by rote which fails to help the students to draw links between the different meanings in usage. New findings in Cognitive Linguistics (CL) suggest a different approach to teaching prepositions and thus might have a strong impact on the methodologies of foreign language teaching and learning on the aspects of meaningful learning. Based on the Theory of Domains (Langacker, 1987), the notions of image schemas (Johnson, 1987) as well as the Conceptual Metaphor Theory (Lakoff & Johnson, 1980), the present study developed a CL-inspired approach to teaching prepositions, which was compared to the traditional teaching method by an empirical study conducted in a German school setting. Referring to the participants from the higher track and the medium track, who are at different proficiency levels, the results indicate that the CL-inspired teaching approach improved students" performance significantly more than the traditional approach in all the cases for the higher track and in some cases for the medium track. Thus, these findings open up a new perspective of the CL-inspired meaningful learning approach on language teaching. In addition, the CL-inspired approach demonstrates the unification of the integrated model of text and picture comprehension (the ITPC model) in integrating the new knowledge with related prior knowledge in the cognitive structure. According to the learning procedure of the ITPC model, the image schema as visual image is first perceived through the sensory register, then is processed in the working memory by conceptual metaphor, and finally it is integrated with cognitive schemata in the long term memory. Moreover, deep-seated factors, such as transfer of mother tongue, the difficulty of teaching materials, and the influence of prior knowledge, have strong effects on the acquisition of English prepositions.
Etwa 50 % der Fläche Europas werden landwirtschaftlich genutzt. Dennoch gibt es nahezu keine Information ob Fledermäuse diese Flächen beispielsweise zur Nahrungsaufnahme nutzen. Aufgrund der limitierten Datenbasis mangelt es auch an Schutzkonzepten, die mögliche negative Effekte der landwirtschaftlichen Intensivierung auf die Fledermäuse und deren Nahrungsgrundlage ausgleichen könnten. Da die Exposition von Fledermäusen mit Pflanzenschutzmitteln bislang nicht thematisiert wurde, sind im europäischen Zulassungsverfahren für Pflanzenschutzmittel keine Risikoabschätzungen für Fledermäuse gefordert. Um für Fledermäuse die mögliche Exposition gegenüber Pflanzenschutzmitteln abschätzen zu können, sind Informationen über Vorkommen und Aktivität von Fledermäusen in landwirtschaftlich genutzten Flächen erforderlich. Die Erfassung von Fledermäusen auf einer Vielzahl von Flächen machte es notwendig sich im Vorfeld auf eine geeignete Methodik festzulegen. Die akustische Fledermauserfassung ist im Gegensatz zu deutlich zeitaufwändigeren Methoden wie Netzfang, Telemetrie oder direktes Beobachten die einzige logistisch durchführbare Methode. In der wissenschaftlichen Literatur werden jedoch bei vielen bisher durchgeführten akustischen Methoden Bedenken bezüglich der Berücksichtigung zeitlicher und räumlicher Varianz und der Eignung der verwendeten Detektorsysteme geäußert. Deshalb wurden verschiedene Methoden und Detektorsysteme verglichen und das parallele Beproben mit mehreren stationären und kalibrierten automatischen Aufnahmesystemen als die am besten geeignete Methode zur verlässlichen und vergleichbaren Fledermausaktivitäts-Erfassung befunden.
Mit dieser Methode wurden die Fledermaus-Diversitäten und Aktivitäten in verschiedenen landwirtschaftlichen Kulturen, Wiesen und Wäldern aufgenommen. Außerdem wurde gleichzeitig die Verfügbarkeit von fliegenden Insekten (potentieller Fledermausbeute) mit Licht- oder Klebefallen erfasst. In mehr als 500 Erfassungsnächten wurden circa 110,000 akustische Fledermaus-Rufsequenzen und nahezu 120,000 nachtaktive Insekten gesammelt. Insgesamt wurden 14 Fledermausarten nachgewiesen, darunter die im Gebiet sehr seltene und stark bedrohte Nordfledermaus (Eptesicus nilssonii) und die Mopsfledermaus (Barbastella barbastellum). Alle Arten wurden auch auf landwirtschaftlich genutzten Flächen detektiert.
Die Landwirtschaft im südlichen Rheinland-Pfalz ist durch Weinanbau geprägt. Die Untersuchungen zeigten, dass Weinberge aufgrund der geringen Verfügbarkeit an kleineren nachtaktiven Insekten für die meisten Fledermausarten nur eine geringe Qualität als Jagdgebiet haben. Ein weiterer paarweiser Vergleich von Weinbergen und benachbarten Regenrückhaltebecken bezüglich Nahrungsverfügbarkeit und Fledermausaktivität zeigte, dass Regenrückhaltebecken wichtige Nahrungshabitate im Weinbaugebiet darstellen. Das Anlegen dieser künstlichen Kleingewässer ist somit eine geeignete Methode um Nahrungshabitate für Fledermäuse zu schaffen und damit den negativen Effekten der konventionellen Landwirtschaft hinsichtlich der Nahrungsverfügbarkeit entgegenzuwirken. In anderen landwirtschaftlichen Kulturen wurden mit den parallel untersuchten Wald- und Wiesenhabitaten vergleichbar hohe Insektenvorkommen und Fledermausaktivitäten nachgewiesen. Besonders hohe Fledermausaktivitäten so wie eine besonders hohe Verfügbarkeit von geeigneten Nahrungstieren wurden in Apfelplantangen und Gemüsefeldern gemessen. Da diese beiden Kulturen hohem Pestizidaufwand unterliegen, kann eine Exposition von Fledermäusen gegenüber Pflanzenschutzmitteln dort nicht ausgeschlossen werden. Um das zurzeit verwendete Verfahren zur Risikoabschätzung von Pflanzenschutzmittel-anwendungen auf Vögel und Säuger auf Fledermäuse zu übertragen, wurden nach Applikation eines Insektizides dessen Rückstände auf Fledermaus-artspezifischen Beuteinsekten gemessen. Parallel dazu wurde die Fledermausaktivität erfasst. Die höchsten Pestizidrückstände wurden auf kronenbewohnenden Insekten und Spinnen nachgewiesen. Die darauf basierende Risikoabschätzung deutet auf ein Langzeitrisiko für alle Fledermausarten, die sich wenigstens zum Teil von kronenbewohnenden Arthropoden ernähren, hin. Das Vorkommen von Fledermäusen in landwirtschaftlichen Flächen, die einen Großteil der europäischen, aber auch der weltweiten Fläche ausmachen, führt je nach Kultur zur Exposition von Fledermäusen durch kontaminierte Nahrung oder zu einer Verringerung von Beuteinsekten. Bisher konzentrierten sich Schutzbemühungen auf die Sicherung von Winterquartieren und die Bereitstellung künstlicher Tagesquartiere. Potentielle Effekte von Pflanzenschutzmitteln auf Agrarflächen haben aber möglicherweise einen entscheidenden Einfluss auf die Populationsgrößen von Fledermausarten die in diesen Gebieten vorkommen. Aus diesem Grund sollten die Effekte von Pflanzenschutzmitteln auf Fledermäuse untersucht werden, insbesondere bei der Risikoabschätzung im Pflanzenschutzmittel-Zulassungsverfahren.
Agricultural pesticides, especially insecticides, are an integral part of modern farming. However, these may often leave their target ecosystems and cause adverse effects in non- target, especially freshwater ecosystems, leading to their deterioration. In this thesis, the focus will be on Insect Growth Regulators (IGRs) that can in many ways cause disruption of the endocrine system of invertebrates. Freshwater invertebrates play important ecological, economic and medical roles, and disruption of their endocrine systems may be crucial, considering the important role hormones play in the developmental and reproductive processes in organisms. Although Endocrine Disruption Chemicals (EDCs) can affect moulting, behaviour, morphology, sexual maturity, time to first brood, egg development time, brood size (fecundity), and sex determination in invertebrates, there is currently no agreement upon how to characterize and assess endocrine disruption (ED). Current traditional ecotoxicity tests for Ecological Risk Assessment (ERA) show limitations on generating data at the population level that may be relevant for the assessment of EDCs, which effects may be sublethal, latent and persist for several generations of species (transgenerational).
It is therefore the primary objective of this thesis to use a test method to investigate adverse effects of EDCs on endpoints concerning development and reproduction in freshwater invertebrates. The full life-cycle test over two generations that includes all sensitive life stages of C. riparius (a sexual reproductive organism) allows an assessment of its reproduction and should be suitable for the investigation of long-term toxicity of EDCs in freshwater invertebrates. C. riparius is appropriate for this purpose because of its short life cycle that enables the assessment of functional endpoints of the organism over several generations. Moreover, the chironomid life cycle consists of a complete metamorphosis controlled by a well-known endocrine mechanism and the endocrine system of insects has been most investigated in great detail among invertebrates. Hence, the full life-cycle test with C. riparius provides an approach to assess functional endpoints (e.g. reproduction, sex ratio) that are population-relevant as a useful amendment to the ERA of EDCs. In the laboratory, C. riparius was exposed to environmentally-relevant concentrations of the selected IGRs in either spiked water or spiked sediment scenario over two subsequent generations.
The results reported in this thesis revealed significant effects of the IGRs on the development and the reproduction of C. riparius with the second (F1) generation showing greater sensitivity. These findings indicated for the first time the suitability of multigenerational testing for various groups of EDCs and strongly suggested considering the full life-cycle of C. riparius as an appropriate test method for a better assessment of EDCs in the freshwater environment. In conclusion, this thesis helps to detect additional information that can be extrapolated at population level and, thus, might contribute to better protection of freshwater ecosystems against the risks of Endocrine Disrupting Chemicals (EDCs.) It may furthermore contribute to changes in the ERA process that are necessary for a real implementation of the new European chemical legislation, REACH (Registration, Evaluation Authorization and Restriction of Chemicals). Finally, significant interactions between temperature, chemical exposure and generation were reported for the first time and, may help predict impacts that may occur in the future, in the field, under predicted climate change scenarios.
Die vorliegende Dissertation behandelt den Einsatz von Theorembeweise innerhalb der automatischen Fragebeantwortung (question answering - QA). QA-Systeme versuchen, natürlichsprachliche Fragen korrekt zu beantworten. Sie verwenden eine Vielzahl von Methoden aus der Computerlinguistik und der Wissensrepräsentation, um menschliche Sprache zu verarbeiten und die Antworten aus umfangreichen Wissensbasen zu beziehen. Diese Methoden sind allerdings meist syntaxbasiert und können kein implizites Wissen herleiten. Die Theorembeweiser der automatischen Deduktion dagegen können Folgerungsketten mit Millionen von Inferenzschritten durchführen. Die Integration eines Beweisers in ein QA-System eröffnet die Möglichkeit, aus den Fakten einer Wissensbasis neues Wissen herzuleiten und somit die Fragebeantwortung zu verbessern. Herausforderungen liegen in der Überwindung der gegensätzlichen Herangehensweisen von Fragebeantwortung und Deduktion: Während QA-Methoden normalerweise darauf abzielen, auch mit unvollständigen oder fehlerhaften Daten robust und schnell zu halbwegs annehmbaren Ergebnissen zu kommen, verwenden Theorembeweiser logische Kalküle zur Gewinnung exakter und beweisbarer Resultate. Letzterer Ansatz erweist sich sich aber als schwer vereinbar mit der Quantität und der Qualität der im QA-Bereich üblichen Wissensbestände.
Die Dissertation beschreibt Anpassungen von Theorembeweisern zur Überwindung dieser Hürden. Zentrales Beispiel ist der an der Universität Koblenz-Landau entwickelte Beweiser E-KRHyper, der im Rahmen dieser Dissertation in das QA-System LogAnswer integriert worden ist. Außerdem vorgestellt werden zusätzliche Erweiterungsmöglichkeiten auf der Implementierungs- und der Kalkülebene, die sich aus dem praktischen Einsatz bei der Fragebeantwortung ergeben haben, dabei aber generell für Theorembeweiser von Nutzen sein können. Über die reine Deduktionsverbesserung der QA hinausgehend beinhalten diese Erweiterungen auch die Anbindung externer Wissensquellen wie etwa Webdienste, mit denen der Beweiser während des Deduktionsvorgangs gezielt Wissenslücken schließen kann. Zudem ermöglicht dies die Nutzung externer Ontologien beispielsweise zur Abduktion. Evaluationsergebnisse aus eigenen Versuchsreihen und aus Wettbewerben demonstrieren die Effektivität der diskutierten Methoden.
Autonome Systeme, wie Roboter, sind bereits Teil unseres täglichen Lebens. Eine Sache, in der Menschen diesen Maschinen überlegen sind, ist die Fähigkeit, auf sein Gegenüber angemessen zu reagieren. Dies besteht nicht nur aus der Fähigkeit zu hören, was eine Person sagt, sondern auch daraus, ihre Mimik zu erkennen und zu interpretieren.
In dieser Bachelorarbeit wird ein System entwickelt, welches automatisch Gesichtsausdrücke erkennt und einer Emotion zuordnet. Das System arbeitet mit statischen Bildern und benutzt merkmalsbasierte Methoden zur Beschreibung von Gesichtsdaten. In dieser Arbeit werden gebräuchliche Schritte analysiert und aktuelle Methoden vorgestellt. Das beschriebene System basiert auf 2D-Merkmalen. Diese Merkmale werden im Gesicht detektiert. Ein neutraler Gesichtsausdruck wird nicht als Referenzbild benötigt. Das System extrahiert zwei Arten von Gesichtsparametern. Zum einen sind es Distanzen, die zwischen den Merkmalspunkten liegen. Zum anderen sind es Winkel, die zwischen den Linien liegen, die die Merkmalspunkte verbinden. Beide Arten von Parametern werden implementiert und getestet. Der Parametertyp, der die besten Ergebnisse liefert, wird schließlich in dem System benutzt. Eine Support Vector Machine (SVM) mit mehreren Klassen klassifiziert die Parameter. Das Ergebnis sind Kennzeichen von Action Units des Facial Action Coding Systems (FACS). Diese Kennzeichen werden einer Gesichtsemotion zugeordnet.
Diese Arbeit befasst sich mit den sechs Basisgesichtsausdrücken (glücklich, überrascht, traurig, ängstlich, wütend und angeekelt) plus dem neutralen Gesichtsausdruck. Das vorgestellte System wird in C++ implementiert und an das Robot Operating System (ROS) angebunden.
Concept for a Knowledge Base on ICT for Governance and Policy Modelling regarding eGovPoliNet
(2013)
Das EU-Projekt eGovPoliNet beschäftigt sich mit der Forschung und Entwicklung im Bereich der Informations- und Kommunikationstechnologien (IKT) für Steuerung und Politikgestaltung. Zahlreiche Communities verfolgen in diesem Themenbereich ähnliche Ziele der IT-unterstützten, strategischen Entscheidungsfindung und Simulation sozialer Problemfelder. Die vorhandenen Lösungsansätze sind bislang jedoch recht fragmentiert. Ziel von eGovPoliNet ist es in diesem Zusammenhang der Fragmentierung zu begegnen und durch die Förderung der Kooperation von Forschung und Praxis einen internationalen, offenen Dialog zu etablieren. Dieser wird durch die Beteiligung der Akteure auf diesem Gebiet der IKT die Diskussion und Entwicklung verschiedener Problemfelder voranbringen. Hierbei werden Akteure aus Forschung und Praxis ihre Expertise und Best-Practice Erkenntnisse teilen, um Politikanalyse, Modellierung und Steuerung zu unterstützen. eGovPoliNet wird zur Unterstützung dieses Dialogs eine Wissensbasis bereitstellen, deren konzeptuelle Ausarbeitung Gegenstand dieser Arbeit ist. Die Wissensbasis soll mit Inhalten aus dem Bereich der IKT zur strategischen Entscheidungsfindung und Simulation sozialer Problemfelder gefüllt werden, beispielsweise mit Publikationen, Softwarelösungen, oder Projektbeschreibungen. Diese Inhalte gilt es zu strukturieren, nutzenstiftend zu organisieren und zu verwalten, sodass die Wissensbasis letztendlich als Quelle gesammelten Wissens dient, welche die bislang fragmentierten Forschungs- und Entwicklungsergebnisse an zentraler Stelle vereint.
Ziel dieser Arbeit ist es also, ein Konzept einer Wissensbasis zu entwerfen, welches die nötige Struktur und die nötigen Funktionen bietet, Wissen bezüglich IKT-Lösungen zu verwalten. Das bedeutet in diesem Zusammenhang Wissen zu sammeln, aufzubereiten und dem Nutzer zugänglich zu machen. Die Wissensbasis soll außerdem nach Inhalten durchsuchbar sein. Desweiteren sollen die Nutzer motiviert werden, selbstständig an der Weiterentwicklung und Pflege der Wissensbasis mitzuwirken.
Große Mengen qualitativer Daten machen die Verwendung computergestützter Verfahren bei deren Analyse unvermeidlich. In dieser Thesis werden Text Mining als disziplinübergreifender Ansatz, sowie die in den empirischen Sozialwissenschaften üblichen Methoden zur Analyse von schriftlichen Äußerungen vorgestellt. Auf Basis dessen wird ein Prozess der Extraktion von Konzeptnetzwerken aus Texten skizziert, und die Möglichkeiten des Einsatzes von Verfahren zur Verarbeitung natürlicher Sprachen aufgezeigt. Der Kern dieses Prozesses ist die Textverarbeitung, zu deren Durchführung Softwarelösungen die sowohl manuelles als auch automatisiertes Arbeiten unterstützen, notwendig sind. Die Anforderungen an diese Werkzeuge werden unter Berücksichtigung des initiierenden Projektes GLODERS, welches sich der Erforschung von Schutzgelderpressung durchführenden Gruppierungen als Teil des globalen Finanzsystems widmet, beschrieben, und deren Erfüllung durch die zwei hervorstechendsten Kandidaten dargelegt. Die Lücke zwischen Theorie und Praxis wird durch die prototypische Anwendung der Methode unter Einbeziehung der beiden Lösungen an einem dem Projekt entspringenden Datensatz geschlossen.
Wir präsentieren die konzeptuellen und technologischen Grundlagen einer verteilten natürlich sprachlichen Suchmaschine, die einen graph-basierten Ansatz zum Parsen einer Anfrage verwendet. Das Parsing-Modell, das in dieser Arbeit entwickelt wird, generiert eine semantische Repräsentation einer natürlich sprachlichen Anfrage in einem 3-stufigen, übergangsbasierten Verfahren, das auf probabilistischen Patterns basiert. Die semantische Repräsentation einer natürlich sprachlichen Anfrage wird in Form eines Graphen dargestellt, der Entitäten als Knoten und deren Relationen als Kanten repräsentiert. Die präsentierte Systemarchitektur stellt das Konzept einer natürlich sprachlichen Suchmaschine vor, die sowohl in Bezug auf die einbezogenen Vokabulare, die zum Parsen der Syntax und der Semantik einer eingegebenen Anfrage verwendet werden, als auch in Bezug auf die Wissensquellen, die zur Gewinnung von Suchergebnissen konsultiert werden, unabhängig ist. Diese Funktionalität wird durch die Modularisierung der Systemkomponenten erreicht, die externe Daten durch flexible Module anspricht, welche zur Laufzeit modifiziert werden können. Wir evaluieren die Leistung des Systems indem wir die Genauigkeit des syntaktischen Parsers, die Präzision der gewonnenen Suchergebnisse sowie die Geschwindigkeit des Prototyps testen.
Weltweit sind ein Drittel bis die Hälfte der Flusskrebsarten von Populationsrückgang oder Aussterben bedroht. Neben einer Verschlechterung der Habitate, Umweltverschmutzung und anderen vom Menschen verursachten Umweltveränderungen stellen eingeschleppte exotische Arten und Krankheitserreger eine große Bedrohung für das Überleben europäischer Flusskrebsarten dar. Flusskrebse sind die größten Wirbellosen in limnischen Systemen und haben einen entsprechend großen Einfluss auf die Struktur der Nahrungsnetze. Das Verschwinden von Flusskrebsen aus einem Gewässer kann Nahrungsnetze verändern und somit dramatische Konsequenzen für ein Ökosystem zur Folge haben. Ein Ziel im modernen Artenschutz ist die Erhaltung der genetischen Vielfalt. Eine hohe genetische Vielfalt ist für das langfristige Überleben einer Art von Vorteil.
Das Hauptziel meiner Arbeit war es, die genetische Struktur des gefährdeten Edelkrebses (Astacus astacus) in seinem europäischen Verbreitungsgebiet zu untersuchen und die besonders schützenswerten genetische 'Hotspots' zu identifizieren (Teil 1 der Dissertation). Die größte Bedrohung für die Diversität europäischer Flusskrebsarten stellt der Krebspesterreger Aphanomyces astaci dar. Daher muss die Verbreitung des Krankheitserregers bei Schutzprogrammen beachtet werden.
Im zweiten Teil der Dissertation untersuchte ich neue Aspekte der Verbreitung von A. astaci. Die Ergebnisse dienen als Grundlage für zukünftige Artenschutzprogramme für Flusskrebse.
Im ersten Teil dieser Arbeit führte ich eine phylogeographische Analyse der Edelkrebse durch, um genetische 'Hotspots' zu identifizieren und die nacheiszeitliche Wiederbesiedlung Zentraleuropas durch diese Art zu rekonstruieren. Mit mitochondrialer DNA und nuklearen Mikrosatelliten-Markern ermittelte ich eine hohe genetische Vielfalt in Südosteuropa, die darauf hinweist, dass der Edelkrebs die kalten Klimaphasen des Pleistozäns in diesem Gebiet überdauerte (Appendix 1). Wegen der hohen genetischen Vielfalt ist Südosteuropa von besonderer Bedeutung für den Schutz des Edelkrebses. Die mitochondriale DNA-Analyse deutet auf eine gegabelte Kolonisierung vom unteren Donaueinzugsgebiet in a) das Einzugsgebiet der Nordsee und b) das Einzugsgebiet der Ostsee hin (Kapitel 2). Ein zweites, unabhängiges Refugium, welches im westlichen Balkan lokalisiert wurde, hat vermutlich nicht zur Besiedlung Mitteleuropas beigetragen. Außerdem stellte ich fest, dass die natürliche genetische Struktur teilweise überlagert ist, wahrscheinlich aufgrund des hohen menschlichen Einflusses auf die Verbreitung des Edelkrebses (bspw. künstliche Translokation). Im zweite Teil dieser Arbeit konnte ich mittels real-time-PCR ermitteln, dass neben den bekannten drei nordamerikanischen Flusskrebsarten auch Kalikokrebse (Orconectes immunis) Träger des Krebspesterregers sind (Kapitel 3). Des Weiteren habe ich den Krebspesterrreger in der unteren Donau in Rumänien an amerikanischen Kamberkrebsen (Orconectes limosus) und europäischen Galizierkrebsen (Astacus leptodactylus) nachweisen können (Kapitel 4). Die Ausbreitung der infizierten Kamberkrebse bis in die untere Donau stellt eine große Bedrohung für die Artenvielfalt in Südosteuropa dar und zeigt das hohe Invasionspotential der Kamberkrebse. Darüber hinaus stellte ich fest, dass auch einheimische Galizierkrebse im Donaudelta, etwa 970 km hinter der aktuellen Invasionsfront des Kamberkrebses, Träger von A. astaci sind (Kapitel 5). Diese Erkenntnis ist von besonderer Bedeutung, da die einheimischen Arten offenbar nicht an der Infektion leiden. Die Untersuchung koexistierender Populationen europäischer und amerikanischer Flusskrebse ergab, dass die Abwesenheit des Krebspesterregers in diesen Populationen die wahrscheinlichste Erklärung für die erfolgreiche Koexistenz in den untersuchten Gewässern in Mitteleuropa ist (Kapitel 6). Die Ergebnisse meiner Dissertation zeigen neue Aspekte, die von hoher Relevanz für den Schutz und Erhalt einheimischer Flusskrebsarten und deren genetischer Vielfalt sind: 1)Die genetische Diversität des Edelkrebses ist in Südosteuropa am höchsten. Dort überdauerten Edelkrebse die letzte Eiszeit in mindestens zwei unabhängigen Refugien. 2) Nicht alle amerikanischen Flusskrebspopulationen sind Träger der Krebspest und 3) nicht alle europäischen Flusskrebspopulationen sterben innerhalb kurzer Zeit an einer Infizierung mit dem Krebspesterreger. Um einheimische Flusskrebse und deren (genetische) Vielfalt langfristig zu erhalten, dürfen keine weiteren amerikanischen Flusskrebse in der Natur ausgesetzt werden. Das unbefugte Aussetzen wird jedoch erst zurückgehen, wenn der Handel mit exotischen Flusskrebsen verboten wird.
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.