Refine
Document Type
- Preprint (3)
- Article (1)
- Master's Thesis (1)
Has Fulltext
- yes (5)
Keywords
- Ameisen (1)
- Herbivorie (1)
- Pflanzenabwehr (1)
- Pilz (1)
- ants (1)
- fungus (1)
- herbivory (1)
- induced (1)
- induziert (1)
- plant defence (1)
Faculty / Organisational entity
We present an overview of various learning techniques used in automated theorem provers. We characterize the main problems arising in this context and classify the solutions to these problems from published approaches. We analyze the suitability of several combinations of solutions for different approaches to theorem proving and place these combinations in a spectrum ranging from provers using very specialized learning approaches to optimally adapt to a small class of proof problems, to provers that learn more general kinds of knowledge, resulting in systems that are less efficient in special cases but show improved performance for a wide range of problems. Finally, we suggest combinations of solutions for various proof philosophies.
We present a distributed system, Dott, for approximately solving the Trav-eling Salesman Problem (TSP) based on the Teamwork method. So-calledexperts and specialists work independently and in parallel for given time pe-riods. For TSP, specialists are tour construction algorithms and experts usemodified genetic algorithms in which after each application of a genetic operatorthe resulting tour is locally optimized before it is added to the population. Aftera given time period the work of each expert and specialist is judged by a referee.A new start population, including selected individuals from each expert and spe-cialist, is generated by the supervisor, based on the judgments of the referees.Our system is able to find better tours than each of the experts or specialistsworking alone. Also results comparable to those of single runs can be found muchfaster by a team.
Automatic proof systems are becoming more and more powerful.However, the proofs generated by these systems are not met withwide acceptance, because they are presented in a way inappropriatefor human understanding.In this paper we pursue two different, but related, aims. First wedescribe methods to structure and transform equational proofs in away that they conform to human reading conventions. We developalgorithms to impose a hierarchical structure on proof protocols fromcompletion based proof systems and to generate equational chainsfrom them.Our second aim is to demonstrate the difficulties of obtaining suchprotocols from distributed proof systems and to present our solutionto these problems for provers using the TEAMWORK method. Wealso show that proof systems using this method can give considerablehelp in structuring the proof listing in a way analogous to humanbehaviour.In addition to theoretical results we also include descriptions onalgorithms, implementation notes, examples and data on a variety ofexamples.
The generation of liquid-liquid dispersions with defined droplet size distributions is an important aspect for process equipment design. In this work, two centrifugal pumps with different impeller diameters were used to generate dispersions at selected operating points for a paraffin oil-water system. The droplet break-up phenomena within the centrifugal pumps were analyzed using a transparent pump design in combination with high-speed imaging. Droplet size distributions at centrifugal pump discharge nozzle were recorded with optical probe measurement technologies and evaluated by means of image processing using a neural network. The influence of impeller diameter, rotational speed, volumetric flow rate and dispersed phase fraction are discussed. Experimental data is correlated using fluid properties, operating data as well as centrifugal pump dimensions. The correlations developed from results of this work serve as a basis for the equipment design of centrifugal pumps.
Das Futtersuchverhalten von Blattschneiderameisen (BSA) weist zwei Besonderheiten auf, die bislang nicht mit der Theorie des optimalen Nahrungserwerbs in Übereinstimmung gebracht werden konnten: sie (i) verlassen ihre Nahrungspflanzen frühzeitig bevor diese komplett entlaubt sind und (ii) ernten Bäume in beträchtlicher Distanz , obwohl conspezifische Bäume (mit scheinbar gleicher Blattqualität) näher am Nest liegen. Eine mögliche kausale Erklärung bietet die Hypothese induzierter Pflanzenabwehr (induced-defence hypothesis), durch welche die beobachteten Futtersuchmuster als zeitlich und räumlich dynamisches Mosaik aus induzierter, wenig induzierter und nicht induzierter Pflanzenabwehr in Pflanzenindividuen und Pflanzenteilen zu verstehen wären. In diesem Kontext war es das Ziel meiner Diplomarbeit zu klären ob und mit welcher Wirkung herbivorieinduzierte Pflanzenvolatile (HIPVs) von BSA perzipiert werden. Der Fokus lag dabei auf der jeweils spezifischen Rolle der beiden symbiontischen Partner des BSA-Systems (Ameisen und Pilz) und möglichen Interaktionen zwischen ihnen. Im ersten Untersuchungsabschnitt wurden Atta colombica-Arbeiterinnen in olfaktometrischen Wahlexperimenten mit einzelnen Komponenten und dem naturgetreuen Mix der HIPVs der Limabohne (Phaseolus lunatus) konfrontiert. Da hierbei kein Eintrag induzierter Blätter in die Kolonie stattfand, blieb der symbiotische Pilz unbeeinflusst von den HIPVs. Um andererseits spezifisch die Reaktion des Pilzpartners auf die HIPVs der Limabohne zu beurteilen, wurden Wachstumsassays mit Kulturen des Gartenpilzes Leucoagaricus gongylophorus durchgeführt. Zentrale Ergebnisse meiner Untersuchung waren: (1) BSA-Arbeiterinnen zeigten im Olfaktometer keine Reaktion auf verschiedene Konzentrationen der Limabohnen-HIPVs (Abb. 1); (2) Hingegen konnten für eine Reihe von HIPVs antimykotische Eigenschaften auf den symbiotischen Pilz nachgewiesen werden (Abb. 2). Im Lichte dieser Ergebnisse sind viele bisher publizierte Hinweise auf die repellente Wirkung von HIPV-Komponenten auf BSA-Kolonien/Arbeiterinnen (Aigner 2007, Tremmel 2008) nur dann zu verstehen, wenn man sie als eine nachträgliche, vom symbiotischen Pilz vermittelte‚ verzögerte Ablehnung (so genannte delayed rejection hypothesis, sensu Knapp et al 1990) interpretiert. Pilz-inhibierende Substanzen werden dabei zunächst von BSA- Arbeiterinnen in die Kolonie eingetragen und zu einem späteren Zeitpunkt abgelehnt. Die vorliegende Studie kann somit als Unterstützung der induced-defence hypothesis gelten.