MiG

Publications

76 Publikation(en)

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.

Leseprobe

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

C. Benzmüller

Erschienen in: Journal of Philosophical Logic

Manuskript

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

C. Benzmüller, A. Steen

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

Daniel Göhring, Raúl Rojas, Fritz Ulbrich, Simon Rotter

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

pdf-Datei

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 Göhring, 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.

IEEE-link

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

Is it Reasonable to Employ Agents in Theorem Proving?

Max Wisniewski, Christoph Benzmüller

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.

pdf-Datei

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

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

pdf-DateiFrontiers

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).

IEEE

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

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

Daniel Göhring, Hamma Tadjine

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

pdf-DateiProceedings[bib][slides]

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

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.

pdf-DateiFrontiers

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

Autonomer Rollstuhl

Adalberto Llarena, Bennet Fischer, Jose Alvarez-Ruiz

Springer Vieweg | 2015-08

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

Springer-link

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

Raúl Rojas, Bingyi Cao, Margarita Esponda

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.

IEEE

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

IEEE

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

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.

Springer-linkManuskript

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

pdf-DateiSpringer

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

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.

pdf-DateiSpringer[bib]

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.

Learning to Detect Visual Grasp Affordance

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

Erschienen in: IEEE Transactions on Automation and Engineering

pdf-Datei[bib]

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

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

Springerpdf-Datei

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.

pdf-Datei

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.

pdf-DateiElsevier

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.

pdf-Datei[bib][slides]

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

Cryptologiapdf-Datei

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

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

pdf-Dateievent-website[bib]

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.

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

ManuskriptIEEE-link[bib]

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

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

B-14-03

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.

Die Tiefe des Raumes

Die Tiefe des Raumes

Raúl Rojas

Heise Zeitschriften Verlag | 2014-06-04

Heise-Verlag

"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

arXivpdf-Datei

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)

pdf-Datei

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

pdf-Datei

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

pdf-DateiIJIET-link

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

Heise-Verlag

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

arXiv-linkpdf-Datei

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)

journal-linkpdf-Datei

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

C. Benzmüller

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

pdf-Dateievent-website

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

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.

Springer-linkManuskript

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

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

ManuskriptIEEE-link

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

event-website

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

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.

Springer-LinkManuskript

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

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

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.

Springer-LinkManuskript

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

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).

Springer-Linkpdf-Datei

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

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)

Online-Proceedingspdf-Datei

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

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

pdf-Datei

Computer Controlled Human Soccer League

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

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

CCHS

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

pdf-DateiSpringer-link

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.

Springer-Linkpdf-Datei

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

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.

Springer-Link

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

B-13-02

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

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.

Springer-linkManuskript

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.

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

IEEE-linkManuskript

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.

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.

Springer-linkManuskript

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

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

konnen-roboter-lugen-telepolis-187

Raúl Rojas

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

Heise-Verlag

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

LEO-II Version 1.5

C. Benzmüller, Nik Sultana

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

pdf-Datei

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

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.

ManuskriptSpringer-Link[bib]

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

A Top-down Approach to Combining Logics

C. Benzmüller

Barcelona, Spain: SciTePress | 2013

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

pdf-Datei

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

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.

Springer-Link[bib]

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.

Automated Consistency Checking of Expressive Ontologies

C. Benzmüller, Marco Ziener

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

pdf-Datei

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

Sigma: An Integrated Development Environment for Formal Ontology

C. 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

pdf-Datei

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

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

pdf-Datei

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

B-12-06

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

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

Springer-Link

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

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

Springer-Link

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

Higher-Order Aspects and Context in SUMO

C. 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

pdf-Datei

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

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)

pdf-Datei

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.

Provers for First-order Modal Logics

C. 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

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

pdf-Datei

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

Springer-Link

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

Embedding and automating conditional logics in classical higher-order logic

C. 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

arXiv

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.

Quantified Multimodal Logics in Simple Type Theory

Christoph Benzmüller, L.C. Paulson

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

arXiv

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.

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

C. Benzmüller

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

pdf-Datei