## Fachbereich Informatik

### Filtern

#### Erscheinungsjahr

- 1998 (38) (entfernen)

#### Dokumenttyp

- Preprint (20)
- Wissenschaftlicher Artikel (13)
- Bericht (3)
- Dissertation (1)
- Masterarbeit (1)

#### Schlagworte

- AG-RESY (13)
- PARO (12)
- SKALP (9)
- Case Based Reasoning (4)
- industrial robots (4)
- motion planning (3)
- parallel processing (3)
- CIM-OSA (2)
- HANDFLEX (2)
- TOVE (2)

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.

This paper presents a new approach to parallel path planning for industrial robot arms with six degrees of freedom in an on-line given 3D environment. The method is based a best-first search algorithm and needs no essential off-line computations. The algorithm works in an implicitly discrete configuration space. Collisions are detected in the Cartesian workspace by hierarchical distance computation based on polyhedral models of the robot and the obstacles. 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 path planner on a workstation cluster with 9 PCs and tested the planner for several benchmark environments. With optimal discretisation, the new approach usually shows very good speedups. In on-line provided environments with static obstacles, the parallel planning times are only a few seconds.

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.

This paper discusses the problem of automatic off-line programming and motion planning for industrial robots. At first, a new concept consisting of three steps is proposed. The first step, a new method for on-line motion planning is introduced. The motion planning method is based on the A*-search algorithm and works in the implicit configuration space. During searching, the collisions are detected in the explicitly represented Cartesian workspace by hierarchical distance computation. In the second step, the trajectory planner has to transform the path into a time and energy optimal robot program. The practical application of these two steps strongly depends on the method for robot calibration with high accuracy, thus, mapping the virtual world onto the real world, which is discussed in the third step.

This paper describes a tableau-based higher-order theorem prover HOT and an application to natural language semantics. In this application, HOT is used to prove equivalences using world knowledge during higher-order unification (HOU). This extended form of HOU is used to compute the licensing conditions for corrections.

Simultaneous quantifier elimination in sequent calculus is an improvement over the well-known skolemization. It allows a lazy handling of instantiations as well as of the order of certain reductions. We prove the soundness of a sequent calculus which incorporates a rule for simultaneous quantifier elimination. The proof is performed by semantical arguments and provides some insights into the dependencies between various formulas in a sequent.

The notion of formal description techniques for timed systems (T-FDTs) has been introduced in [EDK98a] to provide a unifying framework for description techniques that are formal and that allow to describe the ongoing behavior of systems. In this paper we show that three well known temporal logics, MTL, MTL-R , and CTL*, can be embedded in this framework. Moreover, we provide evidence that a large number of dioeerent kinds of temporal logics can be considered as T-FDTs.

The paper addresses two problems of comprehensible proof presentation, the hierarchically structured presentation at the level of proof methods and different presentation styles of construction proofs. It provides solutions for these problems that can make use of proof plans generated by an automated proof planner.