Higher-order modal logic is a framework for modeling a large variety of problems and is applied in philosophy and computer science. Automating reasoning in this framework could be very beneficial. Unfortunately, there exists no software which achieves this. However automatic reasoning tools for higher-order logic do exist and there is a method which allows expressing higher-order model logic in terms of higher-order logic. Hence, the method enables automatic reasoning in the desired logic. In this thesis a tool which converts a higher-order model problem into a higher-order problem by applying this method is devised.

Die Neurorobotik beschäftigt sich mit der Übertragung eines biologischen Gehirns auf ein kleines künstliches Gehirn. Insektengehirne weisen autonome Verhaltensmuster auf, die überraschend komplex sind und verwenden allgemeine Prinzipien der neuronalen Vorgänge, wie dem Lernen.

Es wurde ein Neuronales Netz entworfen, das das assoziierte Lernen simuliert und das untersucht, ob der Roboter, der von diesem Netz gesteuert wird, nach der Konditionierung sein Verhalten bei einem neutralen Reiz ändert. Im Rahmen der Bachelorarbeit wurde untersucht, in wie weit das Neuronale Netz einen neutralen und einen bedingten Reiz paaren kann. Es wurde ein Roboter, den NeuroRover, zur Verfügung gestellt, der vom Simulator gesteuert wird. Der Rover wurde mit der HaViMo2.0 Kamera ausgestattet, die Farben erkennt, so dass der Roboter diese Informationen verarbeiten kann. Mit dem Arduino WiFi-Shield ist eine drahtlose Kommunikation zuwischen dem Neuro-Rover und dem Neuronalen Netz garantiert. Die Simulationssoftware wurde um eine Logging-Funktion erweitert, die jede Aktivität aller Neuronen und Synapsen protokolliert. Der neutrale Reiz ist die von der HaViMo2.0 erkannte Farbe, die rot oder blau ist. Beim bedingten Reiz handelt es sich um eine Bestrafung oder eine Belohnung. Nach zahlreichen Versuchsdurchführungen und Auswertungen konnte das Neuronale Netz zwei Reize miteinander paaren. Ein neutraler Reiz sorgte für eine Verhaltensänderung des NeuroRovers. Bei der Konditionierung veränderten sich die Synapsengewichte so derart, dass ein neutraler Reiz das gleiche Verhalten auslöste wie das gleichzeitige Auftreten zweier gepaarter Reize. Die aufgenommenen Daten bestätigen die Mächtigkeit der Simulation des assoziierten Lernens, sowie die Verhaltensänderungen, die in Form von Aktivitäten von bestimmten Neuronen auftraten.

Freie Logik erweitert Logik um den Aspekt der Nichtexistenz von Objekten und schafft Raum für Undefiniertheit. Logische Schlussfolgerungen über solche nicht-klassischen Logiken können über unkonventionelle Einbettungen in die klassische Logik höherer Stufe gezogen werden. Automatische Beweiser für höherstufige Logik sezen auf die TPTP-Sprache THF, eine standardisierte Kodierung für Formeln der Logik höherer Stufe. In dieser Arbeit wurde eine TPTP-konforme Kodierung für die nicht-klassische freie Logik entworfen sowie die Einbettung von freier Logik in Logik höherer Stufe implementiert. Ziel der Arbeit war es, die native Formulierung von Formeln der freien Logik zu ermöglichen, für deren Auswertung aber trotzdem auf die Fertigkeiten von namhaften höherstufigen Theorembeweisern wie Leo-II(I) ausgewichen wird.

Die Effektivität der Übersetzung wurde anhand beispielhafter Formalisierungen untersucht. Ansatzpunkt dafür bildete das kategorientheoretische Buch Categories, Allegories von Freyd und Scedrov (1990).

Das BeesBook Projekt beschäftigt sich mit der Langzeitanalyse des Kommunikationsverhaltens von Bienen. Dazu werden Bienen auf einer Wabe eindeutig  identifiziert und ihre Bewegung mit Hilfe mehrerer Kameras erfasst. Zwei hochauflösende Kameras nehmen jeweils eine Wabenseite auf, wobei stets eine Kamera eine Wabenhälfte erfasst. Die Positionen der Bienen werden dann in Relation  zum Bild einer Wabenhälfte bestimmt. Für die weitere Analyse ist es erforderlich, dass die Position in Relation zu einem Gesamtbild einer Wabenseite beschrieben werden kann. Diese Arbeit entwickelt daher Lösungen, welche es ermöglichen, die Korodinaten aus den Bildern der Wabenhälften in ein Gesamtkoordinatensystem zu überführen.

In der Humanoid Kid-Size League des RoboCups werden im Moment Spiele über ein WLAN-Signal gestartet. In Zukunft soll das durch eine Trillerpfeife geschehen. Problem in diesem Szenario ergeben sich vor allem durch die geforderte Erkennung in Echtzeit und dem Level an Hintergrundlärm beim RoboCup. In dieser Arbeit wird ein Verfahren vorgestellt, das auf Basis des Obertonspektrums den Klang mehrerer Trillerpfeifen generalisiert, bei gleichzeitiger Berücksichtigung der Anforderungen. Das Verfahren wurde in C++ implementert und auf den FUmanoids getestet.

The automatic detection of emotions in faces plays an increasing role in todays life. The goal of this work is to provide a simple and flexible Framework for Action Unit detection with Support Vector Machines. Therefore, I present the project for which this  framework was made, a short overview of the theories used, the database used for training, the created framework, including landmark estimation and normalization, feature extraction, training Support Vector Machines and predicting Action Units with them.

Computer vision aims to reconstruct high-level information from raw image data e.g. the pose of an object. Deep Convolutional Neuronal Networks (DCNN) are showing remarkable performance on many computer vision tasks. As they are typically trained in a supervised setting and have a large parameter space, they require large sets of labeled data. The costs of annotating data manually can render DCNNs infeasible. I present a novel framework called RenderGAN that can generate large amounts of realistic labeled images by combining a 3D model and the Generative Adversarial Network (GAN) framework. In my approach, the distribution of image deformations (e.g. lighting, background, and detail) is learned from unlabeled image data to make the generated images look realistic. I evaluate the RenderGAN framework in the context of the BeesBook project, where it is used to generate labeled data of honeybee tags. A DCNN trained on this generated dataset shows remarkable performance on real data.

Das Toreschießen ist die Kernkompetenz der Fußballroboter. Dafür müssen die Roboter sich stabil bewegen und ihre Umgebung visuell wahrnehmen können - jeder der Roboter muss den Ball und das Tor erkennen. Aus den Kameradaten, die der Roboter von einer gewöhnlichen Webcam bekommt, wird eine Klassifizierung nach grünem Rasen, weißen Linien, Toren und einem teilweise weißen Ball und den übrigen Objekten durchgeführt. Im Falle von Sonneneinstrahlung auf einem Teil des Spielfelds oder sich plötzlich ändernder Lichtbedingungen während eines Spiels ist diese Klassifizierung jedoch nicht mehr brauchbar. Um zukünftig auch unter sich verändernden Lichtbedingungen spielen zu können, müssen die Charakteristika der Kameras bekannt sein. Bei den aktuellen - und allen vorherigen - Implementierungen der Bildverarbeitung wird nicht auf veränderliches Licht reagiert.

Durch ein Experiment, in dem eine statische Szene mit verschiedenen Anteilen  von rotem, grünem und blauem Licht beleuchtet wird, soll gezeigt werden, inwiefern sich der Farbraum bei einer Änderung der Lichtfarbe verändert und wie stark dies von den Farben und Objekten abhängt. Eine Kamerakennlinie gibt an, wie die eigentliche Beleuchtung der Szene von der Kamera abgebildet wird. Sie kann mit verschiedenen Verfahren berechnet werden, unter anderem durch eine Methode, die einige verschieden beleuchtete Bilder derselben Szene benutzt. In dieser Bachelorarbeit wird ein Experiment vorgestellt und ausgewertet sowie ein Verfahren zur Berechnung der Kamerakennlinie aus den durch das Experiment gewonnenen Daten präsentiert und das Ergebnis dargelegt.

With the augmenting variety of platforms on the market, supporting as many of them became an inevitable obstacle to confront in order to reach as many users as possible. Platforms support different native languages, such as Java for Android or Objective-C for iOS. The most straight-forward way to support both of these platforms is to produce native codes for each of them, which is greatly cost and time consuming.

There are several tools to avoid programming in the native languages of targeted platforms and to achieve cross-platform programming, but using them generally results in a performance loss. For video games, such a loss can be critical, which is why native programming is favored in order to get the best performance possible from the targeted platforms.

In this paper we investigate the productivity and efficiency of cross-platform programming with Haxe by reimplementing essential OpenGL features while targeting two platforms at the same time, Android and Windows.

The result of our research showed that, while the consumed time in programming cost trivially less effort than native coding on each of the different platforms, Haxe did not engender any significant performance loss.

To deepen this investigation, expanding the scenes' complexity or making an actual game would put the devices to test in more extreme conditions.

Zum 75. Jubiläum der "Z3" von Konrad Zuse habe ich mich mit einer seiner weniger bekannten Erfindungen befasst und eine schematische Darstellung der "logistischen Maschine" animiert.

Meine Simulation wurde in Python mit Hilfe der GUI-Bibliothek  "TkInter" erstellt und imitiert das Original in so weit, dass man das Verhalten der wichtigen Bauteile nachvollziehen kann.

Das Programmm wird im September 2016 im Rahmen des Heidelberg Laureate Forums ausgestellt und soll dem Zuschauer die Funktionsweise der Maschine verständlich machen.

Das Interesse an der Darstellung von großen Punktwolken ist durch das Aufkommen von günstigen 3D-Scannern und der 3D-Rekonstruktion in den letzten Jahrzehnten stark gewachsen. Aufgrund der technologischen Entwicklungen in diesem Bereich ist es möglich von kleinen Objekten, wie einem Dinosaurierschädel bis hin zu ganzen Städten, Modelle in hoher Detailstufe digital zu erfassen. In der Denkmalpflege werden Objekte mittlerweile aus Routine abgescannt und archiviert.

Für gewöhnlich sind die erzeugten Modelle enorm groß und daher nicht ohne weiteres darstellbar. Die Modelle bestehen meist aus einer ungeordneten Sammlung von dreidimensionalen Punkten mit Farbinformationen. Desktop-Lösungen verlassen sich zur Lösung des Problems auf Level-of-Detail (LOD) Konzepte kombiniert mit Out-of-core Verfahren und klugen Caching  Strategien, um der hohen Datenmenge Herr zu werden. Durch das Aufkommen von leistungsstarken Smartphones entstand eine neue Plattform zum Darstellen von Modellen.

Daraus entstand eine Nachfrage durch Forschungsgruppen für eine mobile Applikation zum Betrachten großer Modelle. Die Applikation kann beispielsweise bei 3D-Rekonstruktion schnelles Feedback liefern, vereint mt den Vorzügen eines mobilen Gerätes. Dadurch können schnell unvollständige oder schwer zu erfassende Bereiche des Modells beim Scannen erkannt werden. Des Weiteren kann die Applikation zur Präsentation von Modellen  eingesetzt werden.

Die Herausforderung bestand darin, trotz der Limitierungen eines Tablets durch seinen geringen Arbeitsspeicher und der relativ schwachen GPU, Punktwolken mit mehreren Millionen Punkten flüssig darzustellen. Dabei sollte es möglich sein,  jederzeit neue Punkte in die bestehende Darstellung hinzuzufügen. Zur Zeit existieren nur bedingt geeignete Softwarelösungen für das Problem.

Humanoide Roboter sind Maschinen, die ihre Umwelt wahrnehmen und mit ihr interagieren können. Dabei sind sie dem menschlichen Körperbau nachempfunden: Ihr Körper gliedert sich in einen Rumpf mit Kopf, zwei Beinen und Armen. Im Gegensatz zum Menschen kann ein Roboter allerdings auf eine größere Auswahl an Sensoren zurückgreifen, um Informationen über seine Umwelt zu erhalten. Eine wichtige Rolle spielen dabei Kameras. Sie bieten den Vorteil, sehr schnell und berührungslos viele Details aufnehmen zu können.  Gerade im kompetitiven Umfeld des Roboterfußballs ist es ein essentieller Vorteil, eine dem Gegner überlegene Bildverarbeitung zu besitzen, die sich an die immer wieder ändernden Herausforderungen anpassen kann. Dabei verbieten die Regeln den Einsatz aktiver Sensoren wie z.B. die Mikrosoft Kinect Tiefenkamera, LIDAR und Ultraschall, so dass für das Sammeln von Tiefeninformationen passive Sensoren, wie z.B. eine Stereokamera, eingesetzt werden müssen.

Konrad Zuses logistische Maschine ist ein sehr einfacher, arithmetisch vollständiger Relaiscomputer, dessen Prozessor beispielsweise aus nur fünf Relais besteht. Im Rahmen dieser Arbeit wurde eine interaktive Simulation entwickelt, die diese Maschine in Aktion zeigt. Die Visualisierung ist geeignet, um Laien zu demonstrieren, wie aus dem zusammenspiel weniger, leicht zu verstehender Bauteile ein programmierbarer Computer wird.

------------------

Konrad Zuse's "logistische Maschine" (logical machine) is a very simple but arithmetically complete electromechanical computer, for instance having a processor consisting of only five relays. In this paper an interactive simulation was developed showing this machine in action. The visualisation is particularly suited for demonstrating to laymen how the interaction of only a few simple-to-understand components bears the power of a programmable computer. 

Der SpaceBot Cup ist ein Wettbewerb des Deutschen Luft- und Raumfahrtzentrums. In einer simulierten Raumfahrtmission sollen robotische Systeme ihre Fähigkeiten der autonomen Exploration unter Beweis stellen.

Die Navigation in unbekanntem Gelände spielt dabei eine zentrale Rolle, damit der Roboter sich sicher autonom bewegen kann. Hierfür muss das Simultaneous Localization and Mapping (SLAM) Problem gelöst werden. Der Roboter muss eine Karte seiner Umgebung erstellen und sich gleichzeitig in dieser lokalisieren.

Ein Team aus Studierenden der Freien Universität Berlin hat innerhalb der Arbeitsgruppe Intelligente Systeme und Robotik einen Roboter entwickelt und programmiert um sich den Herausforderungen des SpaceBot Cup zu stellen.

Diese Arbeit beschreibt die Entwicklung eines SLAM-Algorithmus mittels eines Laserscanners. Es wurde der Iterative Closest Point SLAM-Algorithmus mithilfe der Mobile Robot Programming Toolkit Softwarebibliothek implementiert und in das Robot Operating System Framework integriert.

Wenn eine Honigbiene eine Futterquelle gefunden und sie ausgebeutet hat und anschließend in den Bienenstock zurückkehrt, teilt sie ihren Artgenossinnen in einem besonderen Kommunikationsprozess, dem Bienentanz, Informationen wie die Entfernung, die Flugrichtung, sowie die Qualität der Futterquelle mit. Nach kurzer Zeit begeben sich weitere Bienen zu der beschriebenen Nahrungsquelle.

Frühere Forschungsergebnisse lassen darauf schließen, dass bei naheliegenden Futterquellen (in einem Umkreis von maximal einem Kilometer) die Abweichung von der erwarteten Tanzrichtung bei den Schwänzelläufen größer ist bzw. die Tanzrichtung ungenauer ist, als bei weiter entfernten Futterquellen. Ebenso ließ sich in einem Tanzparameter, der Frequenz des Schwänzellaufs, individuelle Variabilität nachweisen. Es ergibt sich daraus die Frage, ob bei der Genauigkeit der Richtungsweisung im Bienentanz es ebenfalls konsistente Unterschiede zwischen den Individuen gibt. Es wurden dazu die analysierten Videoaufnahmen vom 20.08. bis zum 22.08.2008 von Tim Landgraf et. al. (2011) genutzt, die Informationen über die Position und den Winkel beinhalten, wie eine Biene sich zu einem Schwänzellauf verhält. Nachdem zu jedem Tanz die Abweichung nach links, rechts und insgesamt, sowie der aufgespannte Winkel zwischen linker und rechter Abweichung berechnet wurde, stellte sich ebenfalls die Frage, ob feste Effekte wie der Tag, die Temperatur, die Uhrzeit und die Anzahl der Schwänzelläufe die Genauigkeit der Richtungsweisung beeinflussen. Es kam einmal heraus, dass für die Abweichung nach links, rechts und insgesamt konsistente Unterschiede in der Genauigkeit der Richtungsweisung existierten und somit individuelle Variabilität nachzuweisen war, die möglicherweise auf Faktoren wie die Erfahrung, das Alter und die Morphologie einer Biene zurückzuführen ist.

Ebenso zeigte sich eine leichte Abhängigkeit zwischen der gesamten Abweichung und der Uhrzeit. Aus den Analysen war ebenfalls festzustellen, dass der abweichende Tanzwinkel nach links und rechts im Verhältnis fast gleich groß war und sich somit daraus schließen lässt, dass Bienen gewollt einen kleinen bzw. großen Abweichungswinkel in beide Richtungen tanzen. Um die Daten zu verifizieren, sollte das Projekt wiederholt werden, wobei einmal das Tracking-Programm, welches die Videoaufnahmen analysierte, überprüft werden sollte, sowie Daten aus einem größeren Zeitraum ausgewertet werden sollten. Ebenso sollten für die genaue Identifikation von konsistenten Unterschieden in der Genauigkeit der Richtungsweisung Faktoren wie das Alter, die Morphologie und die Erfahrung bei der Futtersuche, sowie die genaue Orientierung, die die Bienen auf der Wabe präferieren, miteinbezogen werden.

Video tracking aids users in various domains. In medicine, it plays an increasingly important role in assisting clinicians in diagnosis while in arts image processing helps Special Effects technicians in applying visual effects to movies. Another area of application is surveillance where real-time video tracking enables security personnel to monitor a large set of video collectors. The Biorobotics Lab profits greatly from computer vision and realized that many parts of vision applications can be reused for future projects to reduce programming overhead. Functions, that are useful, regardless of the computer vision task, include loading and decoding videos, the interaction with image and video data, like pausing, panning and zooming, and means to serialize trajectory data. This motivated the BioTracker, a modular open source c++ framework for computer vision applications. However, the application still experiences a number of issues and inconveniences. For example, it cannot be embedded into other programs or used in automated environments like servers and super computers. Furthermore, extending the application with new computer vision algorithms is unintuitive and error-prone. This thesis restructures the BioTracker to tackle the aforementioned problems and furthermore introduces a novel technique to bring scriptability to the application using 0mq, a high performance messaging queue, to greatly simplify the creation of new tracking modules. The new BioTracker framework enables users to apply general purpose computer vision and image processing techniques to any type of domain, not limited to Biology.

Honigbienen benutzen den Schwänzeltanz, um anderen Bienen mitzuteilen wo Futterstellen sind. Diesen Tanz automatisiert zu erkennen, ist eine schwere Aufgabe für die es bereits einige Systeme gibt. Eines dieser Systeme, der Waggle Dance Detector, bietet eine automatisierte Echtzeiterkennung von Schwanzeltänzen. In dieser Arbeit wird die Erkennungsrate des Waggle Dance Detectors mit Hilfe eines Convolutional Neuronal Networks verbessert. Dazu werden die Ergebnisse des Waggle Dance Detectors im Zuge eines Nachbearbeitung-Schrittes nochmals klassifiziert, um falsch erkannte Tänze heraus zu filtern.

Im Rahmen des Projekts BeesBook wurden über 370 TB an  Bildmaterial von Honigbienenkolonien auf dem Supercomputer des HLRN (Norddeutscher Verbund für Hoch- und Höchstleistungsrechnen) ausgewertet. Diese Arbeit entwickelt eine Software, die die Ergebnisse von dem Supercomputer in eine Datenbank überführt. Damit die Daten schnell in Datenbank gespeichert werden können, wurde den gesamten Ablauf in kleinere und von einander unabhängige Komponente zerlegt. Das ermöglicht eine parallele Ausführung aller Komponente. Des Weiteren wurde die Datenbank zur Verhaltensanalyse von Honigbienenkolonien konzipiert.