Kaiserslautern - Fachbereich Informatik
Refine
Year of publication
Document Type
- Article (134) (remove)
Has Fulltext
- yes (134)
Keywords
- AG-RESY (42)
- PARO (30)
- SKALP (15)
- HANDFLEX (8)
- CoMo-Kit (6)
- Robotik (5)
- motion planning (5)
- SIMERO (4)
- Wissensverarbeitung (4)
- industrial robots (4)
Faculty / Organisational entity
In this paper we present the results of the project “#Datenspende” where during the German election in 2017 more than 4000 people contributed their search results regarding keywords connected to the German election campaign.
Analyzing the donated result lists we prove, that the room for personalization of the search results is very small. Thus the opportunity for the effect mentioned in Eli Pariser’s filter bubble theory to occur in this data is also very small, to a degree that it is negligible. We achieved these results by applying various similarity measures to the result lists that were donated. The first approach using the number of common results as a similarity measure showed that the space for personalization is less than two results out of ten on average when searching for persons and at most four regarding the search for parties. Application of other, more specific measures show that the space is indeed smaller, so that the presence of filter bubbles is not evident.
Moreover this project is also a proof of concept, as it enables society to permanently monitor a search engine’s degree of personalization for any desired search terms. The general design can also be transferred to intermediaries, if appropriate APIs restrict selective access to contents relevant to the study in order to establish a similar degree of trustworthiness.
Virtual Robot Programming for Deformable Linear Objects: System concept and Prototype Implementation
(2002)
In this paper we present a method and system for robot programming using virtual reality techniques. The proposed method allows intuitive teaching of a manipulation task with haptic feedback in a graphical simulation system. Based on earlier work, our system allows even an operator who lacks specialized knowledge of robotics to automatically generate a robust sensor-based robot program that is ready to execute on different robots, merely by demonstrating the task in virtual reality.
In diesem Papier beschreiben wir eine Methode zur Spezifikation und Operationalisierung von konzeptuellen Modellen kooperativer wissensbasierter Arbeitsabläufe. Diese erweitert bekannte Ansätze um den Begriff des Agenten und um alternative Aufgabenzerlegungen. Das Papier beschreibt schwerpunktmäßig Techniken, die unserem verteilten Interpreter zugrunde liegen. Dabei gehen wir insbesondere auf Methoden ein, die Abhängigkeiten zwischen Aufgaben behandeln und ein zielgerichtetes Backtracking effizient unterstützen.
3D joint kinematics can provide important information about the quality of movements. Optical motion capture systems (OMC) are considered the gold standard in motion analysis. However, in recent years, inertial measurement units (IMU) have become a promising alternative. The aim of this study was to validate IMU-based 3D joint kinematics of the lower extremities during different movements. Twenty-eight healthy subjects participated in this study. They performed bilateral squats (SQ), single-leg squats (SLS) and countermovement jumps (CMJ). The IMU kinematics was calculated using a recently-described sensor-fusion algorithm. A marker based OMC system served as a reference. Only the technical error based on algorithm performance was considered, incorporating OMC data for the calibration, initialization, and a biomechanical model. To evaluate the validity of IMU-based 3D joint kinematics, root mean squared error (RMSE), range of motion error (ROME), Bland-Altman (BA) analysis as well as the coefficient of multiple correlation (CMC) were calculated. The evaluation was twofold. First, the IMU data was compared to OMC data based on marker clusters; and, second based on skin markers attached to anatomical landmarks. The first evaluation revealed means for RMSE and ROME for all joints and tasks below 3°. The more dynamic task, CMJ, revealed error measures approximately 1° higher than the remaining tasks. Mean CMC values ranged from 0.77 to 1 over all joint angles and all tasks. The second evaluation showed an increase in the RMSE of 2.28°– 2.58° on average for all joints and tasks. Hip flexion revealed the highest average RMSE in all tasks (4.87°– 8.27°). The present study revealed a valid IMU-based approach for the measurement of 3D joint kinematics in functional movements of varying demands. The high validity of the results encourages further development and the extension of the present approach into clinical settings.
In diesem Papier stellen wir einen Interpreter vor, der die Validierung von konzeptuellen Modellen bereits in fruehen Entwicklungsphasen unterstuetzt. Wir vergleichen Hypermedia- und Expertensystemansaetze zur Wissensverarbeitung und erlaeutern, wie ein integrierter Ansatz die Erstellung von Expertensystemen vereinfacht. Das von uns entwickelte Knowledge Engineering Werkzeug ermoeglicht einen "sanften" Uebergang von initialen Protokollen ueber eine semi-formale Spezifikation in Form eines getypten Hypertextes hin zu einem operationalen Expertensystem. Ein Interpreter nutzt die in diesem Prozess erzeugte Zwischenrepraesentation direkt zur interaktiven Loesung von Problemen, wobei einzelne Aufgaben ueber ein lokales Rechnernetz auf die Bearbeiter verteilt werden. Das heisst, die Spezifikation des Expertensystems wird direkt fuer die Loesung realer Probleme eingesetzt. Existieren zu einzelnen Teilaufgaben Operationalisierungen (d.h. Programme), dann werden diese vom Computer bearbeitet.
Typical instances, that is, instances that are representative for a particular situ-ation or concept, play an important role in human knowledge representationand reasoning, in particular in analogical reasoning. This wellADknown obser-vation has been a motivation for investigations in cognitive psychology whichprovide a basis for our characterization of typical instances within conceptstructures and for a new inference rule for justified analogical reasoning withtypical instances. In a nutshell this paper suggests to augment the proposi-tional knowledge representation system by a non-propositional part consistingof concept structures which may have directly represented instances as ele-ments. The traditional reasoning system is extended by a rule for justifiedanalogical inference with typical instances using information extracted fromboth knowledge representation subsystems.
Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading
(1999)
We develop an order-sorted higher-order calculus suitable forautomatic theorem proving applications by extending the extensional simplytyped lambda calculus with a higher-order ordered sort concept and constantoverloading. Huet's well-known techniques for unifying simply typed lambdaterms are generalized to arrive at a complete transformation-based unificationalgorithm for this sorted calculus. Consideration of an order-sorted logicwith functional base sorts and arbitrary term declarations was originallyproposed by the second author in a 1991 paper; we give here a correctedcalculus which supports constant rather than arbitrary term declarations, aswell as a corrected unification algorithm, and prove in this setting resultscorresponding to those claimed there.
The introduction of sorts to first-order automated deduc-tion has brought greater conciseness of representation and a considerablegain in efficiency by reducing search spaces. This suggests that sort in-formation can be employed in higher-order theorem proving with similarresults. This paper develops a sorted (lambda)-calculus suitable for automatictheorem proving applications. It extends the simply typed (lambda)-calculus by ahigher-order sort concept that includes term declarations and functionalbase sorts. The term declaration mechanism studied here is powerfulenough to subsume subsorting as a derived notion and therefore gives ajustification for the special form of subsort inference. We present a set oftransformations for sorted (pre-) unification and prove the nondetermin-istic completeness of the algorithm induced by these transformations.
In many applications, visual analytics (VA) has developed into a standard tool to ease data access and knowledge generation. VA describes a holistic cycle transforming data into hypothesis and visualization to generate insights that enhance the data. Unfortunately, many data sources used in the VA process are affected by uncertainty. In addition, the VA cycle itself can introduce uncertainty to the knowledge generation process but does not provide a mechanism to handle these sources of uncertainty. In this manuscript, we aim to provide an extended VA cycle that is capable of handling uncertainty by quantification, propagation, and visualization, defined as uncertainty-aware visual analytics (UAVA). Here, a recap of uncertainty definition and description is used as a starting point to insert novel components in the visual analytics cycle. These components assist in capturing uncertainty throughout the VA cycle. Further, different data types, hypothesis generation approaches, and uncertainty-aware visualization approaches are discussed that fit in the defined UAVA cycle. In addition, application scenarios that can be handled by such a cycle, examples, and a list of open challenges in the area of UAVA are provided.
Most automated theorem provers suffer from the problemthat the resulting proofs are difficult to understand even for experiencedmathematicians. An effective communication between the system andits users, however, is crucial for many applications, such as in a mathematical assistant system. Therefore, efforts have been made to transformmachine generated proofs (e.g. resolution proofs) into natural deduction(ND) proofs. The state-of-the-art procedure of proof transformation fol-lows basically its completeness proof: the premises and the conclusionare decomposed into unit literals, then the theorem is derived by mul-tiple levels of proofs by contradiction. Indeterminism is introduced byheuristics that aim at the production of more elegant results. This inde-terministic character entails not only a complex search, but also leads tounpredictable results.In this paper we first study resolution proofs in terms of meaningful op-erations employed by human mathematicians, and thereby establish acorrespondence between resolution proofs and ND proofs at a more ab-stract level. Concretely, we show that if its unit initial clauses are CNFsof literal premises of a problem, a unit resolution corresponds directly toa well-structured ND proof segment that mathematicians intuitively un-derstand as the application of a definition or a theorem. The consequenceis twofold: First it enhances our intuitive understanding of resolutionproofs in terms of the vocabulary with which mathematicians talk aboutproofs. Second, the transformation process is now largely deterministicand therefore efficient. This determinism also guarantees the quality ofresulting proofs.
Patients after total hip arthroplasty (THA) suffer from lingering musculoskeletal restrictions. Three-dimensional (3D) gait analysis in combination with machine-learning approaches is used to detect these impairments. In this work, features from the 3D gait kinematics, spatio temporal parameters (Set 1) and joint angles (Set 2), of an inertial sensor (IMU) system are proposed as an input for a support vector machine (SVM) model, to differentiate impaired and non-impaired gait. The features were divided into two subsets. The IMU-based features were validated against an optical motion capture (OMC) system by means of 20 patients after THA and a healthy control group of 24 subjects. Then the SVM model was trained on both subsets. The validation of the IMU system-based kinematic features revealed root mean squared errors in the joint kinematics from 0.24° to 1.25°. The validity of the spatio-temporal gait parameters (STP) revealed a similarly high accuracy. The SVM models based on IMU data showed an accuracy of 87.2% (Set 1) and 97.0% (Set 2). The current work presents valid IMU-based features, employed in an SVM model for the classification of the gait of patients after THA and a healthy control. The study reveals that the features of Set 2 are more significant concerning the classification problem. The present IMU system proves its potential to provide accurate features for the incorporation in a mobile gait-feedback system for patients after THA.
Background: The use of health apps to support the treatment of chronic pain is gaining importance. Most available pain management apps are still lacking in content quality and quantity as their developers neither involve health experts to ensure target group suitability nor use gamification to engage and motivate the user. To close this gap, we aimed to develop a gamified pain management app, Pain-Mentor.
Objective: To determine whether medical professionals would approve of Pain-Mentor’s concept and content, this study aimed to evaluate the quality of the app’s first prototype with experts from the field of chronic pain management and to discover necessary improvements.
Methods: A total of 11 health professionals with a background in chronic pain treatment and 2 mobile health experts participated in this study. Each expert first received a detailed presentation of the app. Afterward, they tested Pain-Mentor and then rated its quality using the mobile application rating scale (MARS) in a semistructured interview.
Results: The experts found the app to be of excellent general (mean 4.54, SD 0.55) and subjective quality (mean 4.57, SD 0.43). The app-specific section was rated as good (mean 4.38, SD 0.75). Overall, the experts approved of the app’s content, namely, pain and stress management techniques, behavior change techniques, and gamification. They believed that the use of gamification in Pain-Mentor positively influences the patients’ motivation and engagement and thus has the potential to promote the learning of pain management techniques. Moreover, applying the MARS in a semistructured interview provided in-depth insight into the ratings and concrete suggestions for improvement.
Conclusions: The experts rated Pain-Mentor to be of excellent quality. It can be concluded that experts perceived the use of gamification in this pain management app in a positive manner. This showed that combining pain management with gamification did not negatively affect the app’s integrity. This study was therefore a promising first step in the development of Pain-Mentor.
Using an experience factory is one possible concept for supporting and improving reuse in software development. (i.e., reuse of products, processes, quality models, ...). In the context of the Sonderforschungsbereich 501: "Development of Large Systems with Generic methods" (SFB501), the Software Engineering Laboratory (SE Lab) runs such an experience factory as part of the infrastructure services it offers. The SE Lab also provides several tools to support the planning, developing, measuring, and analyzing activities of software development processes. Among these tools, the SE Lab runs and maintains an experience base, the SFB-EB. When an experience factory is utilized, support for experience base maintenance is an important issue. Furthermore, it might be interesting to evaluate experience base usage with regard to the number of accesses to certain experience elements stored in the database. The same holds for the usage of the tools provided by the SE LAB. This report presents a set of supporting tools that were designed to aid in these tasks. These supporting tools check the experience base's consistency and gather information on the usage of SFB-EB and the tools installed in the SE Lab. The results are processed periodically and displayed as HTML result reports (consistency checking) or bar charts (usage profiles).
Comprehensive reuse and systematic evolution of reuse artifacts as proposed by the Quality Improvement Paradigm (QIP) do not only require tool support for mere storage and retrieval. Rather, an integrated management of (potentially reusable) experience data as well as project-related data is needed. This paper presents an approach exploiting object-relational database technology to implement the QIP-driven reuse repository of the SFB 501. Requirements, concepts, and implementational aspects are discussed and illustrated through a running example, namely the reuse and continuous improvement of SDL patterns for developing distributed systems. Based on this discussion, we argue that object-relational database management systems (ORDBMS) are best suited to implement such a comprehensive reuse repository. It is demonstrated how this technology can be used to support all phases of a reuse process and the accompanying improvement cycle. Although the discussions of this paper are strongly related to the requirements of the SFB 501 experience base, the basic realization concepts, and, thereby, the applicability of ORDBMS, can easily be extended to similar applications, i. e., reuse repositories in general.
Load balancing is one of the central problems that have to be solved in parallel computation. Here, the problem of distributed, dynamic load balancing for massive parallelism is addressed. A new local method, which realizes a physical analogy to equilibrating liquids in multi-dimensional tori or hypercubes, is presented. It is especially suited for communication mechanisms with low set-up to transfer ratio occurring in tightly-coupled or SIMD systems. By successive shifting single load elements to the direct neighbors, the load is automatically transferred to lightly loaded processors. Compared to former methods, the proposed Liquid model has two main advantages. First, the task of load sharing is combined with the task of load balancing, where the former has priority. This property is valuable in many applications and important for highly dynamic load distribution. Second, the Liquid model has high efficiency. Asymptotically, it needs O(D . K . Ldiff ) load transfers to reach the balanced state in a D-dimensional torus with K processors per dimension and a maximum initial load difference of Ldiff . The Liquid model clearly outperforms an earlier load balancing approach, the nearest-neighbor-averaging. Besides a survey of related research, analytical results within a formal framework are derived. These results are validated by worst-case simulations in one-and two-dimensional tori with up to two thousand processors.
We describe a platform for the portable and secure execution of mobile agents writtenin various interpreted languages on top of a common run-time core. Agents may migrate at anypoint in their execution, fully preserving their state, and may exchange messages with otheragents. One system may contain many virtual places, each establishing a domain of logicallyrelated services under a common security policy governing all agents at this place. Agents areequipped with allowances limiting their resource accesses, both globally per agent lifetime andlocally per place. We discuss aspects of this architecture and report about ongoing work.
Versions- und Konfigurationsmanagement sind zentrale Instrumente zur intellektuellen Beherrschung komplexer Softwareentwicklungen. In stark wiederverwendungsorientierten Softwareentwicklungsansätzen -wie vom SFB bereitgestellt- muß der Begriff der Konfiguration von traditionell produktorientierten Artefakten auf Prozesse und sonstige Entwicklungserfahrungen erweitert werden. In dieser Veröffentlichung wird ein derartig erweitertes Konfigurationsmodell vorgestellt. Darüberhinau wird eine Ergänzung traditioneller Projektplanungsinformationen diskutiert, die die Ableitung maßgeschneiderter Versions- und Konfigurationsmanagementmechanismen vor Projektbeginn ermöglichen.
Dataflow process networks (DPNs) are intrinsically data-driven, i.e., node actions are not synchronized among each other and may fire whenever sufficient input operands arrived at a node. While the general model of computation (MoC) of DPNs does not impose further restrictions, many different subclasses of DPNs representing different dataflow MoCs have been considered over time. These classes mainly differ in the kinds of behaviors of the processes. A DPN may be heterogeneous in that different processes in the network belong to different classes of DPNs. A heterogeneous DPN can therefore be effectively used to model and to implement different components of a system with different kinds of processes and, therefore, different dataflow MoCs. This paper presents a model-based design based on different dataflow MoCs including their heterogeneous combinations. In particular, it covers the automatic software synthesis of systems from DPN models. The main objective is to validate, evaluate and compare the artifacts exhibited by different dataflow MoCs at the implementation level of systems under the supervision of a common design tool. Moreover, this work also offers an efficient synthesis method that targets and exploits heterogeneity in DPNs by generating implementations based on the kinds of behaviors of the processes. The proposed synthesis method provides a tool chain including different specialized code generators for specific dataflow MoCs, and a runtime system that finally maps models using a combination of different dataflow MoCs on cross-vendor target hardware.
Struktur und Werkzeuge des experiment-spezifischen Datenbereichs der SFB501 Erfahrungsdatenbank
(1999)
Software-Entwicklungsartefakte müssen zielgerichtet während der Durchführung eines Software- Projekts erfasst werden, um für die Wiederverwendung aufbereitet werden zu können. Die methodische Basis hierzu bildet im Sonderforschungsbereich 501 das Konzept der Erfahrungsdatenbank. In ihrem experiment-spezifischen Datenbereich werden für jedes Entwicklungsprojekt alle Software-Entwicklungsartefakte abgelegt, die während des Lebenszyklus eines Projektes anfallen. In ihrem übergreifenden Datenbereich werden all die jenigen Artefakte aus dem experiment-spezifischen Datenbereich zusammengefasst, die für eine Wiederverwendung in nachfolgenden Projekten in Frage kommen. Es hat sich gezeigt, dass bereits zur Nutzung der Datenmengen im experiment- spezifischen Datenbereich der Erfahrungsdatenbank ein systematischer Zugriff notwendig ist. Ein systematischer Zugriff setzt jedoch eine normierte Struktur voraus. Im experiment-spezifischen Bereich werden zwei Arten von Experimenttypen unterschieden: "Kontrollierte Experimente" und "Fallstudien". Dieser Bericht beschreibt die Ablage- und Zugriffsstruktur für den Experimenttyp "Fallstudien". Die Struktur wurde aufgrund der Erfahrungen in ersten Fallstudien entwickelt und evaluiert.
About the approach The approach of TOPO was originally developed in the FABEL project1[1] to support architects in designing buildings with complex installations. Supplementing knowledge-based design tools, which are available only for selected subtasks, TOPO aims to cover the whole design process. To that aim, it relies almost exclusively on archived plans. Input to TOPO is a partial plan, and output is an elaborated plan. The input plan constitutes the query case and the archived plans form the case base with the source cases. A plan is a set of design objects. Each design object is defined by some semantic attributes and by its bounding box in a 3-dimensional coordinate system. TOPO supports the elaboration of plans by adding design objects.
In order to reduce the elapsed time of a computation, a pop-ular approach is to decompose the program into a collection of largelyindependent subtasks which are executed in parallel. Unfortunately, it isoften observed that tightly-coupled parallel programs run considerablyslower than initially expected. In this paper, a framework for the anal-ysis of parallel programs and their potential speedup is presented. Twoparameters which strongly affect the scalability of parallelism are iden-tified, namely the grain of synchronization, and the degree to which thetarget hardware is available. It is shown that for certain classes of appli-cations speedup is inherently poor, even if the program runs under theidealized conditions of perfect load balance, unbounded communicationbandwidth and negligible communication and parallelization overhead.Upper bounds are derived for the speedup that can be obtained in threedifferent types of computations. An example illustrates the main find-ings.
This paper presents fill algorithms for boundary-defined regions in raster graphics. The algorithms require only a constant size working memory. The methods presented are based on the so-called "seed fill" algorithms using the internal connectivity of the region with a given inner point. Basic methods as well as additional heuristics for speeding up the algorithm are described and verified. For different classes of regions, the time complexity of the algorithms is compared using empirical results.
Extending existing calculi by sorts is astrong means for improving the deductive power offirst-order theorem provers. Since many mathemat-ical facts can be more easily expressed in higher-orderlogic - aside the greater power of higher-order logicin principle - , it is desirable to transfer the advant-ages of sorts in the first-order case to the higher-ordercase. One possible method for automating higher-order logic is the translation of problem formulationsinto first-order logic and the usage of first-order the-orem provers. For a certain class of problems thismethod can compete with proving theorems directlyin higher-order logic as for instance with the TPStheorem prover of Peter Andrews or with the Nuprlproof development environment of Robert Constable.There are translations from unsorted higher-order lo-gic based on Church's simple theory of types intomany-sorted first-order logic, which are sound andcomplete with respect to a Henkin-style general mod-els semantics. In this paper we extend correspond-ing translations to translations of order-sorted higher-order logic into order-sorted first-order logic, thus weare able to utilize corresponding first-order theoremprover for proving higher-order theorems. We do notuse any (lambda)-expressions, therefore we have to add so-called comprehension axioms, which a priori makethe procedure well-suited only for essentially first-order theorems. However, in practical applicationsof mathematics many theorems are essentially first-order and as it seems to be the case, the comprehen-sion axioms can be mastered too.
An important research problem is the incorporation of "declarative" knowledge into an automated theorem prover that can be utilized in the search for a proof. An interesting pro-posal in this direction is Alan Bundy's approach of using explicit proof plans that encapsulatethe general form of a proof and is instantiated into a particular proof for the case at hand. Wegive some examples that show how a "declarative" highlevel description of a proof can be usedto find proofs of apparently "similiar" theorems by analogy. This "analogical" information isused to select the appropriate axioms from the database so that the theorem can be proved.This information is also used to adjust some options of a resolution theorem prover. In orderto get a powerful tool it is necessary to develop an epistemologically appropriate language todescribe proofs, for which a large set of examples should be used as a testbed. We presentsome ideas in this direction.
IoT systems consist of Hardware/Software systems (e.g., sensors) that are embedded in a physical world, networked and that interact with complex software platforms. The validation of such systems is a challenge and currently mostly done by prototypes. This paper presents the virtual environment for simulation, emulation and validation of an IoT platform and its semantic model in real life scenarios. It is based on a decentralized, bottom up approach that offers interoperability of IoT devices and the value-added services they want to use across different domains. The framework is demonstrated by a comprehensive case study. The example consists of the complete IoT “Smart Energy” use case with focus on data privacy by homomorphic encryption. The performance of the network is compared while using partially homomorphic encryption, fully homomorphic encryption and no encryption at all.As a major result, we found that our framework is capable of simulating big IoT networks and the overhead introduced by homomorphic encryption is feasible for VICINITY.
Den in der industriellen Produktion eingesetzten Manipulatoren fehlt in der Regel die Möglichkeit, ihre Umwelt wahrzunehmen. Damit Mensch und Roboter in einem gemeinsamen Arbeitsraum arbeiten können, wird im SIMERO-System die Transferbewegung des Roboters durch Kameras abgesichert. Dieses Kamerasystem wird auf Ausfall überprüft. Dabei werden Fehler in der Bildübertragung und Positionierungsfehler der Kameras betrachtet.
Zur Zeit haben Industrieroboter nur eine sehr begrenzte Wahrnehmung ihrer Umwelt. Wenn sich Menschen im Arbeitsraum des Roboters aufhalten sind sie daher gefährdet. Durch eine Einteilung der möglichen Roboterbewegung in verschiedene Klassen kann gezeigt werden, dass die für einen Menschen im Arbeitsraum gefährlichste Bewegung die freie Transferbewegung ist. Daher besteht die betrachtete Aufgabe darin, diese Transferbewegung eines Manipulators durchzuführen, ohne mit dynamischen Hindernissen, wie zum Beispiel Menschen, zu kollidieren. Das SIMERO-System gliedert sich in die vier Hauptkomponenten Bildverarbeitung, Robotermodellierung, Kollisionserkennung und Bahnplanung. Diese Komponenten werden im einzelnen vorgestellt. Die Leistungsfähigkeit des Systems und die weiteren Verbesserungen werden an einem Versuch exemplarisch gezeigt.
We present a system concept allowing humans to work safely in the same environment as a robot manipulator. Several cameras survey the common workspace. A look-up-table-based fusion algorithm is used to back-project directly from the image spaces of the cameras to the manipulator?s con-figuration space. In the look-up-tables both, the camera calibration and the robot geometry are implicitly encoded. For experiments, a conven-tional 6 axis industrial manipulator is used. The work space is surveyed by four grayscale cameras. Due to the limits of present robot controllers, the computationally expensive parts of the system are executed on a server PC that communicates with the robot controller via Ethernet.
This paper analyzes the problem of sensor-based colli-sion detection for an industrial robotic manipulator. A method to perform collision tests based on images taken from several stationary cameras in the work cell is pre-sented. The collision test works entirely based on the im-ages, and does not construct a representation of the Carte-sian space. It is shown how to perform a collision test for all possible robot configurations using only a single set of images taken simultaneously.
Die Domäne der Operationsroboter liegt heute in Fräsarbeiten an knöchernen Strukturen. Da Roboter über eine extreme Präzision verfügen und nicht ermüden bietet sich ihr Einsatz ins-besondere bei langwierigen und zugleich hochpräzisen Fräsvorgängen im Bereich der lateralen Schädelbasis an. Aus diesem Grunde wurde ein Verfahren entwickelt, welches aus einer geometrischen Beschreibung des Implantates eine geeignete Fräsbahn errechnet und eine kraftgeregelte Prozesskontrolle des Fräsvorganges implementiert. Mit einem 6*achsigen Knickarmroboter erfolgten die Untersuchungen primär an Tierpräparaten und zur Optimierung an Felsenbeinpräparaten.
In this paper, we compare the BERKOM globally ac-cessible services project (GLASS) with the well-knownWorld-Wide Web with respect to the ease of development,realization, and distribution of multimedia presentations.This comparison is based on the experiences we gainedwhen implementing a gateway between GLASS and theWorld-Wide Web. Since both systems are shown to haveobvious weaknesses, we are concluding this paper with apresentation of a better way to multimedia document en-gineering and distribution. This concept is based on awell-accepted approach to function-shipping in the Inter-net: the Java language, permitting for example a smoothintegration of GLASS92 MHEG objects and WWW HTMLpages within one common environment.
Structured domains are characterized by the fact that there is an intrinsic dependency between certain key elements in the domain. Considering these dependencies leads to better performance of the planning systems, and it is an important factor for determining the relevance of the cases stored in a case-base. However, testing for cases that meet these dependencies, decreases the performance of case-based planning, as other criterions need also to be consider for determining this relevance. We present a domain-independent architecture that explicitly represents these dependencies so that retrieving relevant cases is ensured without negatively affecting the performance of the case-based planning process.
A straightforward formulation of a mathematical problem is mostly not ad-equate for resolution theorem proving. We present a method to optimize suchformulations by exploiting the variability of first-order logic. The optimizingtransformation is described as logic morphisms, whose operationalizations aretactics. The different behaviour of a resolution theorem prover for the sourceand target formulations is demonstrated by several examples. It is shown howtactical and resolution-style theorem proving can be combined.
Most automated theorem provers suffer from the problem thatthey can produce proofs only in formalisms difficult to understand even forexperienced mathematicians. Effort has been made to reconstruct naturaldeduction (ND) proofs from such machine generated proofs. Although thesingle steps in ND proofs are easy to understand, the entire proof is usuallyat a low level of abstraction, containing too many tedious steps. To obtainproofs similar to those found in mathematical textbooks, we propose a newformalism, called ND style proofs at the assertion level , where derivationsare mostly justified by the application of a definition or a theorem. Aftercharacterizing the structure of compound ND proof segments allowing asser-tion level justification, we show that the same derivations can be achieved bydomain-specific inference rules as well. Furthermore, these rules can be rep-resented compactly in a tree structure. Finally, we describe a system calledPROVERB , which substantially shortens ND proofs by abstracting them tothe assertion level and then transforms them into natural language.
The hallmark of traditional Artificial Intelligence (AI) research is the symbolic representation and processing of knowledge. This is in sharp contrast to many forms of human reasoning, which to an extraordinary extent, rely on cases and (typical) examples. Although these examples could themselves be encoded into logic, this raises the problem of restricting the corresponding model classes to include only the intended models.There are, however, more compelling reasons to argue for a hybrid representa-tion based on assertions as well as examples. The problems of adequacy, availability of information, compactness of representation, processing complexity, and last but not least, results from the psychology of human reasoning, all point to the same conclusion: Common sense reasoning requires different knowledge sources and hybrid reasoning principles that combine symbolic as well as semantic-based inference. In this paper we address the problem of integrating semantic representations of examples into automateddeduction systems. The main contribution is a formal framework for combining sentential with direct representations. The framework consists of a hybrid knowledge base, made up of logical formulae on the one hand and direct representations of examples on the other, and of a hybrid reasoning method based on the resolution calculus. The resulting hybrid resolution calculus is shown to be sound and complete.
We have presented a novel approach to parallel motion planning for robot manipulators in 3D workspaces. The approach is based on arandomized parallel search algorithm and focuses on solving the path planning problem for industrial robot arms working in a reasonably cluttered workspace. The path planning system works in the discretized con guration space, which needs not to be represented explicitly. The parallel search is conducted by a number of rule-based sequential search processes, which work to find a path connecting the initial con guration to the goal via a number of randomly generated subgoal con gurations. Since the planning performs only on-line collision tests with proper proximity information without using pre-computed information, the approach is suitable for planning problems with multirobot or dynamic environments. The implementation has been carried outontheparallel virtual machine (PVM) of a cluster of SUN4 workstations and SGI machines. The experimental results have shown that the approach works well for a 6-dof robot arm in a reasonably cluttered environment, and that parallel computation increases the e ciency of motion planning signi cantly.
Since the h-index has been invented, it is the most frequently discussed bibliometric value and one of the most commonly used metrics to quantify a researcher’s scientific output. The more it is increasingly gaining popularity to use the metric as an indication of the quality of a job applicant or an employee the more important it is to assure its correctitude. Many platforms offer the h-index of a scientist as a service, sometimes without the explicit knowledge of the respective person. In this article we show that looking up the h-index for a researcher on the five most commonly used platforms, namely AMiner, Google Scholar, ResearchGate, Scopus and Web of Science, results in a variance that is in many cases as large as the average value. This is due to the varying definitions of what a scientific article is, the underlying data basis, and different qualities of the entity recognition problem. To perform our study, we crawled the h-index of the worlds top researchers according to two different rankings, all the Nobel Prize laureates except Literature and Peace, and the teaching staff of the computer science department of the TU Kaiserslautern Germany with whom we additionally computed their h-index manually. Thus we showed that the individual h-indices differ to an alarming extent between the platforms. We observed that researchers with an extraordinary high h-index and researchers with an index appropriate to the scientific career path and the respective scientific field are affected alike by these problems.
Postmortem Analysis of Decayed Online Social Communities: Cascade Pattern Analysis and Prediction
(2018)
Recently, many online social networks, such as MySpace, Orkut, and Friendster, have faced inactivity decay of their members, which contributed to the collapse of these networks. The reasons, mechanics, and prevention mechanisms of such inactivity decay are not fully understood. In this work, we analyze decayed and alive subwebsites from the Stack Exchange platform. The analysis mainly focuses on the inactivity cascades that occur among the members of these communities. We provide measures to understand the decay process and statistical analysis to extract the patterns that accompany the inactivity decay. Additionally, we predict cascade size and cascade virality using machine learning. The results of this work include a statistically significant difference of the decay patterns between the decayed and the alive subwebsites. These patterns are mainly cascade size, cascade virality, cascade duration, and cascade similarity. Additionally, the contributed prediction framework showed satisfactorily prediction results compared to a baseline predictor. Supported by empirical evidence, the main findings of this work are (1) there are significantly different decay patterns in the alive and the decayed subwebsites of the Stack Exchange; (2) the cascade’s node degrees contribute more to the decay process than the cascade’s virality, which indicates that the expert members of the Stack Exchange subwebsites were mainly responsible for the activity or inactivity of the Stack Exchange subwebsites; (3) the Statistics subwebsite is going through decay dynamics that may lead to it becoming fully-decayed; (4) the decay process is not governed by only one network measure, it is better described using multiple measures; (5) decayed subwebsites were originally less resilient to inactivity decay, unlike the alive subwebsites; and (6) network’s structure in the early stages of its evolution dictates the activity/inactivity characteristics of the network.
This paper deals with the reference choices involved in thegeneration of argumentative text. A piece of argument-ative text such as the proof of a mathematical theoremconveys a sequence of derivations. For each step of de-rivation, the premises (previously conveyed intermediateresults) and the inference method (such as the applica-tion of a particular theorem or definition) must be madeclear. The appropriateness of these references cruciallyaffects the quality of the text produced.Although not restricted to nominal phrases, our refer-ence decisions are similar to those concerning nominalsubsequent referring expressions: they depend on theavailability of the object referred to within a context andare sensitive to its attentional hierarchy . In this paper,we show how the current context can be appropriatelysegmented into an attentional hierarchy by viewing textgeneration as a combination of planned and unplannedbehavior, and how the discourse theory of Reichmann canbe adapted to handle our special reference problem.
In this article we formally describe a declarative approach for encoding plan operatorsin proof planning, the so-called methods. The notion of method evolves from the much studiedconcept tactic and was first used by Bundy. While significant deductive power has been achievedwith the planning approach towards automated deduction, the procedural character of the tacticpart of methods, however, hinders mechanical modification. Although the strength of a proofplanning system largely depends on powerful general procedures which solve a large class ofproblems, mechanical or even automated modification of methods is nevertheless necessary forat least two reasons. Firstly methods designed for a specific type of problem will never begeneral enough. For instance, it is very difficult to encode a general method which solves allproblems a human mathematician might intuitively consider as a case of homomorphy. Secondlythe cognitive ability of adapting existing methods to suit novel situations is a fundamentalpart of human mathematical competence. We believe it is extremely valuable to accountcomputationally for this kind of reasoning.The main part of this article is devoted to a declarative language for encoding methods,composed of a tactic and a specification. The major feature of our approach is that the tacticpart of a method is split into a declarative and a procedural part in order to enable a tractableadaption of methods. The applicability of a method in a planning situation is formulatedin the specification, essentially consisting of an object level formula schema and a meta-levelformula of a declarative constraint language. After setting up our general framework, wemainly concentrate on this constraint language. Furthermore we illustrate how our methodscan be used in a Strips-like planning framework. Finally we briefly illustrate the mechanicalmodification of declaratively encoded methods by so-called meta-methods.
Planning Argumentative Texts
(1999)
This paper presents PROVERB a text planner forargumentative texts. PROVERB's main feature isthat it combines global hierarchical planning and un-planned organization of text with respect to local de-rivation relations in a complementary way. The formersplits the task of presenting a particular proof intosubtasks of presenting subproofs. The latter simulateshow the next intermediate conclusion to be presentedis chosen under the guidance of the local focus.
This paper deals with the problem of picking-up deformable linear workpieces such as cables or ropes with an industrial robot. First, we give a motivation and problem definition. Based on a brief conceptual discussion of possible approaches we derive an algorithm for picking-up hanging deformable linear objects using two light barriers as sensor system. For this hardware, a skill-based approach is described and the parameters and major influence factors are discussed. In an experi- mental study, the feasibility and reliability under diverse conditions are investigated. The algorithm is found to be very reliable, if certain boundary conditions are met.
Turbulence models, which are a means to fix the closure problem arising from Reynolds averaging of Navier-Stokes equations, are economical stop-gaps but suffer from accuracy issues. Modifying turbulence models by incorporating corrections in their functional form is one approach to improve their accuracy. We estimate correction functionals for the Spalart - Allmaras turbulence model, based on an inverse problem with PDE constraints emphasizing the issue of regularization.
The paper presents a novel approach to parallel motion planning for robot manipulators in 3D workspaces. The approach is based on a randomized parallel search algorithm and focuses on solving the path planning problem for industrial robot arms working in a reasonably cluttered workspace. The path planning system works in the discretized configuration space which needs not to be represented explicitly. The parallel search is conducted by a number of rule-based sequential search processes, which work to nd a path connecting the initial configuration to the goal via a number of randomly generated subgoal configurations. Since the planning performs only on-line collision tests with proper proximity information without using pre-computed information, the approach is suitable for planning problems with multirobot or dynamic environments. The implementation has been carried out on the parallel virtual machine (PVM) of a cluster of SUN4 workstations and SGI machines. The experimental results have shown that the approach works well for a 6-dof robot arm in a reasonably cluttered environment, and that parallel computation increases the efficiency of motion planning significantly.
This paper presents the different possibilities for parallel processing in robot control architectures. At the beginning, we shortly review the historic development of control architectures. Then, a list of requirements for control architectures is set up from a parallel processing point of view. As our main topic, we identify the levels of parallel processing in robot control architectures. With each level of parallelism, examples for a typical robot control architecture are presented. Finally, a list of keywords is provided for each previous work we refer to.
This paper presents a new approach to parallel motion planning for industrial robot arms with six degrees of freedom in an on-line given 3D environment. The method is based on the A*-search algorithm and needs no essential off-line computations. The algorithm works in an implicitly descrete configuration space. Collisions are detected in the cartesian workspace by hierarchical distance computation based on the given CAD model. By decomposing the 6D configuration space into hypercubes and cyclically mapping them onto multiple processing units, a good load distribution can be achieved. We have implemented the parallel motion planner on a workstation cluster with 9 PCs and tested the planner for several benchmark environments. With optimal discretisation, the new approach usually shows linear, and sometimes even superlinear speedups. In on-line provided environments with static obstacles, the parallel planning times are only a few seconds.
Several governmental organizations all over the world aim for algorithmic accountability of artificial intelligence systems. However, there are few specific proposals on how exactly to achieve it. This article provides an extensive overview of possible transparency and inspectability mechanisms that contribute to accountability for the technical components of an algorithmic decision-making system. Following the different phases of a generic software development process, we identify and discuss several such mechanisms. For each of them, we give an estimate of the cost with respect to time and money that might be associated with that measure.
In this paper we describe a framework for defining and operationalizing conceptual models of distributed knowledge-based systems which extends published approaches by the notion of ,agents" and multiple task decompositions. The main part deals with techniques underlying our distributed interpreter. We show how a client-server-architecture can be implemented which allows prototyping distributed knowledge-based systems. Further we describe our mechanism which manages task interactions and supports dependency-directed backtracking efficiently.
This paper is based on a path planning approach we reported earlier for industrial robot arms with 6 degrees of freedom in an on-line given 3D environment. It has on-line capabilities by searching in an implicit and descrete configuration space and detecting collisions in the Cartesian workspace by distance computation based on the given CAD model. Here, we present different methods for specifying the C-space discretization. Besides the usual uniform and heuristic discretization, we investigate two versions of an optimal discretization for an user-predefined Cartesian resolution. The different methods are experimentally evaluated. Additionally, we provide a set of 3- dimensional benchmark problems for a fair comparison of path planner. For each benchmark, the run-times of our planner are between only 3 and 100 seconds on a Pentium PC with 133 MHz.
In this paper, the problem of path planning for robot manipulators with six degrees of freedom in an on-line provided three-dimensional environment is investigated. As a basic approach, the best-first algorithm is used to search in the implicit descrete configuration space. Collisions are detected in the Cartesian workspace by hierarchical distance computation based on the given CAD model. The basic approach is extended by three simple mechanisms and results in a heuristic hierarchical search. This is done by adjusting the stepsize of the search to the distance between the robot and the obstacles. As a first step, we show encouraging experimental results with two degrees of freedom for five typical benchmark problems.
Enhancing the quality of surgical interventions is one of the main goals of surgical robotics. Thus we have devised a surgical robotic system for maxillofacial surgery which can be used as an intelligent intraoperative surgical tool. Up to now a surgeon preoperatively plans an intervention by studying twodimensional X-rays, thus neglecting the third dimension. In course of the special research programme "Computer and Sensor Aided Surgery" a planning system has been developed at our institute, which allows the surgeon to plan an operation on a threedimensional computer model of the patient . Transposing the preoperatively planned bone cuts, bore holes, cavities, and milled surfaces during surgery still proves to be a problem, as no adequate means are at hand: the actual performance of the surgical intervention and the surgical outcome solely depend on the experience and the skill of the operating surgeon. In this paper we present our approach of a surgical robotic system to be used in maxillofacial surgery. Special stress is being laid upon the modelling of the environment in the operating theatre and the motion planning of our surgical robot .
In most cases higher-order logic is based on the (gamma)-calculus in order to avoid the infinite set of so-called comprehension axioms. However, there is a price to be paid, namelyan undecidable unification algorithm. If we do not use the(gamma) - calculus, but translate higher-order expressions intofirst-order expressions by standard translation techniques, we haveto translate the infinite set of comprehension axioms, too. Ofcourse, in general this is not practicable. Therefore such anapproach requires some restrictions such as the choice of thenecessary axioms by a human user or the restriction to certainproblem classes. This paper will show how the infinite class ofcomprehension axioms can be represented by a finite subclass,so that an automatic translation of finite higher-order prob-lems into finite first-order problems is possible. This trans-lation is sound and complete with respect to a Henkin-stylegeneral model semantics.
We show how to buildup mathematical knowledge bases usingframes. We distinguish three differenttypes of knowledge: axioms, definitions(for introducing concepts like "set" or"group") and theorems (for relating theconcepts). The consistency of such know-ledge bases cannot be proved in gen-eral, but we can restrict the possibilit-ies where inconsistencies may be impor-ted to very few cases, namely to the oc-currence of axioms. Definitions and the-orems should not lead to any inconsisten-cies because definitions form conservativeextensions and theorems are proved to beconsequences.
A new problem for the automated off-line programming of industrial robot application is investigated. The Multi-Goal Path Planning is to find the collision-free path connecting a set of goal poses and minimizing e.g. the total path length. Our solution is based on an earlier reported path planner for industrial robot arms with 6 degrees-of-freedom in an on-line given 3D environment. To control the path planner, four different goal selection methods are introduced and compared. While the Random and the Nearest Pair Selection methods can be used with any path planner, the Nearest Goal and the Adaptive Pair Selection method are favorable for our planner. With the latter two goal selection methods, the Multi-Goal Path Planning task can be significantly accelerated, because they are able to automatically solve the simplest path planning problems first. Summarizing, compared to Random or Nearest Pair Selection, this new Multi-Goal Path Planning approach results in a further cost reduction of the programming phase.
We present a parallel path planning method that is able to automatically handle multiple goal configurations as input. There are two basic approaches, goal switching and bi-directional search, which are combined in the end. Goal switching dynamically selects a fa-vourite goal depending on some distance function. The bi-directional search supports the backward search direction from the goal to the start configuration, which is probably faster. The multi-directional search with goal switching combines the advantages of goal switching and bi-directional search. Altogether, the planning system is enabled to select one of the pref-erable goal configuration by itself. All concepts are experimentally validated for a set of benchmark problems consisting of an industrial robot arm with six degrees of freedom in a 3D environment.
This paper presents a new approach to parallel motion planning for industrial robot arms with six degrees of freedom in an on-line given 3D environment. The method is based on the A-search algorithm and needs no essential off-line computations. The algorithm works in an implicitly descrete configuration space. Collisions are detected in the Cartesian workspace by hierarchical distance computation based on the given CAD model. By decomposing the 6D configuration space into hypercubes and cyclically mapping them onto multiple processing units, a good load distribution can be achieved. We have implemented the parallel motion planner on a workstation cluster with 9 PCs and tested the planner for several benchmark environments. With optimal discretisation, the new approach usually shows linear speedups. In on-line provided environments with static obstacles, the parallel planning times are only a few seconds.
It is difficult for robots to handle a vibrating deformable object. Even for human beings it is a high-risk operation to, for example, insert a vibrating linear object into a small hole. However, fast manipulation using a robot arm is not just a dream; it may be achieved if some important features of the vibration are detected online. In this paper, we present an approach for fast manipulation using a force/torque sensor mounted on the robot's wrist. Template matching method is employed to recognize the vibrational phase of the deformable objects. Therefore, a fast manipulation can be performed with a high success rate, even if there is acute vibration. Experiments inserting a deformable object into a hole are conducted to test the presented method. Results demonstrate that the presented sensor-based online fast manipulation is feasible.
In this paper, we investigate the efficient simulation of deformable linear objects. Based on the state of the art, we extend the principle of minimizing the potential energy by considering plastic deformation and describe a novel approach for treating workpiece dynamics. The major influence factors on precision and computation time are identified and investigated experimentally. Finally, we discuss the usage of parallel processing in order to reduce the computation time.
This paper deals with the robust manipulation of deformable linear objects such as hoses or wires. We propose manipulation based on thequalitative contact state between the deformable workpiece and a rigid environment. First, we give an enumeration of possible contact states and discuss the main characteristics of each state. Second, we investigate the transitions which are possible between the contact states and derive criteria and conditions for each of them. Finally, we apply the concept of contact states and state transitions to the description of a typical assembly task.
This paper deals with the handling of deformable linear objects (DLOs), such as hoses, wires or leaf springs. It investigates the a priori knowledge about the 6-dimensional force/torque signal for a changing contact situation between a DLO and a rigid polyhedral obstacle. The result is a complete list, containing for each contact change the most significant combination of force/torque signal components together with a description of the expected signal curve. This knowledge enables the reliable detection of changes in the DLO contact situation and with it the implementation of sensor-based manipulation skills for all possible contact changes.
Manipulating deformable linear objects - Vision-based recognition of contact state transitions -
(1999)
A new and systematic approach to machine vision-based robot manipulation of deformable (non-rigid) linear objects is introduced. This approach reduces the computational needs by using a simple state-oriented model of the objects. These states describe the relation of the object with respect to an obstacle and are derived from the object image and its features. Therefore, the object is segmented from a standard video frame using a fast segmentation algorithm. Several object features are presented which allow the state recognition of the object while being manipulated by the robot.
The task of handling non-rigid one-dimensional objects by a robot manipulation system is investigated. To distinguish between different non-rigid object behaviors, five classes of deformable objects from a robotic point of view are proposed. Additionally, an enumeration of all possible contact states of one-dimensional objects with polyhedral obstacles is provided. Finally, the qualitative motion behavior of linear objects is analyzed for stable point contacts. Experiments with different materials validate the analytical results.
This paper describes how knowledge-based techniques can be used to overcome problems of workflow management in engineering applications. Using explicit process and product models as a basis for a workflow interpreter allows to alternate planning and execution steps, resulting in an increased flexibility of project coordination and enactment. To gain the full advantages of this flexibility, change processes have to be supported by the system. These require an improved traceability of decisions and have to be based on dependency management and change notification mechanisms. Our methods and techniques are illustrated by two applications: Urban land-use planning and software process modeling.
Four different initialization methods for parallel Branch-and-bound algorithms are described and compared with reference to several criteria. A formal analysis of their idle times and efficiency follows. It indicates that the efficiency of three methods depends on the branching factor of the search tree. Furthermore, the fourth method offers the best efficiency of the overall algorithm when a centralized OPEN set is used. Experimental results by a PRAM simulation support these statements.
We present two techniques for reasoning from cases to solve classification tasks: Induction and case-based reasoning. We contrast the two technologies (that are often confused) and show how they complement each other. Based on this, we describe how they are integrated in one single platform for reasoning from cases: The Inreca system.
Die Lösung einer Konfigurationsaufgabe in technischen Domänen besteht aus einer Menge von Bauteilen, die miteinander verträglich sind und in ihrem Zusammenspiel die gegebenen Anforderung erfüllen. Eine gängige Vorgehensweise bei der Suche nach einer Lösung ist die schrittweise Spezialisierung einer abstrakten Aufgabenstellung oder ihre Zerlegung in Teilaufgaben. Ein Konfigurationssystem, das diese Vorgehensweise unterstützt, muss Wissen enthalten, wie eine Aufgabe spezialisiert oder in Teilaufgaben zerlegt werden kann, welche konkreten Bauteile zur Erfüllung einer ausreichend detaillierten Teilaufgabe verwendet werden können und ob alle Teile einer Lösung miteinander verträglich sind. Aufgrund dieses Wissens kann eine konsistente Lösung durch Tiefensuche hergeleitet werden.
In diesem Papier vergleichen wir Hypermedia- und Expertensystemansaetze zur Wissensverarbeitung. Wir zeigen, wie ein integrierter Ansatz die Erstellung von Expertensystemen erleichtert. Das von uns entwickelte und implementierte System ermoeglicht einen "sanften" Entwicklungsprozess ausgehend von initialen Protokollen zu einer semi-formale Strukturierung in Form eines getypten Hypertextes. Dem Hypertext ist eine aufgabenorientierte Struktur aufgepraegt, so dass eine anschliessende Operationalisierung in Form eines Expertensystems vereinfacht wird. Die in diesem Prozess erzeugte Zwischenrepraesentation (der Hypertext) wird von einem Interpreter direkt zur interaktiven Loesung von Problemen benutzt, wobei die einzelnen Aufgaben auf die verschiedenen Sachbearbeiter verteilt werden. Abschliessend erlaeutern wir, dass Hypertext und Expertensysteme nur die Raender eines Kontinuums einer allgemeinen Wissensverarbeitung sind.
Algorithmic decision-making (ADM) systems have come to support, pre-empt or substitute for human decisions in manifold areas, with potentially significant impacts on individuals' lives. Achieving transparency and accountability has been formulated as a general goal regarding the use of these systems. However, concrete applications differ widely in the degree of risk and the accountability problems they entail for data subjects. The present paper addresses this variation and presents a framework that differentiates regulatory requirements for a range of ADM system uses. It draws on agency theory to conceptualize accountability challenges from the point of view of data subjects with the purpose to systematize instruments for safeguarding algorithmic accountability. The paper furthermore shows how such instruments can be matched to applications of ADM based on a risk matrix. The resulting comprehensive framework can guide the evaluation of ADM systems and the choice of suitable regulatory provisions.
In this paper we are interested in using a firstorder theorem prover to prove theorems thatare formulated in some higher order logic. Tothis end we present translations of higher or-der logics into first order logic with flat sortsand equality and give a sufficient criterion forthe soundness of these translations. In addi-tion translations are introduced that are soundand complete with respect to L. Henkin's gen-eral model semantics. Our higher order logicsare based on a restricted type structure in thesense of A. Church, they have typed functionsymbols and predicate symbols, but no sorts.
This paper analyzes how mathematicians prove the-orems. The analysis is based upon several empiricalsources such as reports of mathematicians and math-ematical proofs by analogy. In order to combine thestrength of traditional automated theorem provers withhuman-like capabilities, the questions arise: Whichproblem solving strategies are appropriate? Which rep-resentations have to be employed? As a result of ouranalysis, the following reasoning strategies are recog-nized: proof planning with partially instantiated meth-ods, structuring of proofs, the transfer of subproofs andof reformulated subproofs. We discuss the represent-ation of a component of these reasoning strategies, aswell as its properties. We find some mechanisms neededfor theorem proving by analogy, that are not providedby previous approaches to analogy. This leads us to acomputational representation of new components andprocedures for automated theorem proving systems.
Higher-Order Tableaux
(1999)
Even though higher-order calculi for automated theorem prov-ing are rather old, tableau calculi have not been investigated yet. Thispaper presents two free variable tableau calculi for higher-order logicthat use higher-order unification as the key inference procedure. Thesecalculi differ in the treatment of the substitutional properties of equival-ences. The first calculus is equivalent in deductive power to the machine-oriented higher-order refutation calculi known from the literature, whereasthe second is complete with respect to Henkin's general models.
Software development organizations are recognizing the increasing importance of investing in the build-up of core competencies for their competitiveness in software system development. This is supported by reuse and experience repository systems that assist in capturing and reusing all kinds of software artifacts (e. g., code, patterns, frameworks) and processes as well as experiences related to these artifacts and processes. To justify such an investment and guide its improvement, it must be evaluated according to the business case, that is, a measurement program has to be developed that is oriented towards the business goals of such a reuse and experience repository system. In this paper, we suggest an approach to iteratively build up measurement programs for gaining feedback and, thereby, controlling and improving such a reuse and experience repository system. The focus is placed on guidelines for the evolution of such measurement programs over time, rather than providing directly applicable metrics or questionnaires. In order to illustrate the feasibility of the approach, examples of running measurement programs at different stages of evolutions are given.
We describe a novel technique for the simultaneous visualization of multiple scalar fields, e.g. representing the members of an ensemble, based on their contour trees. Using tree alignments, a graph-theoretic concept similar to edit distance mappings, we identify commonalities across multiple contour trees and leverage these to obtain a layout that can represent all trees simultaneously in an easy-to-interpret, minimally-cluttered manner. We describe a heuristic algorithm to compute tree alignments for a given similarity metric, and give an algorithm to compute a joint layout of the resulting aligned contour trees. We apply our approach to the visualization of scalar field ensembles, discuss basic visualization and interaction possibilities, and demonstrate results on several analytic and real-world examples.
Kinetic models of human motion rely on boundary conditions which are defined by the interaction of the body with its environment. In the simplest case, this interaction is limited to the foot contact with the ground and is given by the so called ground reaction force (GRF). A major challenge in the reconstruction of GRF from kinematic data is the double support phase, referring to the state with multiple ground contacts. In this case, the GRF prediction is not well defined. In this work we present an approach to reconstruct and distribute vertical GRF (vGRF) to each foot separately, using only kinematic data. We propose the biomechanically inspired force shadow method (FSM) to obtain a unique solution for any contact phase, including double support, of an arbitrary motion. We create a kinematic based function, model an anatomical foot shape and mimic the effect of hip muscle activations. We compare our estimations with the measurements of a Zebris pressure plate and obtain correlations of 0.39≤r≤0.94 for double support motions and 0.83≤r≤0.87 for a walking motion. The presented data is based on inertial human motion capture, showing the applicability for scenarios outside the laboratory. The proposed approach has low computational complexity and allows for online vGRF estimation.
Es wird die Aufgabe der vollständigen räumlichen Abdeckung von Regionen in durch mobile Roboter betrachtet. Da-bei können die Regionen in vollständig, teilweise oder nicht bekannten Umgebungen liegen. Zur Lösung wird ein Verfahren aus der Computer-grafik zum Füllen von Bildregionen zugrunde gelegt. Das Verfahren hat eine lokale Sichtweise und läßt somit den Einsatz von Sensordaten und das Auftreten von unvorhergesehenen Hindernissen zu. Die Regionen können durch Karten off-line vorgegeben sein oder durch Sensordaten on-line aufgebaut werden. Dennoch ist eine vollständige und genau einma-lige Flächenbearbeitung garantiert. Dies wird an Beispielen in einer graphischen Visualisierung der Realzeit-Steuerung des Roboters validiert.
Beim Greifen deformierbarer oder zerbrechlicher Werkstücke kommen der Greifgeschwindigkeit sowie der Greifkraft besondere Bedeutung zu. In dieser Arbeit wird eine universelle Steuerung für pneumatische Greifer beschrieben, die eine einfache Einstellung dieser Größen über zwei spannungsgesteuerte Proportionalventile gestattet. Diese Anordnung wird für eine Einflußanalyse von Greifkraft und Greifgeschwindigkeit beim Greifen von Kabeln und Kabelbäumen genutzt, welche sich als robust und unproblematisch erwiesen haben.
One of the many features needed to support the activities of autonomous systems is the ability of motion planning. It enables robots to move in their environment securely and to accomplish given tasks. Unfortunately, the control loop comprising sensing, planning, and acting has not yet been closed for robots in dynamic environments. One reason involves the long execution times of the motion planning component. A solution for this problem is offered by the use of highly computational parallelism. Thus, an important task is the parallelization of existing motion planning algorithms for robots so that they are suitable for highly computational parallelism. In several cases, completely new algorithms have to be designed, so that a parallelization is feasible. In this survey, we review recent approaches to motion planning using parallel computation. As a classification scheme, we use the structure given by the different approaches to the robot's motion planning. For each approach, the available parallel processing methods are discussed. Each approach is uniquely assigned a class. Finally, for each referenced research work, a list of keywords is given.
For the online collision detection with a multi-arm robot a fast method for computing the so-called collision vector is presented. Manipulators and obstacles are modelled by sets of convex polytopes. Known distance algorithms serve as a foundation. To speed up the collision detection dynamic obstacles are approximated by geometric primitives and organized in hierarchies. On-line, the here introduced Dynamic Hierarchies are adjusted to the current arm configuration. A comparison with previous methods shows an increased acceleration of the computations.
Die Bewegungsplanung für Industrieroboter ist eine notwendige Voraussetzung, damit sich autonome Systeme kollisionsfrei durch die Umwelt bewegen können. Die Berücksichtigung von dynamischen Hindernissen zur Laufzeit erfordert allerdings leistungsfähige Algorithmen, zur Lösung dieser Aufgabenstellung in Echtzeit. Eine Möglichkeit zur Beschleunigung der Algorithmen ist der effiziente Einsatz von skalierbarer Parallelverarbeitung. Die softwaretechnische Umsetzung kann aber nur dann erfolgreich sein, wenn ein Parallelrechner zur Verfügung steht, der einen hohen Datendurchsatz bei geringer Latenzzeit bietet. Darüber hinaus muß dieser Parallelrechner unter vertretbarem Aufwand bedienbar sein und ein gutes Preisleistungsverhältnis aufweisen, damit die Parallelverarbeitung verstärkt in der Industrie zum Einsatz kommt. In diesem Artikel wird ein Workstation-Cluster auf der Basis von neun Standard- PCs vorgestellt, die über eine spezielle Kommunikationskarte miteinander vernetzt sind. In den einzelnen Abschnitten werden die gesammelten Erfahrungen bei der Inbetriebnahme, Systemadministration und Anwendung geschildert. Als Beispiel für eine Anwendung auf diesem Cluster wird ein paralleler Bewegungsplaner für Industrieroboter beschrieben.
In diesem Beitrag wird gezeigt, wie mit Hilfe von Knowledge Engineering Techniken eine komplexe Domäne, die Entwicklung von Bebauungsplänen, modelliert werden kann. Dabei wird insbesondere auf notwendige Erweiterungen bekannter Ansätze eingegangen, die sich aus einer praxisbezogenen Entwurfsdomäne ergeben. Der beschriebene Ansatz unterstützt die Koordination mehrerer Agenten durch die Verwaltung von Abhängigkeiten. Das beschriebene Projekt "Intelligenter Bebauungsplan" integriert GIS/CAD, Hypertext und Expertensystemtechnologie. Die Strukturierung der benötigten Informationen als Hypertext wurde von den beteiligten Stadtplanern gewünscht und ist eine natürliche Repräsentation für Gesetzestexte (und Kommentare), da sie ohnehin viele Querverweise enthalten.
Diese Arbeit skizziert einen allgemeinen Ansatz zur Montage deformierbarer linearer Werkstücke (wie Kabel, Drähte, Schläuche, Blattfedern) mit Industrierobotern. Hierzu werden insbesondere die folgenden zwei Aspekte betrachtetet. Erstens die zuverlässige Ausführung der Montage unter Berücksichtigung der Werkstückdeformation und anderer Unsicherheiten, zweitens die numerische Simulation des Werkstückverhaltens. Zur robusten Ausführung der Montage wird das aus der Montage starrer Werkstücke bekannte Konzept der Manipulation-Skills auf deformierbare Werkstücke übertragen. Bei der numerischen Simulation wird insbesondere die Bestimmung der Greifertrajektorie bei gegebener Aufgabenstellung betrachtet.
Editorial
(2020)
Editorial
(2020)
Editorial
(2020)
Editorial
(2021)
Deduktionssysteme
(1999)
This paper addresses the decomposition of proofs as a means of constructingmethods in plan-based automated theorem proving. It shows also, howdecomposition can beneficially be applied in theorem proving by analogy.Decomposition is also useful for human-style proof presentation. We proposeseveral decomposition techniques that were found to be useful in automatedtheorem proving and give examples of their application.
Machine learning algorithms are widely applied to create powerful prediction models. With increasingly complex models, humans' ability to understand the decision function (that maps from a high-dimensional input space) is quickly exceeded. To explain a model's decisions, black-box methods have been proposed that provide either non-linear maps of the global topology of the decision boundary, or samples that allow approximating it locally. The former loses information about distances in input space, while the latter only provides statements about given samples, but lacks a focus on the underlying model for precise ‘What-If'-reasoning. In this paper, we integrate both approaches and propose an interactive exploration method using local linear maps of the decision space. We create the maps on high-dimensional hyperplanes—2D-slices of the high-dimensional parameter space—based on statistical and personal feature mutability and guided by feature importance. We complement the proposed workflow with established model inspection techniques to provide orientation and guidance. We demonstrate our approach on real-world datasets and illustrate that it allows identification of instance-based decision boundary structures and can answer multi-dimensional ‘What-If'-questions, thereby identifying counterfactual scenarios visually.