102 Publikation(en)

Automatic detection and decoding of honey bee waggle dances

Fernando Wario, Ben Wild, Raúl Rojas, Tim Landgraf

arXiv | 2017-12

Erschienen in: PLOS One


PLOS onearXiv-linkpdf-Datei

Thema: Computer Vision, Pattern Recognition; Quantitative Methods

Logistic Regression as Soft Perceptron Learning

Raúl Rojas

arXiv | 2017-08

Erschienen in: Cornell University Library


We comment on the fact that gradient ascent for logistic regression has a connection with the perceptron learning algorithm. Logistic learning is the "soft" variant of perceptron learning.

Deepest Neural Networks

Raúl Rojas

arXiv | 2017-07

Erschienen in: Cornell University Library


This paper shows that a long chain of perceptrons (that is, a multilayer perceptron, or MLP, with many hidden layers of width one) can be a universal classifier. The classification procedure is not necessarily computationally efficient, but the technique throws some light on the kind of computations possible with narrow and deep MLPs.

Thema: Neural Networks, Neural and Evolutionary Computing, Learning

Stable Timed Elastic Bands with Loose Ends

Fritz Ulbrich , Daniel Göhring, Tobias Langner, Zahra Boroujeni, Raúl Rojas

IEEExplore | 2017-06

Erschienen in: Proceedings of the IEEE Intelligent Vehicles Symposium (IV), June 11-14, 2017, Redondo Beach, CA, USA

ManuskriptIEEE link

In this paper we propose a trajectory planning approach for autonomous vehicles in highly dynamic traffic scenarios, capable of exploiting the observed trajectories of other vehicles. For this purpose, we introduce a novel variant of the timed elastic bands (TEB) approach by using fixed time intervals and a flexible goal position. We tested our method with a simulated merge-into-traffic scenario and compare it to a reference TEB implementation with focus on the impact of important parameters and the stability of planned trajectories. The results show that our method is an improvement over TEB in terms trajectory smoothness and stability.

Thema: Trajectory, Planning, Vehicle dynamics, Acceleration, Linear programming, Optimization

Capability Discovery for Automated Reasoning Systems

Alexander Steen, Max Wisniewski, Hans-Jörg Schurr, Christoph Benzmüller

EasyChair | 2017-06

Erschienen in: Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21, Kalpa Publications in Computing, Vol. 1.


Automated reasoning systems such as theorem provers often employ interaction or cooperation with further reasoning software. Whereas in most cases the concrete choice of cooperating software is, to some extent, irrelevant, these systems are nevertheless often rigid in practice due to compatibility issues. In order to support more flexible cooperation schemes, a machine-readable description format for automated reasoning systems' capabilities is proposed. Additionally, a simple HTTP-based protocol for system and capability discovery is outlined. Both the format and the protocol are designed to be simple, extensible and easy to use with none to minor modifications for existing reasoning systems.

Computer-assisted Assessment of Lowe's Model Ontological Argument

Christoph Benzmüller, David Fuenmayor, Alexander Steen, Max Wisniewski

Erschienen in: Handbook of the 2nd World Congress on Logic and Religion, Warsaw, Poland


Going Polymorphic - TH1 Reasoning for Leo-III

Alexander Steen, Max Wisniewski, Christoph Benzmüller

EasyChair | 2017-06

Erschienen in: Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Kalpa Publications in Computing, Vol. 1, 2017


While interactive proof assistants for higher-order logic (HOL) commonly admit reasoning within rich type systems, current theorem provers for HOL are mainly based on simply typed lambda-calculi and therefore do not allow such flexibility. In this paper, we present modifications to the higher-order automated theorem prover Leo-III for turning it into a reasoning system for rank-1 polymorphic HOL. To that end, a polymorphic version of HOL and a suitable paramodulation-based calculus are sketched. The implementation is evaluated using a set of polymorphic TPTP THF problems.

Online vehicle detection using Haar-like, LBP and HOG feature based image classifiers with stereo vision preselection

Daniel Neumann, Tobias Langner, Fritz Ulbrich , Daniel Göhring, Dorothee Spitta

IEEExplore | 2017-06

Erschienen in: Proceedings of the IEEE Intelligent Vehicles Symposium (IV) June 11-14, 2017, Redondo Beach, CA, USA

ManuskriptIEEE link

Environment sensing is an essential property for autonomous cars. With the help of sensors, nearby objects can be detected and localized. Furthermore, the creation of an accurate model of the surroundings is crucial for highlevel planning. In this paper, we focus on vehicle detection based on stereo camera images. While stereoscopic computer vision is applied to localize objects in the environment, the objects are then identified by image classifiers. We implemented and evaluated several algorithms from image based pattern recognition in our autonomous car framework, using HOG-, LBP-, and Haar-like features. We will present experimental results using real traffic data with focus on classification accuracy and execution times.

Thema: Feature extraction, Cameras, Stereo vision, Automobiles, Three-dimensional displays, Sensors, Vehicle detection

Types, Tableaus and Gödel's God in Isabelle/HOL

Christoph Benzmüller, David Fuenmayor

Erschienen in: Archive of Formal Proofs, 2017


A computer-formalisation of the essential parts of Fitting's textbook "Types, Tableaus and Gödel's God" in Isabelle/HOL is presented. In particular, Fitting's (and Anderson's) variant of the ontological argument is verified and confirmed. This variant avoids the modal collapse, which has been criticised as an undesirable side-effect of Kurt Gödel's (and Dana Scott's) versions of the ontological argument. Fitting's work is employing an intensional higher-order modal logic, which we shallowly embed here in classical higher-order logic. We then utilize the embedded logic for the formalisation of Fitting's argument. (See also the earlier AFP entry ``Gödel's God in Isabelle/HOL''

Dancing attraction: followers of honey bee tremble and waggle dances exhibit similar behaviors

Tim Landgraf, Calvin Lam, Yanlei Li, James Nieh

The Company of Biologists Ltd. | 2017-05


The function of the honey bee tremble dance and how it attracts signal receivers is poorly understood. We tested the hypothesis that tremble followers and waggle followers exhibit the same dance following behavior. If correct, this would unify our understanding of dance following, provide insight into dance information transfer, and offer a way to identify the signal receivers of tremble dance information. Followers showed similar initial attraction to and tracking of dancers. However, waggle dancers were faster than tremble dancers, and follower forward, sideways, and angular velocities were generally similar to the velocities of their respective dancers. Waggle dancers attracted followers from 1.3-fold greater distances away than tremble dancers. Both follower types were attracted to the lateral sides of dancers, but tremble followers were more attracted to the dancer's head, and waggle followers were more attracted to the dancer's abdomen. Tremble dancers engaged in 4-fold more brief food exchanges with their followers than waggle dancers. The behaviors of both follower types are therefore relatively conserved. Researchers can now take the next steps, observing tremble followers to determine their subsequent behaviors and testing the broader question of whether follower attraction and tracking is conserved in a wide range of social insects.

Thema: Apis mellifera, foraging communication, signaling, colony organization, division of labor

Universal Reasoning, Rational Argumentation and Human-Machine Interaction

Christoph Benzmüller

Cornell University Library | 2017-03

Erschienen in: arXiv

cite as: arXiv:1703.09620


Classical higher-order logic, when utilized as a meta-logic in which various other (classical and non-classical) logics can be shallowly embedded, is well suited for realising a universal logic reasoning approach. Universal logic reasoning in turn, as envisioned already by Leibniz, may support the rigorous formalisation and deep logical analysis of rational arguments within machines. A respective universal logic reasoning framework is described and a range of exemplary applications are discussed. In the future, universal logic reasoning in combination with appropriate, controlled forms of rational argumentation may serve as a communication layer between humans and intelligent machines.

Thema: Classical higher-order logic, Artificial Intelligence

The Ontological Model Collapse as a Collapse of the Square of Opposition

Christoph Benzmüller, Bruno Woltzenlogel Paleo

Springer International Publishing | 2017-01

Erschienen in: The Square of Opposition: A Cornerstone of Thought


Thema: Model Logics, Higher-Order Logics, Ontological Argument, Interactive and Automated Theorem Proving

Die Computerprogramme von Charles Babbage

Raúl Rojas

Erschienen in: Informatik Spektrum, Springer Verlag Berlin Heidelberg


Der britische Mathematiker und Erfinder Charles Babbage hat von 1836-1841 bis zu 26 Programme für die nie zu Ende gebaute "Analytische Maschine" niedergeschrieben. In diesem Beitrag leiten wir die Programmarchitektur des mechanischen Computers aus dem von Babbage hinterlassenen Code ab.

Thema: Babbage, Rechenmaschinen, Computerprogramme

Computer-Assisted Analysis of the Anderson-Hájek Controversy

Christoph Benzmüller, Leon Weber, Bruno Woltzenlogel-Paleo

Springer International Publishing | 2017

Erschienen in: Logica Universalis, volume 11, number 1.

Bibtex entry URL: bibtexbrowser.local.php?key=J32&bib=chris.bib


We present an exemplary study in Computational Methaphysics, which is an emerging, interdisciplinary field aiming at the rigorous formatlisation and deep Logical assessment of rational, philosophical arguments on the Computer. The particular focus here is on the ontological argument for the existence of God. While related work has concentrated on Anselm's simpler original version of the ontological argument and formalized it in classical predicate logic, we here focus on modern variants of Kurt Gödel's seminal contribution requiring higher-prder modal logic.

Pole-based Localization for Autonomous Vehicles in Urban Scenarios

Daniel Göhring, Raúl Rojas, Robert Spangenberg

IEEE Xplore | 2016-12

Erschienen in: Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) 2016.


Localization is a key capability for autonomous vehicles especially in urban scenarios. We propose the use of pole-like landmarks as primary features in these environments, as they are distinct, long-term stable and can be detected reliably with a stereo camera system. Furthermore, the resulting map representation is memory efficient, allowing for easy storage and on-line updates. The localization is performed in real-time by a stereo camera system as a main sensor, using vehicle odometry and an off-the-shelf GPS as secondary information sources. Localization is performed by a particle filter approach, coupled with an Kalman filter for robustness and sensor fusion. This leads to a lateral accuracy below 20 cm in various urban test areas. The system has been included in our autonomous test vehicle and successfully demonstrated the full loop from mapping to autonomous driving.

Thema: Vehicles, Cameras, Global Positioning System, Atmospheric measurements, Particle measurements, Kalman filters, Robustness

TPTP And Beyond: Representation of Quantified Non-Classical Logics

Christoph Benzmüller, Max Wisniewski, Alexander Steen

Erschienen in: Proceedings of the 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016).


The practical employment of automated deduction systems requires the user to input problem statements in a well-formed string representation. While this presentation is usually fixed by the respective system, the various language dialects of the TPTP library are meanwhile accepted as a de-facto standard for all current automated theorem provers based on classical logics. In the context of reasoning in non-classical logics, however, only a few limited standardization approaches exist, with QMLTP being the most notable exception. To move standardization forward, we outline conservative extensions to the TPTP language that allow systematic syntax definitions for various expressive, non-classical logics. These logics include higher-order versions of modal logics, conditional logics, hybrid logics, free logics, and many-valued logics. We are convinced that a standard syntax for prominent non-classical logics will not only facilitate their deployment but also support the development and comparibility of corresponding theorem proving systems.

RenderGAN: Generating Realistic Labeled Data

Tim Landgraf, Leon Sixt, Benjamin Wild

arXiv preprint arXiv:1611.01331 | 2016-11-04


Deep Convolutional Neuronal Networks (DCNNs) are showing remarkable performance on many computer vision tasks. Due to their large parameter space, they require many labeled samples when trained in a supervised setting. The costs of annotating data manually can render the use of DCNNs infeasible. We 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 framework. In our approach, image augmentations (e.g. lighting, background, and detail) are learned from unlabeled data such that the generated images are strikingly realistic while preserving the labels known from the 3D model. We apply the RenderGAN framework to generate images to barcode-like markers that are attached to honeybees. Training a DCNN on data generated by the RenderGAN yields considerably better performance than training it on various baselines.

The Use of a Multi-Display System in University Classroom Lectures

Raúl Rojas, Margarita Esponda, Bingyi Cao

Erschienen in: Proceedings of the 2016 ACM Conference on Interactive Surfaces and Spaces (ISS 2016)

ManuskriptACM link

We have built a display wall system with four liquid crystal displays to provide a very large visual area for university lectures. A program was developed to transform the display wall into an electronic blackboard. It has been used in a long-term classroom practice. Based on the research results, we demonstrate the benefits of the digital multi-display system for classroom learning.

Thema: Multi-Display; Classroom Lectures; Electronic Blackboard

Axiomatizing Category Theory in Free Logic

Christoph Benzmüller, Dana Scott

Erschienen in: Cornel University Library

arXiv:1609.01493v3 [cs.LO]


Starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. Our axiom sets have been formalized in the Isabelle/HOL interactive proof assistant, and this formalization utilizes a semantically correct embedding of free logic in classical higher-order logic. The modeling and formal analysis of our axiom sets has been significantly supported by series of experiments with automated reasoning tools integrated with Isabelle/HOL. We also address the relation of our axiom systems to alternative proposals from the literature, including an axiom set proposed by Freyd and Scedrov for which we reveal a technical issue (when encoded in free logic where free variables range over defined and undefined objects): either all operations, e.g. morphism composition, are total or their axiom system is inconsistent. The repair for this problem is quite straightforward, however.

Thema: Logic in Computer Science; Artificial Intelligence; Category Theory; Logic

Online Vehicle Detection using Deep Neural Networks and Lidar based Preselected Image Patches

Stefan Lange, Fritz Ulbrich, Daniel Goehring

IEEE Xplore | 2016-08-08

Erschienen in: Proceedings of the 2016 IEEE Intelligent Vehicles Symposium (IV16).


In this paper we present a vehicle detection system using convolutional neural networks on 2d image data. Since realtime capabilities are crucial for object detection systems running in real-traffic situations, we will show how the calculation time of our algorithm can be significantly reduced by taking advantage of depth information from lidar sensors. One part of this work focusses on useful network topologies and network parameters to increase the classification precision. We will test the presented algorithm on an autonomous car in different real-traffic scenarios with regards to detection accuracy and calculation time and show experimental results.

Thema: Training, Laser radar, Vehicles, Sensors, Cameras, Neurons

Optimizing a driving strategy by its sensor coverage of relevant environment information

Raúl Rojas, Steffen Heinrich, Jannes Stubbemann

IEEE Xplore | 2016-08-08

Erschienen in: Proceedings of the Intelligent Vehicles Symposium (IV), 2016 IEEE; Gothenburg, Sweden.


We propose a novel approach for automated vehicle motion planning systems that introduces the likelihood of an information gain at future positions to trajectory optimization. In the same way as human drivers, computer controlled vehicles have to be fully aware of their surroundings and the current driving situation. Even though automated cars have a full 360 degrees field of view through sensor data fusion, objects can be hidden behind other obstacles. We optimize the vehicle's future pose (position and orientation) on the road and within the traffic stream, so that it can perceive as much as possible while fulfilling other constraints related to the overall safety or driving comfort. Our results show that perception benefits from maximizing the entropy in areas of interest (EAI) over field of view (FOV). The computation of an EAI is expensive and achieved by using an optimized algorithm for modern GPGPUs.

Thema: Roads, Automobiles, Planning, Robot sensing systems, Entropy, Trajectory

Babbage meets Zuse: A Minimal Mechanical Computer

Raúl Rojas

Springer International Publishing Switzerland | 2016-07

Erschienen in: Proceedings of the 15th International Conference, UCNC 2016, Manchester, UK, July 11-15, 2016. Lecture Notes of Computer Science 9726.


Chemical Reaction Networks (CRNs) model the behavior of molecules in a well-mixed solution. The emerging field of molecular programming uses CRNs not only as a descriptive tool, but as a programming language for chemical computation. Recently, Chen, Doty and Soloveichik introduced rate-Independent continuous CRNs (CCRNs) to study the chemical computation of continuous functions. A fundamental question for any CRN model is reachability, the question whether a given target state is reachable from a given start state via a sequence of reactions (a path) in the network. In this paper, we investigate CCRN-REACH, the reachability problem for rate-independent continuous chemical reaction networks. Our main Theorem is that, for CCRNs, deciding reachability - and constructing a path if there is one - is computable in polynomial time. This contrasts sharply with the known exponential space hardness of the reachability problem for discrete CRNs. We also prove that the related problem Sub-CCRN-REACH, which asks about reachability in a CCRN using only a given numer of its reactions, is NP-complete.

Thema: Babbage, Zuse, minimal computer

Cut-Elimination for Quantified Conditional Logic

Dr. C. Benzmüller

Erschienen in: Journal of Philosophical Logic


A semantic embedding of quantified conditional logic in clasical higher-order logic is utilized for reducing cut-elimination in the former logic to existing results for the latter logic. The presented embedding approach is adaptable to a wide range of other logics, for many of which cut-elimination is still open. However, special attention has to be paid to cut-simulation which may render cut elimination as a pointless criterion.

Thema: cut-elimination; quantified conditional logics; classical higher-order logic; semantic embedding; cut-simulation

Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic

Dr. C. Benzmüller, A. Steen, Dr. C. Benzmüller

Erschienen in: Journal of Logic and Logical Philosophy; Vol 25, No 2 (2016): June 2016

Journal linkManuskript

An embedding of many-valued logics based on SIXTEEN in classical higher-order logic is presented. SIXTEEN generalizes the four-valued set of truth degrees of Dunn/Belnap’s system to a lattice of sixteen truth degrees with multiple distinct ordering relations between them. The theoretical motivation is to demonstrate that many-valued logics, like other non-classical logics, can be elegantly modeled (and even combined) as fragments of classical higher-order logic. Equally relevant are the pragmatic aspects of the presented approach: interactive and automated reasoning in many-valued logics, which have broad applications in computer science, artificial intelligence, linguistics, philosophy and mathematics, become readily enabled with state of the art reasoning tools for classical higher-order logic.

Thema: many-valued logic; non-classical logic; higher-order logic; automated theorem proving; semantic embedding; automation; meta-logical reasoning

Extracting Path Graphs from Vehicle Trajectories

Fritz Ulbrich, Simon Rotter, Daniel Goehring, Raúl Rojas

Erschienen in: 2016 IEEE Intelligent Vehicles Symposium June 19-22, Gothenburg, Sweden.


In this paper we present an approach for building a graph of drivable paths from the reconstructed trajectories of vehicles detected by lidar and radar sensors mounted in an autonomous car. The perceived objects are tracked, and their trajectories are merged, clustered and labeled with meta information. A graph of the underlying road infrastructure can be generated with this information. We report on the results of testing the validity and accuracy of the method. The generated path graph can be used either to update high precision maps or for generating local temporary maps, both of them useful for autonomous driving.

Thema: Situation Analysis and Planning, Mapping and Localization, Self-Driving Vehicles

Traffic Awareness Driver Assistance based on Stereovision, Eye-tracking, and Head-Up Display

Tobias Langner, Daniel Seifert, Bennet Fischer, Daniel Goehring, Tinosch Ganjineh, and Raúl Rojas

IEEE Xplore | 2016-05

Erschienen in: Proceedings of the 2016 IEEE International Conference on Robotics and Automation (ICRA), Stockholm, Sweden, May 16-21, 2016.


This paper presents a system which constantly monitors the level of attention of a driver in traffic. The vehicle is instrumented and can identify the state of traffic-lights, as well as obstacles on the road. If the driver is inattentive and fails to recognize a threat, the assistance system produces a warning. Therefore, the system helps the driver to focus on crucial traffic situations. Our system consists of three components: computer vision detection of traffic-lights and other traffic participants, an eye tracking device used also for head localization, and finally, a human machine interface consisting of a head-up display and an acoustic module used to provide warnings to the driver. The orientation of the driver's head is detected using fiducial markers visible in video frames. We describe how the system was integrated using an autonomous car as experimental ADAS platform.

Thema: traffic awareness, stereovision, eye-tracking, head-up display

Development and Evaluation of a Classroom Interaction System

Raúl Rojas, Bingyi Cao, Margarita Esponda

Erschienen in: Proceedings of the 12th International Conference Mobile Learning, April 2016, Algarve, Portugal


In order to reduce the passivity of students and enhance their learning experience in large lectures, we developed a browser-based tool called Classroom Interacter to promote classroom interaction. It allows students to use their own mobile devices to participate in the learning process. The main Features of Classroom Interacter include live voting, status setting and question sending. The evaluation results showed that students were satisfied with the usability and felt it was helpful for their study. Although distraction was reported by some students, the system received very positive evaluations. Most students showed their willingness to use Classroom Intracter in the future.

Thema: Classroomm interaction, mobile device, voting, usability

The Design Principles of Konrad Zuse’s Mechanical Computers

Raúl Rojas

Cornell University Library | 2016-03



Konrad Zuse built the Z1, a mechanical programmable computing machine, between 1935/36 and 1937/38. The Z1 was a binary floating-point computing device. The individual logical gates were constructed using metallic plates and interconnection rods. This paper describes the design principles Zuse followed in order to complete a complex calculating machine, as the Z1 was. Zuse called his basic switching elements "mechanical relays" in analogy to the electrical relays used in telephony.

RoboFish: increased acceptance of interactive robotic fish with realistic eyes and natural motion patterns by live Trinidadian guppies

Tim Landgraf, David Bierbach, Hai Nguyen, Nadine Muggelberg, Pawel Romanczuk, Jens Krause

Erschienen in: Bioinspiration & Biomimetics, Volume 11, Number 1

Journal linkpdf-Datei

In recent years, simple biomimetic robots have been increasingly used in biological studies to investigate social behavior, for example collective movement. Nevertheless, a big challenge in developing biomimetic robots is the acceptance of the robotic agents by live animals. In this contribution, we describe our recent advances with regard to the acceptance of our biomimetic RoboFish by live Trinidadian guppies(Poecilia reticulata). We provide a detailed technical description of the RoboFish system and show the effect of different appearance, motion patterns and interaction modes on the acceptance of the artificial fish replica. Our results indicate that realistic eye dummies along with natural motion patterns significantly improve the acceptance level of the RoboFish. Through the interactive behaviors, our system can be adjusted to imitate different individual characteristics of live animals, which further increases the bandwidth of possible applications of our RoboFish for the study of animal behavior.

Thema: robotic fish, collective behavior, biomimetics

Is it Reasonable to Employ Agents in Theorem Proving?

Christoph Benzmüller, Max Wisniewski

Erschienen in: In Proc. of the 8th International Conference on Agents and Artificial Intelligence (ICAART), SciTePress - Digital Library -- Science and Technology Publications, Lda, Vol. 1, 2016.


Agent architectures and parallelization are, with a few exceptions, rarely to encounter in traditional automated theorem proving systems. This situation is motivating our ongoing work in the higher-order theorem prover Leo-III . In contrast to its predecessor – the well established prover LEO-II – and most other modern provers, Leo-III is designed from the very beginning for concurrent proof search. The prover features a multiagent blackboard architecture for reasoning agents to cooperate and to parallelize proof construction on the term, clause and search level

Thema: ATP, Multi-Agent Systems, Blackboard Architecture, Concurrent Reasoning

Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL

Christoph Benzmüller, Alexander Steen, Max Wisniewski

Erschienen in: Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, EPiC Series in computing, vol. 41, 2016.

Non-classical logics (such as modal logics, description logics, conditional logics, multi-valued logics, hybrid logics, etc.) have many applications in artificial intelligence. In this tutorial, we will demonstrate a generic approach to automate propositional and quantified variants of non-classical logics using theorem proving systems for classical higher-order logic. Our particular focus will be on quantified multimodal logics. We will present and discuss a semantical embedding of quantified multimodal logics into classical higher-order logic, which enables the encoding and automated analysis of non-trivial modal logic problems in the Isabelle/HOL proof assistant. Additionally, TPTP compliant automated theorem proving systems can be called from within Isabelle’s Sledgehammer tool for automating reasoning tasks. In the tutorial, we will apply this approach to exemplarily solve a prominent puzzle from the AI literature: the well-known wise men.

Swarm Behavior for Autonomous Cars

Raúl Rojas, Fritz Ulbrich, Simon Rotter

Erschienen in: Handbook of Research on Design, Control and Modeling of Swarm Robotics, IGI, Global 2015. Ying Tang (ed)

IGI Global

Swarm behavior can be applied to many aspects of autonomous driving: e.g. localization, perception, path planning or mapping. A reason for this is that from the information observed by swarm members, e.g. the relative position and speed of other cars, further information can be derived. In this chapter the processing pipeline of a “swarm behavior module” is described step by step from selecting and abstracting sensor data to generating a plan – a drivable trajectory – for an autonomous car. Such a swarm-based path planning can play an important role in a scenario where there is a mixture of human drivers and autonomous cars. Experienced human drivers flow with the traffic and adapt their driving to the environment. They do not follow the traffic rules as strictly as computers do, but they are often using common sense. Autonomous cars should not provoke dangerous situations by sticking absolutely to the traffic rules, they must adapt their behavior with respect to the other drivers around them and thus merge with the traffic swarm.

Thema: trajectory, AutoNOMOS Project, Swarm Behaviour Module, C2C/C2X Communication

TVB-EduPack—An Interactive Learning and Scripting Platform for The Virtual Brain

Raúl Rojas, Henrik Matzke, Michael Schirner, Daniel Vollbrecht, Simon Rothmeier, Adalberto Llarena, Paul Triebkorn, Lia Domide, Jochen Mersmann, Ana Solodkin, Viktor Jirsa, Anthony Randal McIntosh, Petra Ritter

Erschienen in: frontiers in Neuroinformatics


The Virtual Brain (TVB; thevirtualbrain.org) is a neuroinformatics platform for full brain network simulation based on individual anatomical connectivity data. The framework addresses clinical and neuroscientific questions by simulating multi-scale neural dynamics that range from local population activity to large-scale brain function and related macroscopic signals like electroencephalography and functional magnetic resonance imaging. TVB is equipped with a graphical and a command-line interface to create models that capture the characteristic biological variability to predict the brain activity of individual subjects. To enable researchers from various backgrounds a quick start into TVB and brain network modeling in general, we developed an educational module: TVB-EduPack. EduPack offers two educational functionalities that seamlessly integrate into TVB's graphical user interface (GUI): (i) interactive tutorials introduce GUI elements, guide through the basic mechanics of software usage and develop complex use-case scenarios; animations, videos and textual descriptions transport essential principles of computational neuroscience and brain modeling; (ii) an automatic script generator records model parameters and produces input files for TVB's Python programming interface; thereby, simulation configurations can be exported as scripts that allow flexible customization of the modeling process and self-defined batch- and post-processing applications while benefitting from the full power of the Python language and its toolboxes. This article covers the implementation of TVB-EduPack and its integration into TVB architecture. Like TVB, EduPack is an open source community project that lives from the participation and contribution of its users. TVB-EduPack can be obtained as part of TVB from thevirtualbrain.org.

Thema: The Virtual Brain, brain modeling, computational neuroscience, connectome, educational platform

Real-Time Trajectory Optimization under Motion Uncertainty Using a GPU

Steffen Heinrich, André Zoufahl, Raúl Rojas

IEEE Xplore | 2015-10

Erschienen in: Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS).


This paper presents a sampling-based planning method considering motion uncertainty to generate more human-like driving paths for automated vehicles. Given information in the form of a small set of rules and driving heuristics the planning system optimizes trajectories in a seven dimensional state space. In a post-processing step a set of candidates is evaluated considering the uncertainty of the vehicles motion executing the given trajectory using a Linear-Quadratic Gaussian (LQG). This addresses the problem of indecisive planning behavior in case the optimal solution is unlikely to be followed precisely. The results of our experiments show that the mobile graphics processing unit (GPU) technology can be used as an enabler for real-time applications of computationally expensive planning approaches.

Thema: intelligent transportation systems, linear quadratic Gaussian control, optimisation, path planning, road vehicles, trajectory control

Automatic methods for long-term tracking and the detection and decoding of communication dances in honeybees

Raúl Rojas, Tim Landgraf, Benjamin Wild, Fernando Wario, Margaret J. Couvillon

Erschienen in: Frontiers in Ecology and Evolution - Behavioral and Evolutionary Ecology.


The honeybee waggle dance communication system is an intriguing example of abstract animal communication and has been investigated thoroughly throughout the last seven decades. Typically, observables such as waggle durations or body angles are extracted manually either directly from the observation hive or from video recordings to quantify properties of the dance and related behaviors. In recent years, biology has profited from automation, improving measurement precision, removing human bias, and accelerating data collection. We have developed technologies to track all individuals of a honeybee colony and to detect and decode communication dances automatically. In strong contrast to conventional approaches that focus on a small subset of the hive life, whether this regards time, space, or animal identity, our more inclusive system will help the understanding of the dance comprehensively in its spatial, temporal, and social context. In this contribution, we present full specifications of the recording setup and the software for automatic recognition of individually tagged bees and the decoding of dances. We discuss potential research directions that may benefit from the proposed automation. Lastly, to exemplify the power of the methodology, we show experimental data and respective analyses from a continuous, experimental recording of 9 weeks duration.

Thema: waggle dance, honeybee, animal behavir, animal tracking, computer vision

Acoustic/Lidar Sensor Fusion for Car Tracking in City Traffic Scenarios

Daniel Goehring, Hamma Tadjine

Erschienen in: Proceedings of the 3rd International Symposium on Future Active Safety Technology Towards zero traffic accidents, 2015.


In this paper we describe a sound source localization approach which, in combination with data from lidar sensors, can be used for an improved object tracking in the setting of an autonomous car. After explaining the chosen sensor setup we will show how acoustic data from two Kinect cameras, i.e., multiple microphones, which were mounted on top of a car, can be combined to derive an object's direction and distance. Part of this work will focus on a method to handle non-synchronized sensory data between the multiple acoustic sensors. We will describe how the sound localization approach was evaluated using data from lidar sensors.

Thema: sound source localization, autonomous driving, sensor data fusion

Autonomer Rollstuhl

Adalberto Llarena, Bennet Fischer, Jose Alvarez-Ruiz

Springer Vieweg | 2015-08

Erschienen in: Chapter in the book: "Technische Unterstützungssysteme"


Die zunehmende Alterung der Bevölkerung motiviert die Suche nach neuen Ansätzen für unterstützende Technologien, die Menschen mit eingeschränkter Bewegungsfähigkeit eine größere Selbständigkeit ermöglichen können. Der entwickelte robotische Rollstuhl ist ein Beispiel für autonome Unterstützung. Der Rollstuhl kann mittels abstrakter Befehle wie "Bring mich in die Küche" oder über Gehirnsteuerung kontrolliert werden. Die Software kann ohne Zutun des Nutzers die Fahrtstrecke planen und Hindernissen ausweichen. Dieser hohe Grad an Automatisierung kann somit zur Verbesserung der Lebensqualität beitragen.

Thema: autonomous wheelchair

Digital Ink in Modern Classroom: A Comprehensive Intelligent Teaching System

Bingyi Cao, Margarita Esponda, Raúl Rojas

iated Digital Library | 2015-07

Erschienen in: Proceedings of the 7th International Conference on Education and New Learning Technologies (EDULEARN 2015), Barcelona 2015.

iated Digital-Library

Information and communication technologies have brought great changes in the classroom. A wide variety of multimedia instruction systems are equipped in schools and educational institutions. However, people gradually find pen-paper or blackboard-chalk is still the most natural medium to express thoughts. They are irreplaceable tools for preparing and giving lectures in many subjects such as mathematics, physics and engineering due to their intuitive use and unmatched flexibility. A comprehensive teaching system called Intellichalk was developed based on this idea. Digital ink and information technologies were used to restore and enhance this natural way of expression. The system consists of three parts, a lesson preparation system, a classroom instruction system and a playback player. Each part can be used separately. Lesson preparation system includes a camera with bracket and an independent program. Contents written on the paper can be extracted out digitally and organized as digital ink blocks according to the user’s intention. These descriptive or conceptual digital ink contents can be easily reused to improve the efficiency of lectures. Intellichalk classroom instruction system is inspired by the idea of blackboard. It has a full-featured editor on which users can not only write and draw fluently but also add a wide range of multimedia materials such as images, texts and audios from internet or local disks. Digital ink blocks can be used whenever needed during the lecture. Unlike prepared sliders, this blackboard-like system shows the instructor’s thought process. In order to improve its usability and functionality, three intelligent modules were added to the system: a handwriting recognition module, a hand drawn geometric shapes recognition module and an animation module. Several interesting tools were developed by using these intelligent modules, such as handwriting lambda calculus demonstration program, pen gesture editing assist program and sorting algorithm animation program. The classroom instruction system can be viewed as an electronic blackboard enhanced by multimedia and intelligent technologies. It provides lecturers more possibilities on the form of teaching, gives students chances to follow up the thoughts of the teacher. The highly modular structure ensures that it can be easily configured, extended and upgraded. All the actions on the editor and the instructor’s voice are recorded automatically during the lecture. A player was developed to replay the entire lecture. Compare to normal video records, it has much better graphic quality and smaller file size, which is well suited for long-distance transmission and online playing. The Intellichalk system has been equipped in a multimedia classroom in Free University of Berlin since April 2014. It was configured with a 22-inch graphical tablet and four 60-inch large screens. More than a hundred students and teachers have benefited from the system. Practice has shown that Intellichalk system supports flexible teaching style, enlivens the classroom and provides comprehensive assistance to both teachers and students.

Thema: digital ink, instruction system, multimedia, intelligent module

Grid-based online road model estimation for advanced driver assistance systems

Raúl Rojas, J. Thomas, K. Stiens, S. Rauch

IEEE | 2015-06

Erschienen in: Proceedings of the Intelligent Vehicles Symposium (IV), Seoul 2015.


The information about the road course and individual lanes is an important requirement in driver assistance systems and for automated driving applications. It is often stored in a highly accurate offline map so that the road and the lanes are known in advance. However, there exist situations where an offline map can become unusable or invalid. This paper presents a novel approach for a road model estimation solely based on online measurements from sensors mounted on the ego vehicle. It combines perception data like detected lane markings, the movement history of dynamic objects in the vehicle's environment and detected road boundaries into a grid-based road model. This approach allows for an estimation of the road model even when one source of information is not available and offers a redundant source of information about the road, which is necessary in critical applications such as automated driving. The presented approach was tested and evaluated with a prototype vehicle and real sensor data from German highway scenarios.

Thema: driver information systems, intelligent transportation systems, object detection, road vehicles, sensor fusion

Localization inside a populated parking garage

Raúl Rojas, S. Wahl, P. Schlumberger, M. Stampfle

IEEE | 2015-06

Erschienen in: Proceedings of the Intelligent Vehicles Symposium (IV), Seoul 2015


For a vehicle driving safe inside a parking garage autonomously, it is necessary to build a map with its surroundings and also to localize itself within this map. This is known as Simultaneous Localization And Mapping (SLAM). To enable the vehicle to drive autonomously to an assigned parking slot, a parking area, or the exit, the vehicle also needs knowledge about the whole map of the parking garage. This map only contains static elements of the parking garage. Variable elements are not known to the parking garage and therefore are not contained in this static map. In order to reach a target, the vehicle needs to localize itself with respect to this static map. In this contribution the use of such a static map is proposed to support SLAM. This enables SLAM to determine poses related to a static map. Also the performance of SLAM is improved.

Thema: SLAM (robots), mobile robots, navigation, particle filtering (numerical methods) road vehicles, statistical distributions, traffic control

A Tutorial Introduction to the Lambda Calculus

Raúl Rojas

Erschienen in: Cornell University Library

arXiv:1503.09060 [cs.LO]

pdf-DateiCornell University Library

This paper is a concise and painless introduction to the λ -calculus. This formalism was developed by Alonzo Church as a tool for studying the mathematical properties of effectively computable functions. The formalism became popular and has provided a strong theoretical foundation for the family of functional programming languages. This tutorial shows how to perform arithmetical and logical computations using the λ -calculus and how to define recursive functions, even though λ -calculus functions are unnamed and thus cannot refer explicitly to themselves.

Thema: Lambda Calculus

Learning to Detect Visual Grasp Affordance

Daniel Goehring, Hyun Oh Song, Mario Fritz, Trevor Darrell

Erschienen in: IEEE Transactions on Automation and Engineering


Appearance-based estimation of grasp affordances is desirable when 3-D scans become unreliable due to clutter or material properties. We develop a general framework for estimating grasp affordances from 2-D sources, including local texture-like measures as well as object-category measures that capture previously learned grasp strategies. Local approaches to estimating grasp positions have been shown to be effective in real-world scenarios, but are unable to impart object-level biases and can be prone to false positives. We describe how global cues can be used to compute continuous pose estimates and corresponding grasp point locations, using a max-margin optimization for category-level continuous pose regression. We provide a novel dataset to evaluate visual grasp affordance estimation; on this dataset we show that a fused method outperforms either local or global methods alone, and that continuous pose estimation improves over discrete Output models. Finally, we demonstrate our autonomous object detection and grasping system on the Willow Garage PR2 robot.

Thema: Object detection, Machine learning, Pose estimation

On Logic Embeddings and Goedel's God

C. Benzmüller, B. Woltzenlogel Paleo

Erschienen in: Proceedings of the 22nd International Workshop on Algebraic Development Techniques (WADT 2014), Springer, LNCS, 2015.


We have applied an elegant and exible logic embedding approach to verify and automate a prominent philosophical argument: the ontological argument for the existence of God. In our ongoing computerassisted study, higher-order automated reasoning tools have made some interesting observations, some of which were previously unknown.

Developing a Multi-Agent System for a Blended Learning Application

Raúl Rojas, Dan-El Neil Vila-Rosado, Margarita Esponda,

Springer-Verlag | 2015

Erschienen in: New Research in Multimedia and Internet Systems, Advances in Intelligent Systems and Computing; Vol. 314, 2015. Presented on the "9th International Conference on Multimedia & Network Information Systems", Wroclaw, Sept. 2014.


Blended learning systems have become more popular than e-learning systems or even more than conventional educationalmethodologies. On Blended learning systems, the learners can view teaching materials asynchronously from different sources and collaborate with their peers and also they get the necessary face to face interaction with the instructor in the classroom. PowerChalk has arisen as the result from the analysis of several systems for E-Learning; it was designed to resolve an important limitation of current design methods: adaptability. In terms of adaptability, we have to consider that parallel to the evolution of e-learning methodologies, the intelligent agent paradigm has generated interest in many applications specially in order to support scaffolding activities and problem solving. It is for this reason that in this chapter presents the develop of a Multi-Agent System (MAS) on the PowerChalk system, a blended learning application that provide a robust, reliable, usable and sustainable multimedia technology for collaborative learning.

Leukocyte Detection Through an Evolutionary Method

Raúl Rojas, E. Cuevas, M. Diaz

Springer-Verlag | 2015

Erschienen in: Complex System Modelling and Control Through Intelligent Soft Computations, Studies in Fuzziness and Soft Computing Volume 319, 2015


Classical image processing methods often face great difficulties while dealing with images containing noise and distortions. Under such conditions, the use of soft computing approaches has been recently extended to address challenging real-world image processing problems. The automatic detection of Leukocytes or White Blood Cells (WBC) still remains as an unsolved issue in medical imaging. The analysis of WBC images has engaged researchers from fields of medicine and image processing alike. Since WBC can be approximated by an ellipsoid form, an ellipse detector algorithm may be successfully applied in order to recognize such elements. This chapter presents an algorithm for the automatic detection of leukocytes embedded into complicated and cluttered smear images that considers the complete process as a multi-ellipse detection problem. The approach, which is based on the Differential Evolution (DE) algorithm, transforms the detection task into an optimization problem whose individuals represent candidate ellipses. An objective function evaluates if such candidate ellipses are actually present in the edge map of the smear image. Guided by the values of such function, the set of encoded candidate ellipses (individuals) are evolved using the DE algorithm so that they can fit into the leukocytes which are enclosed within the edge map of the smear image. Experimental results from white blood cell images with a varying range of complexity are included to validate the efficiency of the proposed technique in terms of its accuracy and robustness.

Thema: Leukocyte detection; Image processing; WBC image analysis; Differential evolution; Evolutionary algorithms; Metaheuristics

A Computational Intelligence Optimization Algorithm Based on the Behavior of the Social-Spider

Raúl Rojas, Erik Cuevas, Miguel Cienfuegos; Alfredo Padilla

Springer International Publishing | 2014-12

Erschienen in: Computational Intelligence Applications in Modeling and Control Studies in Computational Intelligence Volume 575


Classical optimization methods often face great difficulties while dealing with several engineering applications. Under such conditions, the use of computational intelligence approaches has been recently extended to address challenging real-world optimization problems. On the other hand, the interesting and exotic collective behavior of social insects have fascinated and attracted researchers for many years. The collaborative swarming behavior observed in these groups provides survival advantages, where insect aggregations of relatively simple and “unintelligent” individuals can accomplish very complex tasks using only limited local information and simple rules of behavior. Swarm intelligence, as a computational intelligence paradigm, models the collective behavior in swarms of insects or animals. Several algorithms arising from such models have been proposed to solve a wide range of complex optimization problems. In this chapter, a novel swarm algorithm called the Social Spider Optimization (SSO) is proposed for solving optimization tasks. The SSO algorithm is based on the simulation of cooperative behavior of social-spiders. In the proposed algorithm, individuals emulate a group of spiders which interact to each other based on the biological laws of the cooperative colony. The algorithm considers two different search agents (spiders): males and females. Depending on gender, each individual is conducted by a set of different evolutionary operators which mimic different cooperative behaviors that are typically found in the colony. In order to illustrate the proficiency and robustness of the proposed approach, it is compared to other well-known evolutionary methods. The comparison examines several standard benchmark functions that are commonly considered within the literature of evolutionary algorithms. The outcome shows a high performance of the proposed method for searching a global optimum with several benchmark functions.

Thema: Swarm algorithms; Global optimization; Bio-inspired algorithms; Computational intelligence; Evolutionary algorithms; Metaheuristics

Human-Machine Cooperation in Highly Automated Driving

R. Rojas, M. Krähling, U. Lages, S. Griesche, D. Käthner

Erschienen in: Intelligent Transportation Systems World Congress 2014, Detroit, Michigan.


This paper presents a concept for a highly automated vehicle which allows for adaption to and cooperation with a human driver. This addresses the problem of vehicle automation level 3, as defined by the NHTSA, where a vehicle is capable of being driven automatically, but the human driver is still in charge from a legal point of view.

Thema: Human-Machine Interaction; Automated Driving, Driver Modelling

An analysis of the transition proportion for binarization in handwritten historical documents

Raúl Rojas, Marte A. Ramirez-Ortegón, Lilia L. Ramirez, Ines Ben Messaoud, Erik Cuevas, Volker Märgner

Elsevier B.V. | 2014-08

Erschienen in: Pattern Recognition, Volume 47, Issue 8.


In this paper, we will present a mathematical analysis of the transition proportion for the normal threshold (NorT) based on the transition method. The transition proportion is a parameter of NorT which plays an important role in the theoretical development of NorT. We will study the mathematical forms of the quadratic equation from which NorT is computed. Through this analysis, we will describe how the transition proportion affects NorT. Then, we will prove that NorT is robust to inaccurate estimations of the transition proportion. Furthermore, our analysis extends to thresholding methods that rely on Bayes rule, and it also gives the mathematical bases for potential applications of the transition proportion as a feature to estimate stroke width and detect regions of interest. In the majority of our experiments, we used a database composed of small images that were extracted from DIBCO 2009 and H-DIBCO 2010 benchmarks. However, we also report evaluations using the original (H-)DIBCO׳s benchmarks.

Thema: Historical documents; Threshold; Binarization; Transition method, Transitionn pixel, Normal; Lognormal; Minimum error rate; Otsu; Bayes´ theory

Automating Gödel’s Ontological Proof of God’s Existence with Higher-order Automated Theorem Provers

C. Benzmüller, Bruno Woltzenlogel Paleo

T. Schaub et al. (Eds.) | 2014-08

Erschienen in: IOS Press, Frontiers in Artificial Intelligence and Applications, volume 263. Presented on the 21st European Conference on Artificial Intelligence, August 18-22, 2014.


Kurt Gödel's ontological argument for God's existence has been formalized and automated on a computer with higher-order automated theorem provers. From Gödel's premises, the computer proved: necessarily, there exists God. On the other hand, the theorem provers have also confirmed prominent criticism on Gödel's ontological argument, and they found some new results about it. The background theory of the work presented here offers a novel perspective towards a computational theoretical philosophy.

Konrad Zuse's Proposal for a Cipher Machine

Raúl Rojas

Erschienen in: Cryptologia , Volume 38, Issue 4, 2014


The German inventor Konrad Zuse wrote a proposal for a cipher machine during the winter of 1939–1940. The document was prepared at the Eastern front during WWII and reached the German military authorities, possibly with the help of Kurt Pannke, a manufacturer of calculating equipment. Zuse's scheme was recently found in his Nachlass. It is documented here for the first time. Zuse's offer was rejected by the military, so the software-based cipher machine described in the letter never materialized.

Thema: Konrad Zuse, Mechanical Computer, Z1

Lane Localization for Autonomous Model Cars

Lukas Maischak

Freie Universität Berlin | 2014-07

Erschienen in: Technical Reports - Serie B - Informatik, Fachbereich Mathematik und Informatik


Mobile robotics is a rapidly growing field and has countless applications including exploration, logistics, rescue operations, as well as domestic and military use. One particularly interesting example of ist use is the construction of autonomous, "self-driving" cars. Imagine that car accidents caused by human error are a thing of the past, or that your car can find ist own parking spot after you have left the vehicle. In many cases, mobile robots need to plan and make decisions autonomously while interacting with their environment. A necessary prerequisite for them to execute most non-trivial tasks is to have a concept of their environment and their location in it. Determining this location is a fundamental problem in mobile robotics known as localization. Autonomous cars need to know where they are on the road, both on a small scale to stay in lane and on a large scale to navigate. This project explores mobile robotic problems on a small scale. The objective is to construct a small model car that is able to drive autonomously in an indoor model environment like those displayed in Figures 1.1 and 1.2. This document focuses on a mechanism for localizing autonomous model cars within such an environment. The next chapter gives a brief overview of the target platform - the model car in use. Chapter 3 defines the problem this document is triying to solve in more detail. Chapters 4 and 5 describe and evaluate two alternative - though related - solutions to that Problem.

Large Scale Semi-Global Matching on the CPU

Tobias Langner, Raúl Rojas, Sven Adfeldt

Erschienen in: Intelligent Vehicles Symposium Proceedings, 2014 IEEE, 2014, 195-201


Semi-Global Matching (SGM) is widely used for real-time stereo vision in the automotive context. Despite its popularity, only implementations using reconfigurable hardware (FPGA) or graphics hardware (GPU) achieve high enough frame rates for intelligent vehicles. Existing real-time implementations for general purpose PCs use image and disparity sub-sampling at the expense of matching quality. We study methods to improve the efficiency of SGM on general purpose PCs, through fine grained parallelization and usage of multiple cores. The different approaches are evaluated on the KITTI benchmark, which provides real imagery with LIDAR ground truth. The system is able to compute disparity maps of VGA image pairs with a disparity range of 128 values at more than 16 Hz. The approach is scalable to the number of available cores and portable to embedded processors.

Thema: Degradation; Field programmable gate arrays; Graphics processing units; Hardware; Image coding; Sociology ; Training data

Blending in with the Shoal: Robotic Fish Swarms for Investigating Strategies of Group Formation in Gruppies

Tim Landgraf, Hai Nguyen, Joseph Schröer, Angelika Szengel, Romain J.G. Clément, David Bierbach, Jens Krause

Springer International Publishing Switzerland | 2014-07

Erschienen in: Living Machines 2014, LNAI 8608. Proceedings of the Third International Conference, Living Machines 2014, Milan.

Robotic fish that dynamically interact with liv fish shoals dramatically augment the toolset of behavioral biologists. We have developed in Guppies and similarly small fish. This contribution presents full implementation Details of he System and promising experimental results. Over long durations our robots are able to integrate themselves into shoals or recruit he group to exposed locations hat are usually avoided. This system is the first open-source projekt for both software and hardware components and is supposed to facilitate research in the emerging field of bio-hybrid societies.

Thema: biomimetic robots, biomimetics, swarm intelligence, social behavior, social networks, swarm tracking

HOL Provers for First-order Modal Logics - Experiments

Christoph Benzmüller

Erschienen in: EasyChair, EPiC Series


Higher-order automated theorem provers are well suited as reasoners for a wide range of quantified non-classical logics. The key idea is to exploit classical higher-order logic (HOL) as a universal meta-logic and, for example, to explicitly encode Kripke structures within this meta-logic. Experiments have shown that this approach which is orthogonal to explicit worls labeling techniques in direct theorem provers, is indeed compeititive. More recent but non-exhaustive, experiments have improved and confirmed these results. This short paper significantly further extends the experiments reported in [3]. The paper thus provides useful and relevant Information for evaluations of competitor systems. Moreover, some light is shed on the collective and individual performances of the higher order automated theorem provers LEO-II, Satallax, Isabelle, agsyHOL and Nitpick.

Die Tiefe des Raumes

Die Tiefe des Raumes

Raúl Rojas

Heise Zeitschriften Verlag | 2014-06-04


"Gott ist rund", schrieb der mexanische Schriftsteller Juan Villoro. Wie sieht seine Flugbahn aus? Den Ball im Blick rennt der Fußballspieler alle 70 Sekunden eines Matches los, um mit seiner Mannschaft das Runde ins Netz zu jagen und Gebete der Fans zu erfüllen. Fußball ist, wie jedes Kind weiß, von magischem Denken durchdrungen: "Wenn mein Fuß beim nächsten Schritt auf die Linie zwischen den Steinplatten trifft, dann gewinnt Deutschland..." Wie aber steht es mit der Wissenschaft, mit Flugbahnen der postaristotelischen Physik oder mit der berechenbaren Wahrscheinlichkeit, dass Deutschland und nicht Brasilien oder Spanien Weltmeister wird? Tore folgen dem "Gesetz der kleinen Zahlen", schreibt Raúl Rojas im e-Book "Aus der Tiefe des Raumes" und verrät vor der WM in Brasilien, wann die entscheidenden Tore fallen, um wieviel schneller das Spiel geworden ist, wie es wissenschaftlich um den neuen "Brazuca"-Ball steht, ob Spieltheorien beim Elfmeter helfen, und dass der Soccer-Power-Index (SPI) mehr aussagt als das FIFA-Ranking. Rojas dribbelt und zaubert mit Karl-Heinz Rummenigges Satz "Fußball ist keine Mathematik". Stimmt schon, so Rojas, Professor für Mathematik und Informatik: Fußball hat eine nicht zu vernachlässigende zufällige Komponente, die die besten Versuche, Ordnung im Chaos zu finden, durcheinander bringt. Aber mit Mathematik, Physik und mit Wirtschaftswissenschaften lassen sich Aussagen treffen, die das Ball-Geschehen besser beleuchten, wie das Buch vorführt. Etwa wenn es darum geht, die Weltmeisterschaft am Computer zu simulieren, um herauszufinden, welche Mannschaft die besten Chancen hat, das Turnier zu gewinnen. "Nicht immer gewinnt die beste Mannschaft, so dass am Ende von 1.000 Simulationen die Häufigkeit des Gewinns durch Brasilien, Deutschland oder Spanien angegeben werden kann. Es ist, als ob wir tausend Welten hätten, in denen die WM ausgetragen wird. In etwa 17% dieser alternativen Realitäten, d.h. in 170 Welten, gewinnt auch Deutschland."

Thema: Telepolis, Fußball, Spieltheorie, Weltmeisterschaft

The Z1: Architecture and Algorithms of Konrad Zuse's First Computer

Raúl Rojas

Erschienen in: Cornell University Library, Report Number: DCIS-14-1


This paper provides the first comprehensive description of the Z1, the mechanical computer built by the German inventor Konrad Zuse in Berlin from 1936 to 1938. The paper describes the main structural elements of the machine, the high-level architecture, and the dataflow between components. The computer could perform the four basic arithmetic operations using floating-point numbers. Instructions were read from punched tape. A program consisted of a sequence of arithmetical operations, intermixed with memory store and load instructions, interrupted possibly by input and output operations. Numbers were stored in a mechanical memory. The machine did not include conditional branching in the instruction set. While the architecture of the Z1 is similar to the relay computer Zuse finished in 1941 (the Z3) there are some significant differences. The Z1 implements operations as sequences of microinstructions, as in the Z3, but does not use rotary switches as micro-steppers. The Z1 uses a digital incrementer and a set of conditions which are translated into microinstructions for the exponent and mantissa units, as well as for the memory blocks. Microinstructions select one out of 12 layers in a machine with a 3D mechanical structure of binary mechanical elements. The exception circuits for mantissa zero, necessary for normalized floating-point, were lacking; they were first implemented in the Z3. The information for this article was extracted from careful study of the blueprints drawn by Zuse for the reconstruction of the Z1 for the German Technology Museum in Berlin, from some letters, and from sketches in notebooks. Although the machine has been in exhibition since 1989 (non-operational), no detailed high-level description of the machine's architecture had been available. This paper fills that gap.

Modular Architecture for Pen-Based Digital Ink on Blended Learning Applications

Raúl Rojas, Margarita Esponda, Dan-El Neil Vila-Rosodo

Library, Engineering & Technology Digital Library, EBSCO | 2014-04

Erschienen in: Proceedings of the "International Journal of Information and Education Technology" Vol. 4(2)


Pen-based technologies can be combined with different kinds of hardware and software to gain pedagogical benefits on blended learning applications. Particularly, digital ink and handwriting recognition furnish the convenience to access, navigate and manipulate data more easily. It is also well know that user interfaces for pen computing can be implemented in several ways, with different techniques and for several kinds of applications. A modular programming architecture for pen-based digital ink was developed in order to provide a robust, reliable, usable and sustainable multimedia technology for a blended learning application. We present this approach and the respective advantages.

Thema: Multimedia technologies, blended learning, modular programming, pen computing, sketch recognition

Konrad Zuse und der bedingte Sprung

Raúl Rojas

Springer-Verlag Berlin Heidelberg | 2014-02-01

Erschienen in: Informatik-Spektrum, Volume 37, Issue 1


Dieser Aufsatz beschreibt die von Konrad Zuse für die Rechenmaschine Z4 eingeführten bedingten Befehle, inklusive dem bedingten Sprung. Die extra für numerische Berechnungen angedachte Anweisungen wurden um 1950 auf Bitte der Mathematiker der ETH-Zürich in der Z4 eingebaut. Der bedingte Sprung ignorierte alle nachfolgende Befehle im Programmlochstreifen bis zur ,,Start“-Marke im Code, falls der Wahrheitswert im ersten Arbeitsregister auf wahr gesetzt war. Anderenfalls wurde der Sprung ignoriert. Einfache Programmierbeispiele erleichtern das Verständnis der Funktionsweise der bedingten Befehle der Z4

An Adaptive Interactive Multimedia System for Intelligent Environments

Raúl Rojas, Dan-El Neil Vila-Rosado

IACSIT-Press | 2014-02

Erschienen in: International Journal of Information and Education Technology


We present a new interactive multimedia system for blended learning called PowerChalk. The goal of PowerChalk is to provide a robust, reliable, usable and sustainable multimedia technology to any intelligent environment focused on blended learning. The software architecture allows adapting the system to any hardware configuration and supports collaboration, communication, creativity and learning. In this sense, PowerChalk resolves many limitations of current e-learning systems, improves human-computer interaction for the management of different kinds of hardware and data and allows to implement different configurations for intelligent environments.

Thema: Multimedia technologies, blended learning, inelligent environments, pen-based user interfaces, modular programming

MOOCs statt Hörsaal

MOOCs statt Hörsaal

Raúl Rojas, Matthias Becker

Heise Zeitschriften Verlag GmbH & Co. KG | 2014-02


Immer mehr Menschen nutzen "Massive Open Online Courses" (MOOCs), an denen sich manchmal Hunderttausende einschreiben. Dozenten, die ansprechend auftreten, werden zu internationalen Stars. Der Hörsaal der Universitäten wird durch das Internet weltweit öffentlich. Immer mehr Universitäten bieten Online-Kurse an und geben dafür teils viel Geld aus. Sie glauben, im internationalen Konkurrenzkampf um Studenten, Image und Überleben Online-Kurse weltweit offerieren zu müssen. Neue Plattformen schießen derzeit wie Pilze aus dem Boden, um die Chancen auf dem weltweiten Bildungsmarkt zu ergreifen. Versprochen wird, dass jeder so auf der ganzen Welt die Möglichkeit erhält, sich an den besten Universitäten weiterzubilden. Bislang gibt es dafür nur eine Teilnahmebestätigung. Interessant wird sein, ob online auch Prüfungen abgelegt werden können. Die technisch avancierte Internetlehre wird die Hochschulbildung insgesamt verändern. Durch Automatisierung, Offshoring und Crowdsourcing ermöglichen MOOCs eine umfassende Rationalisierung, die unsere Vorstellung davon, was akademische Bildung eigentlich bedeutet, gründlich umkrempeln wird. Matthias Becker gibt einen Überblick über den Stand der Dinge und stellt vor, wie es in der schönen, neuen Welt der Online-Universitäten und Online-Ausbildung weitergehen könnte. Raùl Rojas, Robotikprofessor an der FU Berlin, analysiert aus eigenen Erfahrungen die Möglichkeiten von MOOCs. In Interviews mit Experten wird geklärt, warum Universitäten auf MOOCs setzen, welche Grenzen sie haben und was sie verändern werden. Es kommen außerdem zu Wort: Prof. Dr. Bernd Huber, Präsident der LMU, Jürgen Handke, Professor für Anglistik, der seit Mitte der 1990er Jahre multimediales linguistisches Lernmaterial entwickelt, Les Perelman vom Massachusetts Institute of Technology (MIT) und Jörn Loviscach, Professor für Ingenieurmathematik, der seit 2009 seine Lehrveranstaltungen in Mathematik auf YouTube verbreitet.

The straight line, the catenary, the brachistochrone, the circle, and Fermat

Raúl Rojas

Erschienen in: Cornell University Library


This paper shows that the well-known curve optimization problems which lead to the straight line, the catenary curve, the brachistochrone and the circle, can all be handled using a unied formalism. Furthermore, from the general differential equation fulfilled by these geodesics, we can guess additional functions and the required metric. The parabola, for example, is a geodesic under a metric guessed in this way. Numerical solutions are found for the curves corresponding to geodesics in the various metrics using a ray-tracing approach based on Fermat's principle.

An optimization for binarization methods by removing binary artifacts

Raúl Rojas, Marte Ramirez-Ortegon, Volker Märgner, Erik Cuevas

Erschienen in: Pattern Recognition Letters, Vol. 34(11)


In this article, we introduce a novel technique to remove binary artifacts. Given a gray-intensity image and its corresponding binary image, our method detects and remove connected components that are more likely to be background pixels. With this aim, our method constructs an auxiliary image by the min-imum-error-rate threshold and, then, computes the ratio of intersection between the connected compo-nents of the original binary image and the connected components of the auxiliary image. Connected components with high ratio are considered true connected components while the rest are removed from the output. We tested our method in binarization methods for historical documents (handwritten and printed). Our results are favorable and indicate that our method can improve the outputs from diverse binarization methods. In particular, a high improvement was observed for printed documents. Our method is easy to implement, has a moderate computational cost, and has two parameters whose model interpretation allows an easy empirical selection.

Thema: Historical documents, threshold, denoising, binarization minimum error rate, Bayes theory

Cut-free Calculi for Challenge Logics in a Lazy Way

Dr. C. Benzmüller

Erschienen in: Proceedings of the International Workshop on Algebraic Logic in Computer Science


Die Prozessorarchitektur der Rechenmaschine Z1

Raúl Rojas, Hai Nguyen, Julian Röder

Springer-Verlag | 2013-11-28

Erschienen in: Informatik-Spektrum, Band 36, Heft 6, December 2013.


Dieser Aufsatz beschreibt zum ersten Mal die Datenflussarchitektur des Prozessors der Z1, der ersten von Konrad Zuse gebauten Rechenmaschine (1936-1938). Die Struktur wurde aus den Designunterlagen der im Jahr 1989 fertiggestellten Rekonstruktion der Z1 herausdestilliert. Die Z1 war ein Fließkommarechner. Der Prozessor enthält zwei Einheiten: eine arithmetisch-logische Einheit für die Behandlung der Exponenten und eine zweite für die Mantissen. Der Prozessor ähnelt stark dem der Z3, ist aber einfacher, da auf einen großen Shifter und andere Datenflussoptionen verzichtet wurde. Der Prozessor der Z1 brauchte mehr Zyklen für die Grundrechenarten als die Z3, konnte aber mit wenigen logischen Komponenten auskommen, ein wichtiges Designkriterium für eine mechanische Rechenmaschine.

This paper describes the dataflow architecture of the processor of the Z1, the first Computer designed and built by Konrad Zuse (between 1936 and 1938). The structure was recovered from an analysis of the design blueprints drawn for a modern reconstruction of the Z1 which was finished in 1989. The Z1 was a floating-point machine: the processor consists of two sections, one containing the ALU for the exponent, a second with an ALU for the mantissas. The processor is fairly similar to the processor of the Z3, but is simpler since a large shifter and some other dataflow options were sidestepped. The processor of the Z1 needed more cycles than the Z3 for the basic arithmetic operations but could be built with less logical components, an important design feature for a mechanical machine.

Thema: Konrad Zuse, Z1, Rechenmaschine, Prozessarchitektur

Bitcoins: Irrationaler Überschwang

Raúl Rojas

Erschienen in: Telepolis - Heise Online

online Artikel

Das Interesse an Bitcoins bleibt ungebrochen. Die asiatische Nachfrage hat den Wechselkurs der digitalen Währung in schwindelerregende Höhe getrieben. Jedermann kann am heimischen Bildschirm zum Spekulanten werden und digital Dostojewskis Diktum "Geld ist geprägte Freiheit" nachgehen. Man müsste mittlerweile schon völlig von der Außenwelt abgekoppelt sein, um noch nichts über Bitcoins gehört oder gelesen zu haben. Bis zu 900 Dollar wurden zeitweilig für einen Bitcoin bezahlt. Die Zeitungen veröffentlichen herzerwärmende Stories vom beneidenswerten Bitcoin-Besitzer, der schon einen Ferrari oder ein Haus mit dem Erlös von Bitcoins gekauft hat. Da aber das "echte" Geld von irgendwoher kommen muss, gibt es dafür sicherlich tausend Andere, die mit Bitcoins Geld verloren haben. Bitcoins vermitteln nur eine Umverteilung vom Reichtum, ohne echten Reichtum zu generieren.

Thema: Bitcoins, popular science

Conditioned behavior in a robot controlled by a spiking neural network

Raúl Rojas, Tim Landgraf, Martin Nawrot, Lovisa Irpa Helgadottir, Joachim Haenicke

IEEE Xplore | 2013-11

Erschienen in: Proceedings of the 6th IEEE/EMBS Conference on Neural Engineering (NER), November 2013


Insects show a rich repertoire of goal-directed and adaptive behaviors that are still beyond the capabilities of today's artificial systems. Fast progress in our comprehension of the underlying neural computations make the insect a favorable model system for neurally inspired computing paradigms in autonomous robots. Here, we present a robotic platform designed for implementing and testing spiking neural network control architectures. We demonstrate a neuromorphic realtime approach to sensory processing, reward-based associative plasticity and behavioral control. This is inspired by the biological mechanisms underlying rapid associative learning and the formation of distributed memories in the insect.

Computational Intelligence in Image Processing

Raúl Rojas, Eric Cuevas, Daniel Zaldivar, Gonzalo Pajares, Marco Perez-Cisneros

Hindawi Publishing Corporation | 2013-11

Erschienen in: Mathematical Problems in Engineering, Vol. 2013, Article ID 530404

pdf-DateiHindawi link

The Archaeocopter Project

Raúl Rojas, Benjamin Ducke, D. Gräf

Erschienen in: 6th International Congress Science and Technology for the Safeguard of Cultural Heritage in the Mediterranean Basin Athen/Greece, 2013


Located in the heart of Europe, Saxony is characterised by an impressive heritage that encompasses tens of thousands of archaeological sites and registered monuments, bearing testimony to the cultural and historical importance of the region, both within Germany and Central Europe. The effective protection and management of this valuable but finite resource requires innovative new technologies with a focus on accuracy, efficiency and intuitive design. The project "Archaeocopter" (www.archaeocopter.de) is committed to the design and development of ultralight unmanned aerial vehicles (UAV) for airborne image data acquisition in archaeology and related fields. The acquisition of high-resolution, georeferenced imagery is a fundamental prerequisite for the detection and documentation of archaeological heritage. Structure from Motion (SfM) is a popular and robust method for producing 3D reconstructions from series of overlapping images (multi-view reconstruction). It provides heritage professionals with a flexible and low-cost method for the documentation and digital preservation of objects of interest, especially complex architectural remains. SfM currently suffers from two fundamental limitations that restrict the degree to which the quality of the resulting models can be assured: the approach is computationally demanding, and the reconstructed point clouds tend to be inhomogeneous. However, the video material produced by UAV-borne cameras contains massively overlapping image data and therefore constitutes ideal input material for the SfMbased reconstruction of buildings, sites or entire landscapes. In addition, parallel processing of data allows the rapid production of preview models useful for quality assurance.

Thema: 3D site recording, UAVs, SfM, multi-view reconstruction, heritage management

Formalization, Mechanization and Automation of Gödel's Proof of God's Existence

C. Benzmüller, Bruno Woltzenlogel Paleo

Cornell University Library | 2013-08

arXivcomplete formalisation

Goedel's ontological proof has been analysed for the first-time with an unprecedent degree of detail and formality with the help of higher-order theorem provers. The following has been done (and in this order): A detailed natural deduction proof. A formalization of the axioms, definitions and theorems in the TPTP THF syntax. Automatic verification of the consistency of the axioms and definitions with Nitpick. Automatic demonstration of the theorems with the provers LEO-II and Satallax. A step-by-step formalization using the Coq proof assistant. A formalization using the Isabelle proof assistant, where the theorems (and some additional lemmata) have been automated with Sledgehammer and Metis.

Thema: Logic in Computer Science, Artificial Intelligence, Logic

Automating Quantified Conditional Logics in HOL

C. Benzmüller

AAAI Press / International Joint Conferences on Artificial Intelligence | 2013-08

Erschienen in: Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (IJCAI 2013)


A notion of quantified conditional logics is provided that includes quantification over individual and propositional variables. The former is supported with respect to constant and variable domain semantics. In addition, a sound and complete embedding of this framework in classical higher-order logic is presented. Using prominent examples from the literature it is demonstrated how this embedding enables effective automation of reasoning within (object-level) and about (meta-level) quantified conditional logics with off-the-shelf higher-order theorem provers and model finders.

Thema: Higher Order Logic, LEO Prover, Semantic Embedding, Modal Logics, Combinations of Logics

Weighted Semi-Global Matching and Center-Symmetric Census Transform

Tobias Langner, Raúl Rojas

Springer-Verlag *Best paper award* | 2013-08

Erschienen in: Proceedings of the "15th International Conference on Computer Analysis of Images and Patterns (CAIP 2013)", York, United Kingdom.


Automotive applications based on stereo vision require robust and fast matching algorithms, which makes semi-global matching (SGM) a popular method in this field. Typically the Census transform is used as a cost function, since it is advantageous for outdoor scenes. We propose an extension based on center-symmetric local binary patterns, which allows better efficiency and higher matching quality. Our second contribution exploits knowledge about the three-dimensional structure of the scene to selectively enforce the smoothness constraints of SGM. It is shown that information about surface normals can be easily integrated by weighing the paths according to the gradient of the disparity. The different approaches are evaluated on the KITTI benchmark, which provides real imagery with LIDAR ground truth. The results indicate improved performance compared to state-of-the-art SGM based algorithms.

Thema: stereo vision, matching costs, census transform, local binary pattern, semi-global matching

NeuroCopter: Neuromorphic Computation of 6D Ego-Motion of a Quadcopter

Raúl Rojas, Tim Landgraf, M. Nawrot, B. Wild, T. Ludwig, P. Nowak, L. Helgadóttir, B. Daumenlang, P. Breinlinger

Springer-Verlag | 2013-08

Erschienen in: Proceedings of the 2nd Conference on Living Machines 2013, London, United Kingdom, Lecture Notes in Computer Science, Vol. 8064.


The navigation capabilities of honeybees are surprisingly complex. Experimental evidence suggests that honeybees rely on a map-like neuronal representation of the environment. Intriguingly, a honeybee brain exhibits approximately one million neurons only. In an interdisciplinary enterprise, we are investigating models of high-level processing in the nervous system of insects such as spatial mapping and decision making. We use a robotic platform termed NeuroCopter that is controlled by a set of functional modules. Each of these modules initially represents a conventional control method and, in an iterative process, will be replaced by a neural control architecture. This paper describes the neuromorphic extraction of the copter’s ego motion from sparse optical flow fields. We will first introduce the reader to the system’s architecture and then present a detailed description of the structure of the neural model followed by simulated and real-world results.

Thema: neural networks, neuromorphic computation, biomimetics, self-localization

A model for the gray-intensity distribution of historical handwritten documents

Raúl Rojas, Marte A. Ramirez-Ortegón, Lilia L. Ramirez-Ramirez, Ines Ben Messaoud, Volker Märgner, Erik Cuevas

Springer Verlag | 2013-08

Erschienen in: International Journal on Document Analysis and Recognition (IJDAR).


In this article, our goal is to describe mathematically and experimentally the gray-intensity distributions of the fore- and background of handwritten historical documents. We propose a local pixel model to explain the observed asymmetrical gray-intensity histograms of the fore- and background. Our pixel model states that, locally, the gray-intensity histogram is the mixture of gray-intensity distributions of three pixel classes. Following our model, we empirically describe the smoothness of the background for different types of images. We show that our model has potential application in binarization. Assuming that the parameters of the gray-intensity distributions are correctly estimated, we show that thresholding methods based on mixtures of lognormal distributions outperform thresholding methods based on mixtures of normal distributions. Our model is supported with experimental tests that are conducted with extracted images from DIBCO 2009 and H-DIBCO 2010 benchmarks. We also report results for all four DIBCO benchmarks.

Thema: binarization, tresholding, normal, historical documents, handwritten, DIBCO

Camera Based Detection and Classification of Soft Shoulders, Curbs and Guardrails

Raúl Rojas, Alexander Seibert, Andreas Tewes, Michael Hähnel

accepted for oral presentation at 2013 IEEE Intelligent Vehicles Symposium, Gold Coast, Australia | 2013-06-25


Computer Controlled Human Soccer League

Raúl Rojas, Hamid Mobalegh, Björn Karger

Presented on the RoboCup-Symposium, Einhoven, The Netherlands. | 2013-06-24


On-line Stereo Self-Calibration

Tobias Langner, Raúl Rojas

Springer-Verlag | 2013-06-17

Erschienen in: Proceedings of the 18th Scandinavian Conference on Image Analysis, Espoo, Finland. Lecture Notes in Computer Science, Vol. 7944.


This paper presents an approach to the problem of on-line stereo self-calibration. After a short introduction of the general method, we propose a new one, based on the minimization of matching costs. We furthermore show that the number of matched pixels can be used as a quality measure. A Metropolis algorithm based Monte-Carlo scheme is employed to reliably minimize the costs. We present expermental results in the context of automotive stereo with different matching algorithms. These show the effectiveness for the calibration of roll and pitch angle offsets.

Thema: self-calibration, stereo vision, matching costs

The Konrad Zuse Internet Archive Project

Raúl Rojas, Hai Nguyen, Julian Röder

Erschienen in: History of Computing Conference, HC 2013, IFIP AICT 416, IFIP International Federation for Information Processing


Interactive Robotic Fish for the Analysis of Swarm Behavior

Raúl Rojas, Tim Landgraf, Hai Nguyen, Stefan Forgo, S. Schneider, J. Schröer, C. Krüger, Henrik Matzke, R. Clément, Jens Krause

Springer-Verlag | 2013-06-12

Erschienen in: Proceedings of the 4th International Conference (ICSI 2013), Harbin, China, June 12-15, 2013, part I. Lecture Notes in Computer Science, Vol. 7928.


Biomimetics robots can be used to analyze social behavior through active interference with live animals. We have developed a swarm of robotic fish that enables us to examine collective behaviors in fish shoals. The system uses small wheeled robots, moving under a water tank. The robots are coupled to a fish replica inside the tank using neodymium magnets. The position of the robots and each fish in the swarm is tracked by two cameras. The robots can execute certain behaviors integrating feedback from the swarm's position, orientation and velocity. Here, we describe implementation details of our hardware and software and show first results of the analysis of behavioral experiments.

Thema: biomimetic robots, swarm intelligence, social behavior, social networks, swarm tracking

Calibration of Video Cameras

Raúl Rojas, Ernesto Tapia

Erschienen in: Technical Reports - Serie B - Informatik, Fachbereich Mathematik und Informatik


We show how to compute the extrinsic parameters of a video camera from the optical flow measured in consecutive video frames. We assume that the camera is mounted on a car or a robot which move forward and sideways on a flat area to acquire the images used for the calibration. The vanishing points of the optical flow lines provide enough information to compute the camera rotation matrix. We also show how the lines on the ground together with the vehicle's velocity provide enough iinformation to compute the camera position.

Thema: Calibration, Video Cameras, Optical Flow

An objective method to evaluate stroke-width measures for binarized documents

Marte A. Ramírez-Ortegón, Volker Märgner, Erik Cuevas and Raúl Rojas

IEEEXplore | 2013

Erschienen in: Proceedings of the 12th International Conference on Document Analysis and Recognition (ICDAR 2013), Washington, August 2013


In this article, we propose an objective method to evaluate stroke-width measures. With this aim, we discuss the relevance of features based on the stroke width for document analysis. Then, we point out that most of the consulted references have a vague definition of stroke width. Because of this, we propose a formal definition of the stroke-width and remark the linearity of the stroke-width as an important property. Inspired by these ideas, we propose a measure together with a dataset to evaluate the linearity of the measurements of the stroke width and conduct an evaluation for seven well-known stroke-width methods. Our experiments have interesting results, like the fact that the most popular method is the one with the worst performance and that the best method is the easiest to implement. We hope that our objective evaluation assists further authors to choose suitable stroke-width methods for their applications.

A Top-down Approach to Combining Logics

Dr. C. Benzmüller

Barcelona, Spain: SciTePress | 2013

Erschienen in: Proceedings of the 5th International Conference on Agents and Artificial Intelligence (ICAART)


The mechanization and automation of combination of logics, expressive ontologies and notions of context are prominent current challenge problems. I propose to approach these challenge topics from the perspective of classical higher-order logic. From this perspective these topics are closely related and a common, uniform solution appears in reach.

Thema: Combinations of Logics; Context, Expressive Ontologies, Multi-Agent Systems, Higher-order Logic, Semantic Embedding, Proof Automation

Können Roboter lügen? Essays zur Robotik und Künstlichen Intelligenz


Raúl Rojas

Hannover: Heise Zeitschriften Verlag GmbH & Co. KG | 2013


Raúl Rojas ist Professor für Informatik an der Freien Universität Berlin. Schwerpunkt seiner Forschung sind Robotik/KI und Neuronale Netze. Mit den Fußball spielenden Robotern FU Fighters, die von ihm und seinem Team entwickelt wurden, konnte er zweimal im internationalen RoboCup in der Kategorie der Middle Size und Small Size League den Weltmeistertitel erringen. Vor einigen Jahren hat Rojas mit seinem Team ein fahrerloses Auto (Spirit of Berlin) konzipiert. 2011 stellte er ein neues Modell "MadeInGermany" vor, das auf einem VW Passat basiert und seitdem auf zahlreichen Fahrten im öffentlichen Straßenverkehr getestet wurde. Dieses e-Book bietet dem Leser eine Sammlung von Essays über Kognitionswissenschaften, Mikroelektronik und Robotik, die in den Jahren 2011 bis 2013 in Telepolis erschienen sind. Wenn wir intelligente Maschinen bauen möchten, sollten wir als erstes die Intelligenz der Menschen und anderer Lebewesen unter der Lupe nehmen. So beschäftigen sich die Texte über das menschliche Gehirn mit der Struktur und Vernetzung unseren Neuronen, mit Messungen der neuronalen Aktivität und mit dem "Human Brain Project". Als Informatiker har Rojas seit Jahrzehnten die rasche Entwicklung der Mikroelektronik und die Möglichkeiten, die sie bietet, verfolgt, um intelligentes Verhalten in Maschinen nachzubauen. Das Mooresche Gesetz scheint sich immer wieder selbst am eigenen Schopf aus dem Sumpf zu ziehen, um alle technischen Schwierigkeiten zu überwinden. Milliarden von elektronischen Komponenten verbergen sich bereits in kleinsten Rechenmaschinen. Das Problem ist aber nun ein anderes, nämlich die Energiezufuhr zu garantieren und die übermäßige Wärmeentwicklung unter Kontrolle zu bringen. An der Stelle bleibt das biologische Vorbild immer noch unerreicht. Der dritte Teil über Robotik und KI gibt einen Einblick in die Arbeit, die in den letzten Jahren auf diesem Gebiet geleistet worden ist. Wir wären froh, mit Robotern die Eleganz eines Insekts bei der Bewältigung von Hindernissen zu erreichen. Wir können aber schon heute kleine und große Roboter - z.B. autonome Fahrzeuge - mit kognitiven Architekturen ausstatten, die eine effiziente und nützliche Funktionalität erlauben. Die Kapitel über Roboter, die lügen, bzw. über das Watson-System zeigen die zwei Seiten der Medaille: Wie weit die künstliche Intelligenz gekommen ist und wie weit entfernt sie doch noch vom Ziel bleibt.

Thema: Chips, Gedankenlesen, Künstliche Intelligenz, Roboter, Robotik

PowerChalk: An Adaptive e-Learning Application

Raúl Rojas, Dan-El Neil Vila Rosado, Margarita Esponda

Springer Verlag | 2013

Erschienen in: Multimedia and Internet Systems: Theory and Practice Advances in Intelligent Systems and Computing Volume 183.


This chapter presents a new interactive e-learning application called PowerChalk. PowerChalk has arisen as the result from the analysis of the evolution of Information Systems Design Theory for E-Learning; it was designed to resolve an important limitation of current design methods and e-learning systems: adaptability. Modular programming is the design technique used in PowerChalk to improve human computer interaction with the management of different types of data in order to have positive effect on both learning score and learning satisfaction. PowerChalk works like a Transaction Processing System in order to support collaboration, communication, creativity and learning through a collection of organized modules. The characteristics of PowerChalk facilitate developing of competencies for using multimedia technologies in any learning session, taking into account the teacher and student perspective. The goal of PowerChalk is to provide a robust, reliable, usable and sustainable multimedia technology for collaborative learning.

Thema: Multimedia technology; e-Learning; information systems; modular programming

Automated Consistency Checking of Expressive Ontologies

Christoph Benzmüller, Marco Ziener

Erschienen in: Proceedings of the 5th International Workshop on Acquisition, Representation and Reasoning with Contextualized Knowledge (ARCOE-LogIC 2013)


There have been attempts to (partially) translate expressive onotologies such as SUMO or Cyc to first-order logic and to use first-order automated theorem provers for detecting errors and inconsistencies. Claims have been made that these translation results are now ready for use within practival applications. This paper adopts a critical attitude: The fact that a translation of an expressive ontology into a target logic (be it first-order or higher-order or modal, etc.) exists for which satisfiability can be shown does not imply that the approach is ready for application. What might still be missing is a guarantee of the faithfulness of the translation. The issue is illustrated in connection with a (knowingly) unfaithful translation of SUMO into classical higher-order logic. The focus is on a small provably satisfiable subset of this translated SUMO ontology. By adding some intuitively compatible and sound ABox axioms the unfaithfulness of the translation can easily be revealed with automated theorem provers. Without he ABox content, however, the problem remains undetected. We thus argue for the extensive integration of ABox information into automated consistency checking for expressive ontologies, in particular, when logic translations are involved and when faithfulness has not or cannot be formally ensured.

Thema: Automated Reasoning, Ontology Reasoning, LEO Prover, Higher Order Logic

HOL based Universal Reasoing

C. Benzmüller

Handbook of the 4th World Congress and School on Universal Logic (UNILOG 2013), Rio de Janeiro, Brazil. | 2013


A Realistic Simulator for Humanoid Soccer Robot Using Particle Filter

Raúl Rojas, Fu Yao, Hamid Mobalegh, Longxu Jin, Miao Wang

Springer-Verlag, Heidelberg | 2013

Erschienen in: Recent Advances in Robotics and Automation, Studies in Computational Intelligence, Vol. 480.


This work presents a realistic simulator called Reality Sim for humanoid soccer robots especially in simulation of computer vision. As virtual training, testing and evaluating environment, simulation platforms have become one significant component in Soccer Robot projects. Nevertheless, the simulated environment in a simulation platform usually has a big gap with the realistic world. In order to solve this issue, we demonstrate a more realistic simulation system which is called Reality Sim with numerous real images. With this system, the computer vision code could be easily tested on the simulation platform. For this purpose, an image database with a large quantity of images recorded in various camera poses is built. Furthermore, if the camera pose of an image is not included in the database, an interpolation algorithm is used to reconstruct a brand-new realistic image of that pose such that a realistic image could be provided on every robot camera pose. Systematic empirical results illustrate the efficiency of the approach while it effectively simulates a more realistic environment for simulation so that it satisfies the requirement of humanoid soccer robot projects.

Sigma: An Integrated Development Environment for Formal Ontology

Christoph Benzmüller, Adam Pease

IOS Press | 2013

Erschienen in: AI Communications (Special Issue on Intelligent Engineering Techniques for Knowledge Bases), Vol. 26, No.1, 2013


Sigma is an open source environment for the development of logical theories. It has been under development and regular release for nearly a decade, and has been the principal environment under which the open source Suggested Upper Merged Ontology (SUMO) has been created. We discuss its features and evolution, and explain why it is an appropriate environment for the development of expressive ontologies in first and higher order logic.

Thema: formal ontology

Semi-autonomous Car Control Using Brain Computer Interfaces

Raúl Rojas, Daniel Goehring, David Latotzky, Miao Wang

Springer Verlag, Heidelberg | 2013

Erschienen in: Proceedings of the 12th International Conference IAS-12, held June 26-29, 2012, Jeju Island, Korea. Advances in Intelligent Systems and Computing, Volume 194.


In this paper we present an approach to control a real car with brain signals. To achieve this, we use a brain computer interface (BCI) which is connected to our autonomous car. The car is equipped with a variety of sensors and can be controlled by a computer. We implemented two scenarios to test the usability of the BCI for controlling our car. In the first scenario our car is completely brain controlled, using four different brain patterns for steering and throttle/brake. We will describe the control interface which is necessary for a smooth, brain controlled driving. In a second scenario, decisions for path selection at intersections and forkings are made using the BCI. Between these points, the remaining autonomous functions (e.g. path following and obstacle avoidance) are still active. We evaluated our approach in a variety of experiments on a closed airfield and will present results on accuracy, reaction times and usability.

Thema: interfaces, autonomous driving

High Level Sensor Data Fusion of Radar and Lidar for Car-Following on Highways

Daniel Goehring, Tinosch Ganjineh, Michael Schnürmacher, Miao Wang

Springer Verlag, Heidelberg | 2013

Erschienen in: Recent Advances in Robotics and Automation - Studies in Computational Intelligence Volume 480, 2013.


We present a real-time algorithm which enables an autonomous car to comfortably follow other cars at various speeds while keeping a safe distance. We focus on highway scenarios. A velocity and distance regulation approach is presented that depends on the position as well as the velocity of the followed car. Radar sensors provide reliable information on straight lanes, but fail in curves due to their restricted field of view. On the other hand, lidar sensors are able to cover the regions of interest in almost all situations, but do not provide precise speed information. We combine the advantages of both sensors with a sensor fusion approach in order to provide permanent and precise spatial and dynamical data. Our results in highway experiments with real traffic will be described in detail.

LEO-II Version 1.5

Christoph Benzmüller, Nik Sultana

Erschienen in: PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving.


LEO-II cooperates with other theorem-provers to prove theorems in classical higher-order logic. It returns hybrid proofs, containing inferences made by LEO-II as well as the backend provers with which it cooperates. This article describes recent improvements made to LEO-II.

Thema: higher-order logic, simple type theory, automatic theorem provers, prover cooperation, resolution

Controller Architecture for the Autonomous Cars

Daniel Goehring

Freie Universität Berlin | 2012-11

Erschienen in: Technical Reports - Serie B - Informatik, Fachbereich Mathematik und Informatik


In this paper a realtime controller architecture for our autonomous cars, a highly equipped conventional car and an electric vehicle is presented. The key aspects for controlling a car are stability, accuracy and smoothness, which constrain design critereas of all kinds on controller components. This report presents solutions for a variety of controller components, and aspects of a controller implementation of an autonomous car. The algorithms described proved their applicability in dense urban Berlin traffic as well as on the Berlin Autobahn.

Thema: Autonomous Cars, MadeInGermany, e-Instein

Shader-based sensor simulation for autonomous car testing

Raúl Rojas, Miao Wang, Shuiying Wang, Steffen Heinrich

IEEExplore Digital Library | 2012-10

Erschienen in: Proeedings of the 15th International IEEE Conference on Intelligent Transportation Systems

During autonomous car system development, sensor simulation can help to test and evaluate algorithms such as sensor fusion and object tracking in simulated dynamic scenarios at an early stage; thus, time and cost can be spared and more reliable system can be guaranteed. In this paper, shader-based LiDAR and Radar simulations are extended into autonomous car testing. Besides realizing sensor simulations producing information of interest scan data, conceptual programming interfaces to full featured physical models are also provided. Simulation accuracy is discussed and corresponding improvement methods are proposed. Optimistic results are displayed with a software-in-loop test for autonomous car and the computational cost is reported. Comparison between ray-tracing based and shader-based LiDAR simulation in terms of computational cost is also carried out and discussed.

Thema: sensor simulation autonomous car

Imitation of the Honeybee Dance Communication System by Means of a Biomimetic Robot

Raúl Rojas, Tim Landgraf, Michael Oertel, Andreas Kirbach, Randolf Menzel

Springer-Verlag, Heidelberg | 2012-07-09

Erschienen in: Proceedings of the First International Conference on Living Machines 2012, Barcelona, Spain, July 9-12, 2012. Lecture Notes in Computer Science, Vol. 7375


The honeybee dance communication system is one of the most intriguing examples of information transfer in the animal kingdom. After returning from a valuable food source honeybee foragers move vigorously, in a highly stereotypical pattern, on the comb surface conveying polar coordinates of the field site to a human observer. After 60 years of intense research it remains still unknown how the bees decode the dance. To resolve this question we have built a robotic honeybee that is able to reproduce all stimuli found to be generated in the dance ([12]). By imitating single stimuli or combinations and tracking the bees’ ensuing behavior we are able to identify essential signals in the communication process. In this paper we describe the design of our current prototype, show how we validated the function of the robotic wing buzzes and propose a reactive behavior control on the basis of relative body configurations of nearby bees measured by custom smart camera modules. We will conclude by showing first promising result of field experiments within a live honeybee colony.

Thema: imitation, honeybee dance

Quantified Multimodal Logics in Simple Type Theory

Christoph Benzmüller, L.C. Paulson

Logica Universalis (Special Issue on Multimodal Logics), Springer-Verlag | 2012


We present a straightforward embedding of quantified multimodal logic in simple type theory and prove its soundness and completeness. Modal operators are replaced by quantification over a type of possible worlds. We present simple experiments, using existing higher-order theorem provers, to demonstrate that the embedding allows automated proofs of statements in these logics, as well as meta properties of them.

Object Recognition Using Summed Features Classifier

Raúl Rojas, M. Lindner

Springer in the Lecture Notes in Artificial Intelligence series, Part I, LNCS 7267, presented to the 11th International Conference ICAISC 2012, Zakopane, Poland, April 29-May 3, 2012, Proceedings, Part I | 2012


A common task in the field of document digitization for information retrieval is separating text and non-text elements. In this paper an innovative approach of recognizing patterns is presented. Statistical and structural features in arbitrary number are combined into a rating tree, which is an adapted decision tree. Such a tree is trained for character patterns to distinguish text elements from non-text elements. First experiments in a binarization application have shown promising results in significant reduction of false-positives without producing false-negatives.

Thema: Object recognition, features classifier

Sign Language Recognition Using Kinect

Raúl Rojas, Simon Lang

Springer in the Lecture Notes in Artificial Intelligence series, Part I, LNCS 7267. 11th International Conference on Artificial Intelligence and Soft Computing (ICAISC 2012), Zakopane/Poland | 2012


An open source framework for general gesture recognition is presented and tested with isolated signs of sign language. Other than common systems for sign language recognition, this framework makes use of Kinect, a depth camera which makes real-time 3D-reconstruction easily applicable. Recognition is done using hidden Markov models with a continuous observation density. The framework also offers an easy way of initializing and training new gestures or signs by performing them several times in front of the camera. First results with a recognition rate of 97% show that depth cameras are well-suited for sign language recognition

Thema: Language recognition, Kinect

Higher-Order Aspects and Context in SUMO

Christoph Benzmüller, A. Pease

Erschienen in: Web Semantics: Science, Services and Agents on the World Wide Web (Special Issue on Reasoning with Context in the Semantic Web) 12-13, ISSN 1570-8268, Elsevier


This article addresses the automation of higher-order aspects in expressive ontologies such as the Suggested Upper Merged Ontology SUMO. Evidence is provided that modern higher-order automated theorem provers like LEO-II can be fruitfully employed for the task. A particular focus is on embedded formulas (formulas as terms), which are used in SUMO, for example, for modeling temporal, epistemic, or doxastic contexts. This modeling is partly in conflict with SUMO’s assumption of a bivalent, classical semantics and it may hence lead to counterintuitive reasoning results with automated theorem provers in practice. A solution is proposed that maps SUMO to quantified multimodal logic which is in turn modeled as a fragment of classical higher-order logic. This way automated higher-order theorem provers can be safely applied for reasoning about modal contexts in SUMO. Our findings are of wider relevance as they analogously apply to other expressive ontologies and knowledge representation formalisms.

Thema: Expressive ontologies; Context, Classical higher-order logic, Boolean extensionality, Quantified multimodal logic, Automated theorem proving

Embedding and automating conditional logics in classical higher-order logic

Christoph Benzmüller, Dov Gabbay, Valerio Genovese, and Daniele Rsipoli

Springer Verlag | 2012

Erschienen in: Annals of Mathematics and Artificial Intelligence. ISSN 1012-2443, Volume 66, Issue 1-4


A sound and complete embedding of conditional logics into classical higher-order logic is presented. This embedding enables the application of off-the-shelf higher-order automated theorem provers and model finders for reasoning within and about conditional logics.

Image Processing Framework for FPGAs

Raúl Rojas, Bennet Fischer

Erschienen in: Proceedings of the 2nd International Conference on Pervasive and Embedded Computing and Communication Systems (PECCS 2012), published in SciTePress

Research Gate

This paper presents a framework for computer vision tasks on Field Programmable Gate Arrays (FPGA) which allows rapid integration of vision algorithms by separating the framework from the vision algorithms. A vision system can be created by using plug-and-play methodology. On an abstract level several input and output channels of the system can be defined. Also, commonly used image transformations are modularized and can be added to the inputs or outputs of an algorithm. Special input and output modules allow the integration of algorithms with no knowledge of the surrounding framework. Image processing framework for fpgas: Introducing a plug-and-play computer vision framework for fast integration of algorithms in reconfigurable hardware.

Provers for First-order Modal Logics

Christoph Benzmüller, Jens Otten, Thomas Raths

IOS Press Ebooks | 2012

Erschienen in: Frontiers in Artificial Intelligence and Applications, Volume 242: ECAI 2012

pdf-DateiIOS Press Ebooks

While there is a broad literature on the theory of first-order modal logics, little is known about practical reasoning systems for them. This paper presents several implementations of fully automated theorem provers for first-order modal logics based on different proof calculi. Among these calculi are the standard sequent calculus, a prefixed tableau calculus, an embedding into simple type theory, an instance-based method, and a prefixed connection calculus. All implementations are tested and evaluated on the new QMLTP problem library for first-order modal logic.

Thema: Higher Order Logic, Semantic Embedding, Modal Logics, Automated Reasoning

Stereo camera based wearable reading device

Raúl Rojas, Noam Yogev, Roman Guilbourd

Erschienen in: Proceedings of the 3rd ACM Augmented Human International Conference (AH 2012)


The ability to access textual information is crucial for visually impaired people in terms of achieving greater independence in their everyday life. Thus, there is a need for a mobile easy-to-use reading device, capable of dealing with the complexity of the outdoor environment. In this paper a wearable camera-based solution is presented, aiming at improving the performance of existing systems through the use of stereo vision. Specific aspects of the stereo matching problem in document images are discussed and an approach for its integration into the document processing procedure is introduced. We conclude with the presentation of experimental results from a prototype system, which demonstrate the practical benefits of the presented approach.

Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order Logics

Dr. C. Benzmüller

Erschienen in: Annals of Mathematics and Artificial Intelligence (Special Issue Computational Logics in Multiagent Systems (CLIMA XI) 62(1-2)