Refine
Year of publication
Document Type
- Article (492) (remove)
Language
- English (492) (remove)
Has Fulltext
- yes (492)
Keywords
- AG-RESY (32)
- PARO (24)
- SKALP (14)
- resonances (8)
- Wannier-Stark systems (7)
- lifetimes (7)
- HANDFLEX (6)
- Quantum mechanics (6)
- motion planning (5)
- quantum mechanics (5)
Faculty / Organisational entity
- Kaiserslautern - Fachbereich Informatik (98)
- Kaiserslautern - Fachbereich Maschinenbau und Verfahrenstechnik (93)
- Kaiserslautern - Fachbereich Physik (92)
- Kaiserslautern - Fachbereich Mathematik (56)
- Kaiserslautern - Fachbereich Sozialwissenschaften (43)
- Kaiserslautern - Fachbereich Biologie (35)
- Kaiserslautern - Fachbereich Elektrotechnik und Informationstechnik (19)
- Kaiserslautern - Fachbereich Chemie (18)
- Kaiserslautern - Fachbereich Bauingenieurwesen (17)
- Kaiserslautern - Fachbereich Wirtschaftswissenschaften (7)
The performance of napkins is nowadays improved substantially by embedding granules of a superabsorbent into the cellulose matrix. In this paper a continuous model for the liquid transport in such an Ultra Napkin is proposed. Its mean feature is a nonlinear diffusion equation strongly coupled with an ODE describing a reversible absorbtion process. An efficient numerical method based on a symmetrical time splitting and a finite difference scheme of ADI-predictor-corrector type has been developed to solve these equations in a three dimensional setting. Numerical results are presented that can be used to optimize the granule distribution.
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.
In this paper we present an interpreter which allows to support the validation of conceptual models in early stages of the development. We compare hypermedia and expert system approaches to knowledge processing and show how an integrated approach eases the creation of expert systems. Our knowledge engineering tool CoMo-Kit allows a "smooth" transition from initial protocols via a semi-formal specification based on a typed hypertext up to an running expert system. The interpreter uses the intermediate hypertext representation for the interactive solution of problems. Thereby, tasks are distributed to agents via an local area network. This means that the specification of an expert system can directly be used to solve real world problems. If there exist formal (operational) specifications for subtasks then these are delegated to computers. Therefore, our approach allows to specify and validate distributed, cooperative systems where some subtasks are solved by humans and other subtasks are solved automatically by computers.
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.
A method for efficiently handling associativity and commutativity (AC) in implementations of (equational) theorem provers without incorporating AC as an underlying theory will be presented. The key of substantial efficiency gains resides in a more suitable representation of permutation-equations (such as f(x,f(y,z))=f(y,f(z,x)) for instance). By representing these permutation-equations through permutations in the mathematical sense (i.e. bijective func- tions :{1,..,n} {1,..,n}), and by applying adapted and specialized inference rules, we can cope more appropriately with the fact that permutation-equations are playing a particular role. Moreover, a number of restrictions concerning application and generation of permuta- tion-equations can be found that would not be possible in this extent when treating permu- tation-equations just like any other equation. Thus, further improvements in efficiency can be achieved.
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 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.
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.
Hyperbolic planes
(1995)
A survey on continuous, semidiscrete and discrete well-posedness and scale-space results for a class of nonlinear diffusion filters is presented. This class does not require any monotony assumption (comparison principle) and, thus, allows image restoration as well. The theoretical results include existence, uniqueness, continuous dependence on the initial image, maximum-minimum principles, average grey level invariance, smoothing Lyapunov functionals, and convergence to a constant steady state.
Cloudy inhomogenities in artificial fabrics are graded by a fast method which is based on a Laplacian pyramid decomposition of the fabric image. This band-pass representation takes into account the scale character of the cloudiness. A quality measure of the entire cloudiness is obtained as a weighted mean over the variances of all scales.
With this article we first like to give a brief review on wavelet thresholding methods in non-Gaussian and non-i.i.d. situations, respectively. Many of these applications are based on Gaussian approximations of the empirical coefficients. For regression and density estimation with independent observations, we establish joint asymptotic normality of the empirical coefficients by means of strong approximations. Then we describe how one can prove asymptotic normality under mixing conditions on the observations by cumulant techniques.; In the second part, we apply these non-linear adaptive shrinking schemes to spectral estimation problems for both a stationary and a non-stationary time series setup. For the latter one, in a model of Dahlhaus on the evolutionary spectrum of a locally stationary time series, we present two different approaches. Moreover, we show that in classes of anisotropic function spaces an appropriately chosen wavelet basis automatically adapts to possibly different degrees of regularity for the different directions. The resulting fully-adaptive spectral estimator attains the rate that is optimal in the idealized Gaussian white noise model up to a logarithmic factor.
This paper is devoted to the mathematica l description of the solution of the so-called rainflow reconstruction problem, i.e. the problem of constructing a time series with an a priori given rainflow m atrix. The algorithm we present is mathematically exact in the sense that no app roximations or heuristics are involved. Furthermore it generates a uniform distr ibution of all possible reconstructions and thus an optimal randomization of the reconstructed series. The algorithm is a genuine on-line scheme. It is easy adj ustable to all variants of rainflow such as sysmmetric and asymmetric versions a nd different residue techniques.
In the automotive industry both the loca l strain approach and rainflow counting are well known and approved tools in the numerical estimation of the lifetime of a new developed part especially in the automotive industry. This paper is devoted to the combination of both tools and a new algorithm is given that takes advantage of the inner structure of the most used damage parameters.
The ideas of texture analysis by means of the structure tensor are combined with the scale-space concept of anisotropic diffusion filtering. In contrast to many other nonlinear diffusion techniques, the proposed one uses a diffusion tensor instead of a scalar diffusivity. This allows true anisotropic behaviour. The preferred diffusion direction is determined according to the phase angle of the structure tensor. The diffusivity in this direction is increasing with the local coherence of the signal. This filter is constructed in such a way that it gives a mathematically well-funded scale-space representation of the original image. Experiments demonstrate its usefulness for the processing of interrupted one-dimensional structures such as fingerprint and fabric images.
We describe a hybrid case-based reasoning system supporting process planning for machining workpieces. It integrates specialized domain dependent reasoners, a feature-based CAD system and domain independent planning. The overall architecture is built on top of CAPlan, a partial-order nonlinear planner. To use episodic problem solving knowledge for both optimizing plan execution costs and minimizing search the case-based control component CAPlan/CbC has been implemented that allows incremental acquisition and reuse of strategical problem solving experience by storing solved problems as cases and reusing them in similar situations. For effective retrieval of cases CAPlan/CbC combines domain-independent and domain-specific retrieval mechanisms that are based on the hierarchical domain model and problem representation.
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.
We present an approach to systematically describing case-based reasoning systems bydifferent kinds of criteria. One main requirement was the practical relevance of these criteria and their usability for real-life applications. We report on the results we achieved from a case study carried out in the INRECA1 Esprit project.
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.
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.
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.
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.
We derive minimax rates for estimation in anisotropic smoothness classes. This rate is attained by a coordinatewise thresholded wavelet estimator based on a tensor product basis with separate scale parameter for every dimension. It is shown that this basis is superior to its one-scale multiresolution analog, if different degrees of smoothness in different directions are present.; As an important application we introduce a new adaptive wavelet estimator of the time-dependent spectrum of a locally stationary time series. Using this model which was resently developed by Dahlhaus, we show that the resulting estimator attains nearly the rate, which is optimal in Gaussian white noise, simultaneously over a wide range of smoothness classes. Moreover, by our new approach we overcome the difficulty of how to choose the right amount of smoothing, i.e. how to adapt to the appropriate resolution, for reconstructing the local structure of the evolutionary spectrum in the time-frequency plane.
For periodically driven systems, quantum tunneling between classical resonant stability islands in phase space separated by invariant KAM curves or chaotic regions manifests itself by oscillatory motion of wave packets centered on such an island, by multiplet splittings of the quasienergy spectrum, and by phase space localisation of the quasienergy states on symmetry related ,ux tubes. Qualitatively di,erent types of classical resonant island formation | due to discrete symmetries of the system | and their quantum implications are analysed by a (uniform) semiclassical theory. The results are illustrated by a numerical study of a driven non-harmonic oscillator.
The Filter-Diagonalization Method is used to ,nd the broad and even overlapping resonances of a 1D Hamiltonian used before as a test model for new resonance theories and computational methods. It is found that the use of several complex-scaled cross-correlation probability amplitudes from short time propagation enables the calculation of broad overlapping resonances, which can not be resolved from the amplitude of a single complex-scaled autocorrelation calculation.
Static magnetic and spin wave properties of square lattices of permalloy micron dots with thicknesses of 500 Å and 1000 Å and with varying dot separations have been investigated. A magnetic fourfold anisotropy was found for the lattice with dot diameters of 1 micrometer and a dot separation of 0.1 micrometer. The anisotropy is attributed to an anisotropic dipole-dipole interaction between magnetically unsaturated parts of the dots. The anisotropy strength (order of 100000 erg/cm^3 ) decreases with increasing in-plane applied magnetic field.
Static magnetic and spin wave properties of square lattices of permalloy micron dots with thicknesses of 500 Å and 1000 Å and with varying dot separations have been investigated. The spin wave frequencies can be well described taking into account the demagnetization factor of each single dot. A magnetic four-fold anisotropy was found for the lattice with dot diameters of 1 micrometer and a dot separation of 0.1 micrometer. The anisotropy is attributed to an anisotropic dipole-dipole interaction between magnetically unsaturated parts of the dots. The anisotropy strength (order of 100000 erg/cm^3 ) decreases with increasing in-plane applied magnetic field.
The first observation of self-focusing of dipolar spin waves in garnet film media is reported. In particular, we show that the quasi-stationary diffraction of a finite-aperture spin wave beam in a focusing medium leads to the concentration of the wave power in one focal point rather than along a certain line (channel). The obtained results demonstrate the wide applicability of non-linear spin wave media to study non-linear wave phenomena using an advanced combined microwave-Brillouin light scattering technique for a two-dimensional mapping of the spin wave amplitudes.
Brillouin light scattering investigations of exchange biased (110)-oriented NiFe/FeMn bilayers
(1997)
All contributing magnetic anisotropies in (110)-oriented exchange biased Ni 80 Fe 20 /Fe 50 Mn 50 double layers prepared by molecular beam epitaxy on Cu(110) single crystals have been determined by means of Brillouin light scattering. Upon covering the Ni 80 Fe 20 films by Fe 50 Mn 50 , a unidirectional anisotropy contribution appears, which is consistent with the measured exchange bias field. The uniaxial and fourfold in-plane anisotropy contributions are largely modified by an amount, which scales with the Ni 80 Fe 20 thickness, indicating an interface effect. The strong uniaxial anisotropy contribution shows an in-plane switching of the easy axis from [110] to [001] with increasing Ni 80 Fe 20 -layer thickness. The large mode width of the spin wave excitations, which exceeds the linewidth of uncovered Ni 80 Fe 20 films by a factor of more than six, indicates large spatial variations of the exchange coupling constant. (C) 1998 American Institute of Physics.
We report on Brillouin light scattering investigations of the elastic properties in Co/Ni superlattices which exhibit localized electronic eigenstates near the Fermi level causing an oscillation of the resistivity as a function of the superlattice periodicity A. No oscillations of the Rayleigh and Sezawa mode as a function of A could be observed within an error margin of +- 2% indicating that the localized electronic states do not contribute to the elastic constants.
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.
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.
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.
We prove that there exists a positive \(\alpha\) such thatfor any integer \(\mbox{$d\ge 3$}\) and any topological types \(\mbox{$S_1,\dots,S_n$}\) of plane curve singularities, satisfying \(\mbox{$\mu(S_1)+\dots+\mu(S_n)\le\alpha d^2$}\), there exists a reduced irreducible plane curve of degree \(d\) with exactly \(n\) singular points of types \(\mbox{$S_1,\dots,S_n$}\), respectively. This estimate is optimal with respect to theexponent of \(d\). In particular, we prove that for any topological type \(S\) there exists an irreducible polynomial of degree \(\mbox{$d\le 14\sqrt{\mu(S)}$}\) having a singular point of type \(S\).
The quasienergy spectrum of a periodically driven quantum system is constructed from classical dynamics by means of the semiclassical initial value representation using coherent states. For the first time, this method is applied to explicitly time dependent systems. For an anharmonic oscillator system with mixed chaotic and regular classical dynamics, the entire quantum spectrum (both regular and chaotic states) is reproduced semiclassically with surprising accuracy. In particular, the method is capable to account for the very small tunneling splittings.
The dispersions of dipolar (Damon-Eshbach modes) and exchange dominated spin waves are calculated for in-plane magnetized thin and ultrathin cubic films with (111) crystal orientation and the results are compared with those obtained for the other principal planes. The properties of these magnetic excitations are examined from the point of view of Brillouin light scattering experiments. Attention is paid to study the spin-wave frequency variation as a function of the magnetization direction in the film plane for different film thicknesses. Interface anisotropies and the bulk magnetocrystalline anisotropy are considered in the calculation. A quantitative comparison between an analytical expression obtained in the limit of small film thickness and wave vector and the full numerical calculation is given.
A formalism is developed for calculating the quasienergy states and spectrum for time-periodic quantum systems when a time-periodic dynamical invariant operator with a nondegenerate spectrum is known. The method, which circumvents the integration of the Schr-odinger equation, is applied to an integrable class of systems, where the global invariant operator is constructed. Furthermore, a local integrable approximation for more general non-integrable systems is developed. Numerical results are presented for the doubleresonance model.
We consider N coupled linear oscillators with time-dependent coecients. An exact complex amplitude - real phase decomposition of the oscillatory motion is constructed. This decomposition is further used to derive N exact constants of motion which generalise the so-called Ermakov-Lewis invariant of a single oscillator. In the Floquet problem of periodic oscillator coecients we discuss the existence of periodic complex amplitude functions in terms of existing Floquet solutions.
The Wannier-Bloch resonance states are metastable states of a quantum particle in a space-periodic potential plus a homogeneous field. Here we analyze the states of quantum particle in space- and time-periodic potential. In this case the dynamics of the classical counterpart of the quantum system is either quasiregular or chaotic depending on the driving frequency. It is shown that both the quasiregular and the chaotic motion can also support quantum resonances. The relevance of the obtained result to the problem a of crystal electron under simultaneous influence of d.c. and a.c. electric fields is briefly discussed. PACS: 73.20Dx, 73.40Gk, 05.45.+b
We study the statistics of the Wigner delay time and resonance width for a Bloch particle in ac and dc fields in the regime of quantum chaos. It is shown that after appropriate rescaling the distributions of these quantities have universal character predicted by the random matrix theory of chaotic scattering.
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 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 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.
A practical distributed planning and control system for industrial robots is presented. The hierarchical concept consists of three independent levels. Each level is modularly implemented and supplies an application interface (API) to the next higher level. At the top level, we propose an automatic motion planner. The motion planner is based on a best-first search algorithm and needs no essential off-line computations. At the middle level, we propose a PC-based robot control architecture, which can easily be adapted to any industrial kinematics and application. Based on a client/server-principle, the control unit estab-lishes an open user interface for including application specific programs. At the bottom level, we propose a flexible and modular concept for the integration of the distributed motion control units based on the CAN bus. The concept allows an on-line adaptation of the control parameters according to the robot's configuration. This implies high accuracy for the path execution and improves the overall system performance.
We present a parallel control architecture for industrial robot cells. It is based on closed functional components arranged in a flat communication hierarchy. The components may be executed by different processing elements, and each component itself may run on multiple processing elements. The system is driven by the instructions of a central cell control component. We set up necessary requirements for industrial robot cells and possible parallelization levels. These are met by the suggested robot control architecture. As an example we present a robot work cell and a component for motion planning, which fits well in this concept.
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.
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.
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 .
Let \(X\) be a Banach lattice. Necessary and sufficient conditions for a linear operator \(A:D(A) \to X\), \(D(A)\subseteq X\), to be of positive \(C^0\)-scalar type are given. In addition, the question is discussed which conditions on the Banach lattice imply that every operator of positive \(C^0\)-scalar type is necessarily of positive scalar type.
In the scalar case one knows that a complex normalized function of boundedvariation \(\phi\) on \([0,1]\) defines a unique complex regular Borel measure\(\mu\) on \([0,1]\). In this note we show that this is no longer true in generalin the vector valued case, even if \(\phi\) is assumed to be continuous. Moreover, the functions \(\phi\) which determine a countably additive vectormeasure \(\mu\) are characterized.
The following two norms for holomorphic functions \(F\), defined on the right complex half-plane \(\{z \in C:\Re(z)\gt 0\}\) with values in a Banach space \(X\), are equivalent:
\[\begin{eqnarray*} \lVert F \rVert _{H_p(C_+)} &=& \sup_{a\gt0}\left( \int_{-\infty}^\infty \lVert F(a+ib) \rVert ^p \ db \right)^{1/p}
\mbox{, and} \\ \lVert F \rVert_{H_p(\Sigma_{\pi/2})} &=& \sup_{\lvert \theta \lvert \lt \pi/2}\left( \int_0^\infty \left \lVert F(re^{i \theta}) \right \rVert ^p\ dr \right)^{1/p}.\end{eqnarray*}\] As a consequence, we derive a description of boundary values ofsectorial holomorphic functions, and a theorem of Paley-Wiener typefor sectorial holomorphic functions.
We consider wavelet estimation of the time-dependent (evolutionary) power spectrum of a locally stationary time series. Allowing for departures from stationary proves useful for modelling, e.g., transient phenomena, quasi-oscillating behaviour or spectrum modulation. In our work wavelets are used to provide an adaptive local smoothing of a short-time periodogram in the time-freqeuncy plane. For this, in contrast to classical nonparametric (linear) approaches we use nonlinear thresholding of the empirical wavelet coefficients of the evolutionary spectrum. We show how these techniques allow for both adaptively reconstructing the local structure in the time-frequency plane and for denoising the resulting estimates. To this end a threshold choice is derived which is motivated by minimax properties w.r.t. the integrated mean squared error. Our approach is based on a 2-d orthogonal wavelet transform modified by using a cardinal Lagrange interpolation function on the finest scale. As an example, we apply our procedure to a time-varying spectrum motivated from mobile radio propagation.
Several activities around the world aim at integrating object-oriented data models with relational ones in order to improve database management systems. As a first result of these activities, object-relational database management systems (ORDBMS) are already commercially available and, simultaneously, are subject to several research projects. This (position) paper reports on our activities in exploiting object-relational database technology for establishing repository manager functionality supporting software engineering (SE) processes. We argue that some of the key features of ORDBMS can directly be exploited to fulfill many of the needs of SE processes. Thus, ORDBMS, as we think, are much better suited to support SE applications than any others. Nevertheless, additional functionality, e. g., providing adequate version management, is required in order to gain a completely satisfying SE repository. In order to remain flexible, we have developed a generative approach for providing this additional functionality. It remains to be seen whether this approach, in turn, can effectively exploit ORDBMS features. This paper, therefore, wants to show that ORDBMS can substantially contribute to both establishing and running SE repositories.
We present an entropy concept measuring quantum localization in dynamical systems based on time averaged probability densities. The suggested entropy concept is a generalization of a recently introduced [PRL 75, 326 (1995)] phase-space entropy to any representation chosen according to the system and the physical question under consideration. In this paper we inspect the main characteristics of the entropy and the relation to other measures of localization. In particular the classical correspondence is discussed and the statistical properties are evaluated within the framework of random vector theory. In this way we show that the suggested entropy is a suitable method to detect quantum localization phenomena in dynamical systems.
The Filter-Diagonalization Method is applied to time periodic Hamiltonians and used to find selectively the regular and chaotic quasienergies of a driven 2D rotor. The use of N cross-correlation probability amplitudes enables a selective calculation of the quasienergies from short time propagation to the time T (N). Compared to the propagation time T (1) which is required for resolving the quasienergy spectrum with the same accuracy from auto-correlation calculations, the cross-correlation time T (N) is shorter by the factor N , that is T (1) = N T (N).
The global dynamical properties of a quantum system can be conveniently visualized in phase space by means of a quantum phase space entropy in analogy to a Poincare section in classical dynamics for two-dimensional time independent systems. Numerical results for the Pullen Edmonds systems demonstrate the properties of the method for systems with mixed chaotic and regular dynamics.
A novel method is presented which allows a fast computation of complex energy resonance states in Stark systems, i.e. systems in a homogeneous field. The technique is based on the truncation of a shift-operator in momentum space. Numerical results for space periodic and non-periodic systems illustrate the extreme simplicity of the method.
Quantum Chaos
(1999)
The study of dynamical quantum systems, which are classically chaotic, and the search for quantum manifestations of classical chaos, require large scale numerical computations. Special numerical techniques developed and applied in such studies are discussed: The numerical solution of the time-dependent Schr-odinger equation, the construction of quantum phase space densities, quantum dynamics in phase space, the use of phase space entropies for characterizing localization phenomena, etc. As an illustration, the dynamics of a driven one-dimensional anharmonic oscillator is studied, both classically and quantum mechanically. In addition, spectral properties and chaotic tunneling are addressed.
The paper studies metastable states of a Bloch electron in the presence of external ac and dc fields. Provided resonance condition between period of the driving frequency and the Bloch period, the complex quasienergies are numerically calculated for two qualitatively different regimes (quasiregular and chaotic) of the system dynamics. For the chaotic regime an effect of quantum stabilization, which suppresses the classical decay mechanism, is found. This effect is demonstrated to be a kind of quantum interference phenomenon sensitive to the resonance condition.
An unusual interlayer coupling, recently discovered in layered magnetic systems, is analysed from the experimental and theoretical points of view. This coupling favours the 90° orientation of the magnetization of the adjacent magnetic films. It can be phenomenologically described by a term in the energy expression, which is biquadratic with respect to the magnetizations of the two films. The main experimental findings, as well as the theoretical models, explaining the phenomenon are discussed.
The static and spin wave properties of regular square lattices of magnetic dots of 0.5-2 microm dot diameter and 1-4 microm periodicity patterned in permalloy films have been investigated by Brillouin light scattering. The samples have been structured using x-ray lithography and ion beam etching. The Brillouin light scattering spectra reveal both surface and bulk spin wave modes. The spin wave frequencies can be well described taking into account the demagnetization factor of each single dot. For the samples with smallest dot separation of 0.1 microm a fourfold in-plane magnetic anisotropy with the easy axis directed along the pattern diagonal is observed, indicating anisotropic coupling between the dots.
A computer control for a Sandercock-type multipath tandem Fabry-Perot interferometer is described, which offers many advantages over conventionally used analog control: The range of stability is increased due to active control of the laser light intensity and the mirror dither amplitude. The alignment is fully automated enabling start of a measurement within a minute after start of align, including optionally finding the optimum focus on the sample. The software control enables a programmable series of measurements with control of, e.g., the position and rotation of the sample, the angle of light incidence, the sample temperature, or the strength and direction of an applied magnetic field. Built-in fitting routines allow for a precise determination of frequency positions of excitation peaks combined with increased frequency accuracy due to a correction of a residual nonlinearity of the mirror stage drive.
A new method for calculating Stark resonances is presented and applied for illustration to the simple case of a one-particle, one-dimensional model Hamiltonian. The method is applicable for weak and strong dc fields. The only need, also for the case of many particles in multi-dimensional space, are either the short time evolution matrix elements or the eigenvalues and Fourier components of the eigenfunctions of the field-free Hamiltonian.
Epitaxial growth of metastable Pd(001) at high deposition temperatures up to a critical thickness of 6 monolayers on bcc-Fe(001) is reported, the critical thickness being depending dramatically on the deposition temperature. For larger thicknesses the Pd film undergoes a roughening transition with strain relaxation by forming a top polycrystalline layer. These results allow to make a correlation between previ-ously reported unusual magnetic properties of Fe/Pd double layers and the crystallographic structure of the Pd overlayer.
We investigate the temperature dependence of the magnetization reversal process and of spinwaves in epi-taxially grown (001)-oriented [Fem/Aun]30 multilayers (m = 1, 2; n = 1- 6). Both polar magneto-optic Kerrr effect and Brillouin light scattering measurements reveal that all investigated multilayers, apart from the [Fe2/Au1]30-sample, are magnetized perpendicular to the film plane. The out-of-plane anisotropy constants are obtained. At high temperature, the magnetization curves are well described by an alternating stripe domain structure with free mobile domain walls, and at low temperature by a thermal activation model for the domain wall motion.
Static and dynamic properties of patterned magnetic permalloy films are investigated. In square lattices of circular shaped permalloy dots an anisotropic coupling mechanism has been found, which is identified as being due to intrinsically unsaturated parts of the dots caused by spatial variations of demagnetizing field. In arrays of magnetic wires a quantization of the surface spin wave mode in several dispersionless modes is observed and quantitatively described. For large wavevectors the frequency separation between the modes becomes smaller and the frequencies converge to the dispersion of the dipole-exchange surface mode of a continuous film.
Wall energy and wall thickness of exchange-coupled rare-earth transition-metal triple layer stacks
(1999)
The room-temperature wall energy sw 54.0310 23 J/m 2 of an exchange-coupled Tb 19.6 Fe 74.7 Co 5.7 /Dy 28.5 Fe 43.2 Co 28.3 double layer stack can be reduced by introducing a soft magnetic intermediate layer in between both layers exhibiting a significantly smaller anisotropy compared to Tb+- FeCo and Dy+- FeCo. sw will decrease linearly with increasing intermediate layer thickness, d IL , until the wall is completely located within the intermediate layer for d IL d w , where d w denotes the wall thickness. Thus, d w can be obtained from the plot sw versus d IL .We determined sw and d w on Gd+- FeCo intermediate layers with different anisotropy behavior ~perpendicular and in-plane easy axis! and compared the results with data obtained from Brillouin light-scattering measurements, where exchange stiffness, A, and uniaxial anisotropy, K u , could be determined. With the knowledge of A and K u , wall energy and thickness were calculated and showed an excellent agreement with the magnetic measurements. A ten times smaller perpendicular anisotropy of Gd 28.1 Fe 71.9 in comparison to Tb+- FeCo and Dy+- FeCo resulted in a much smaller sw 51.1310 23 J/m 2 and d w 524 nm at 300 K. A Gd 34.1 Fe 61.4 Co 4.5 with in-plane anisotropy at room temperature showed a further reduced sw 50.3310 23 J/m 2 and d w 517 nm. The smaller wall energy was a result of a different wall structure compared to perpendicular layers.
Mn-Si-C alloy films are prepared by e-beam coevaporation onto a Si substrate held at 600 °C. Ferromagnetism is observed below T = (360 +/- 5) K with SQUID magnetometry and magneto-optical Kerr effect. This is the highest Curie temperature T yet observed for a Mn-based alloy. Although the composition determined by Auger depth profiling varies appreciably for different films, their T is the same indicating that ferromagnetism is caused by an alloy of well-defined composition independent of precipitations.
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.
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.
INRECA offers tools and methods for developing, validating, and maintaining classification, diagnosis and decision support systems. INRECA's basic technologies are inductive and case-based reasoning [9]. INRECA fully integrates [2] both techniques within one environment and uses the respective advantages of both technologies. Its object-oriented representation language CASUEL [10, 3] allows the definition of complex case structures, relations, similarity measures, as well as background knowledge to be used for adaptation. The objectoriented representation language makes INRECA a domain independent tool for its destined kind of tasks. When problems are solved via case-based reasoning, the primary kind of knowledge that is used during problem solving is the very specific knowledge contained in the cases. However, in many situations this specific knowledge by itself is not sufficient or appropriate to cope with all requirements of an application. Very often, background knowledge is available and/or necessary to better explore and interpret the available cases [1]. Such general knowledge may state dependencies between certain case features and can be used to infer additional, previously unknown features from the known ones.
The development of complex software systems is driven by many diverse and sometimes contradictory requirements such as correctness and maintainability of resulting products, development costs, and time-to-market. To alleviate these difficulties, we propose a development method for distributed systems that integrates different basic approaches. First, it combines the use of the formal description technique SDL with software reuse concepts. This results in the definition of a use-case driven, incremental development method with SDL-patterns as the main reusable artifacts. Experience with this approach has shown that there are several other factors of influence, such as the quality of reuse artifacts or the experience of the development team. Therefore, we further combined our SDL-pattern approach with an improvement methodology known from the area of experimental software engineering. In order to demonstrate the validity of this integrating approach, we sketch some representative outcomings of a case study.
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 paper studies quantum states of a Bloch particle in presence of external ac and dc fields. Provided the period of the ac field and the Bloch period are commensurate, an effective scattering matrix is introduced, the complex poles of which are the system quasienergy spectrum. The statistics of the resonance width and the Wigner delay time shows a close relation of the problem to random matrix theory of chaotic scattering.
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.
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 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 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.
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.
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.
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.
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.
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.
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.
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.
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.