ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
Filter
  • Articles  (38)
  • Other Sources
  • automated theorem proving  (19)
  • stability  (19)
  • Springer  (38)
  • American Geophysical Union
  • American Institute of Physics (AIP)
  • Blackwell Publishing Ltd
  • Nature Publishing Group
  • 2000-2004
  • 1995-1999  (38)
  • 1945-1949
  • 1997  (38)
  • Computer Science  (27)
  • Physics  (9)
  • Medicine  (2)
Collection
  • Articles  (38)
  • Other Sources
Publisher
  • Springer  (38)
  • American Geophysical Union
  • American Institute of Physics (AIP)
  • Blackwell Publishing Ltd
  • Nature Publishing Group
  • +
Years
  • 2000-2004
  • 1995-1999  (38)
  • 1945-1949
Year
  • 1
    Electronic Resource
    Electronic Resource
    Springer
    Queueing systems 27 (1997), S. 205-226 
    ISSN: 1572-9443
    Keywords: multiclass queueing networks ; ergodicity ; stability ; performance analysis
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract We develop the use of piecewise linear test functions for the analysis of stability of multiclass queueing networks and their associated fluid limit models. It is found that if an associated LP admits a positive solution, then a Lyapunov function exists. This implies that the fluid limit model is stable and hence that the network model is positive Harris recurrent with a finite polynomial moment. Also, it is found that if a particular LP admits a solution, then the network model is transient.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 2
    Electronic Resource
    Electronic Resource
    Springer
    Queueing systems 26 (1997), S. 343-363 
    ISSN: 1572-9443
    Keywords: retrial queues ; stability ; ergodicity ; renovation
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract We consider the following Type of problems. Calls arrive at a queue of capacity K (which is called the primary queue), and attempt to get served by a single server. If upon arrival, the queue is full and the server is busy, the new arriving call moves into an infinite capacity orbit, from which it makes new attempts to reach the primary queue, until it finds it non-full (or it finds the server idle). If the queue is not full upon arrival, then the call (customer) waits in line, and will be served according to the FIFO order. If λ is the arrival rate (average number per time unit) of calls and μ is one over the expected service time in the facility, it is well known that μ 〉 λ is not always sufficient for stability. The aim of this paper is to provide general conditions under which it is a sufficient condition. In particular, (i) we derive conditions for Harris ergodicity and obtain bounds for the rate of convergence to the steady state and large deviations results, in the case that the inter-arrival times, retrial times and service times are independent i.i.d. sequences and the retrial times are exponentially distributed; (ii) we establish conditions for strong coupling convergence to a stationary regime when either service times are general stationary ergodic (no independence assumption), and inter-arrival and retrial times are i.i.d. exponentially distributed; or when inter-arrival times are general stationary ergodic, and service and retrial times are i.i.d. exponentially distributed; (iii) we obtain conditions for the existence of uniform exponential bounds of the queue length process under some rather broad conditions on the retrial process. We finally present conditions for boundedness in distribution for the case of nonpatient (or non persistent) customers.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 3
    Electronic Resource
    Electronic Resource
    Springer
    Celestial mechanics and dynamical astronomy 67 (1997), S. 181-204 
    ISSN: 1572-9478
    Keywords: Hamiltonian systems ; symplectic mappings ; normal forms ; resonances ; stability ; three degrees of freedom
    Source: Springer Online Journal Archives 1860-2000
    Topics: Physics
    Notes: Abstract We analyze four-dimensional symplectic mappings in the neighbourhood of an elliptic fixed point whose eigenvalues are close to satisfy a third-order resonance. Using the perturbative tools of resonant normal forms, the geometry of the orbits and the existence of elliptic or hyperbolic one-dimensional tori (fixed lines) is worked out. This allows one to give an analytical estimate of the stability domain when the resonance is unstable. A comparison with numerical results for the four-dimensional Hénon mapping is given.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 4
    Electronic Resource
    Electronic Resource
    Springer
    Celestial mechanics and dynamical astronomy 69 (1997), S. 271-281 
    ISSN: 1572-9478
    Keywords: restricted three-body problem ; libration points ; stability
    Source: Springer Online Journal Archives 1860-2000
    Topics: Physics
    Notes: Abstract The existence and stability of triangular libration points in the relativistic restricted three-body problem has been studied. It is found that L4,5 are unstable in the whole range 0 ≤ µ ≤ 1/2 in contrast to the classical restricted three-body problem where they are stable for 0 〈 µ 〈 µ0, where µ is the mass parameter and µ0 = 0.03852....
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 5
    Electronic Resource
    Electronic Resource
    Springer
    Celestial mechanics and dynamical astronomy 69 (1997), S. 317-330 
    ISSN: 1572-9478
    Keywords: artificial satellite ; Nekhoroshev's theory ; normal form ; stability
    Source: Springer Online Journal Archives 1860-2000
    Topics: Physics
    Notes: Abstract We investigate the significance of long time stabilty predictions in the light of Nekhoroshev's theory by studying the orbits of artificial satellites. As a simplified model problem we consider the so-called J2problem for an earth's satellite, neglecting luni-solar perturbations and nonconservative effects. We consider a wide range of orbits, excluding those which are too close to the critical inclination. Most of the orbits turn out to be stable for times larger than the estimated age of the solar system, thus proving that, as far as dissipation can be neglected, stability in Nekhoroshev's sense may be effective for physically realistic systems.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 6
    Electronic Resource
    Electronic Resource
    Springer
    Journal of statistical physics 88 (1997), S. 691-711 
    ISSN: 1572-9613
    Keywords: Quasicrystals ; nonperiodic tilings ; classical lattice-gas models ; ground states ; stability
    Source: Springer Online Journal Archives 1860-2000
    Topics: Physics
    Notes: Abstract We give strong evidence that noncrystalline materials such as quasicrystals or incommensurate solids are not exceptions, but rather are generic in some regions of phase space. We show this by constructing classical lattice-gas models with translation-invariant finite-range interactions and with a unique quasiperiodic ground state which is stable against small perturbations of two-body potentials. More generally, we provide a criterion for stability of nonperiodic ground states.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 7
    Electronic Resource
    Electronic Resource
    Springer
    Journal of intelligent and robotic systems 20 (1997), S. 131-155 
    ISSN: 1573-0409
    Keywords: robot adaptive control ; basis function-like networks ; stability ; discrete variable structure
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science , Mechanical Engineering, Materials Science, Production Engineering, Mining and Metallurgy, Traffic Engineering, Precision Mechanics
    Notes: Abstract Stable neural network-based sampled-data indirect and direct adaptivecontrol approaches, which are the integration of a neural network (NN)approach and the adaptive implementation of the discrete variable structurecontrol, are developed in this paper for the trajectory tracking control ofa robot arm with unknown nonlinear dynamics. The robot arm is assumed tohave an upper and lower bound of its inertia matrix norm and its states areavailable for measurement. The discrete variable structure control servestwo purposes, i.e., one is to force the system states to be within the stateregion in which neural networks are used when the system goes out of neuralcontrol; and the other is to improve the tracking performance within the NNapproximation region. Main theory results for designing stable neuralnetwork-based sampled data indirect and direct adaptive controllers aregiven, and the extension of the proposed control approaches to the compositeadaptive control of a flexible-link robot is discussed. Finally, theeffectiveness of the proposed control approaches is illustrated throughsimulation studies.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 8
    Electronic Resource
    Electronic Resource
    Springer
    Journal of intelligent and robotic systems 19 (1997), S. 411-436 
    ISSN: 1573-0409
    Keywords: assembly planning ; stability ; robot ; forward ; operations
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science , Mechanical Engineering, Materials Science, Production Engineering, Mining and Metallurgy, Traffic Engineering, Precision Mechanics
    Notes: Abstract The paper presents an approach to sequence planning consisting in determining assembly sequences defined in terms of mating and non-mating operations and based on a dynamic expansion of the assembly tree obtained using a knowledge base management system. The planner considers the case of a single-robot assembly workcell. The use of stability and the detailed definition of sequences also by means of several non-mating operations are shown to be powerful instruments in the control of the tree expansion. Forward assembly planning has been chosen, in order to minimize the number of stability checks. Backtracking is avoided by combining precedence relations and stability analysis. Hard and soft constrains are introduced to drive the tree expansion. Hard constraints are precedence relations and stability analysis. All operations are associated to costs, which are used as soft constraints. The operation based approach enables one to manage even non-mating operations and to easily overcome the linearity constraint. Costs enable the planner to manage the association among tools and components. The first section of the paper concerns Stability Analysis that is subdivided into Static and Dynamic Stability Analysis. The former is mainly involved in analyzing gravity effects; the latter is mainly involved in evaluate inertia effects due to manipulation. Stability Analysis is implemented in a simplified form. Fundamental assumptions are: no rotational equilibrium condition is considered; for each reaction force only direction and versus, but not magnitude, are considered; friction is neglected. The second section discusses the structure of the planner and its implementation. The planner is a rule based system. Forward chaining and hypothetical reasoning are the inference strategies used. The knowledge base and the data base of the system are presented and the advantages obtained using a rule based system are discussed. The third section shows two planning examples, showing the performance of the system in a simple case and in an industrial test case, the assembly of a microwave branching filter composed of 26 components.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 9
    ISSN: 1573-4919
    Keywords: heart mitochondria ; lability ; muscle mitochondria ; oxidative phosphorylation ; stability ; taurine
    Source: Springer Online Journal Archives 1860-2000
    Topics: Biology , Chemistry and Pharmacology , Medicine
    Notes: Abstract We modified the isolation procedure of muscle and heart mitochondria. In human muscle, this resulted in a 3.4 fold higher yield of better coupled mitochondria in half the isolation time. In a preparation from rat muscle we studied factors that affected the stability of oxidative phosphorylation (oxphos) and found that it decreased by shaking the preparation on a Vortex machine, by exposure to light and by an increase in storage temperature. The decay was found to be different for each substrate tested. The oxidation of ascorbate was most stable and less sensitive to the treatments. When mitochondria were stored in the dark and the cold, the decrease in oxidative phosphorylation followed first order kinetics. In individual preparations of muscle and heart mitochondria, protection of oxidative phosphorylation was found by adding candidate stabilizers, such as desferrioxamine, lazaroids, taurine, carnitine, phosphocreatine, N-acetylcysteine, Trolox-C and ruthenium red, implying a role for reactive oxygen species and calcium-ions in the in vitro damage at low temperature to oxidative phosphorylation. In heart mitochondria oxphos with pyruvate and palmitoylcarnitine was most labile followed by glutamate, succinate and ascorbate.We studied the effect of taurine, hypotaurine, carnitine, and desferrioxamine on the decay of oxphos with these substrates. 1 mM taurine (n = 6) caused a significant protection of oxphos with pyruvate, glutamate and palmitoylcarnitine, but not with the other substrates. 5 mM L-carnitine (n = 6), 1 mM hypotaurine (n = 3) and 0.1 mM desferrioxamine (n = 3) did not protect oxphos with any of the substrates at a significant level. These experiments were undertaken in the hope that the in vitro stabilizers can be used in future treatment of patients with defects in oxidative phosphorylation. (Mol Cell Biochem 174: 61–66, 1997)
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 10
    Electronic Resource
    Electronic Resource
    Springer
    Acta mechanica Sinica 13 (1997), S. 366-376 
    ISSN: 1614-3116
    Keywords: vibro-impact ; stability ; multiplicity
    Source: Springer Online Journal Archives 1860-2000
    Topics: Mechanical Engineering, Materials Science, Production Engineering, Mining and Metallurgy, Traffic Engineering, Precision Mechanics , Physics
    Notes: Abstract The coexisting periodic impacting motions and their multiplicity of a kind of dual component systems under harmonic excitation are analytically derived. The stability condition of a periodic impacting motion is given by analyzing the propagation of small, arbitrary perturbation from that motion. In numerical simulations, the periodic impacting motions are classified according to the system states before and after an impact. The numerical results show that there exist many types of vibro-impacts and the bifurcation of periodic vibro-impacts is not smooth.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 11
    Electronic Resource
    Electronic Resource
    Springer
    Numerical algorithms 14 (1997), S. 343-359 
    ISSN: 1572-9265
    Keywords: progressive interpolation ; stability ; spline ; shape parameters ; geometric continuity ; 41A05 ; 41A15 ; 65D05 ; 65D07
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science , Mathematics
    Notes: Abstract In this paper, we study several interpolating and smoothing methods for data which are known “progressively”. The algorithms proposed are governed by recurrence relations and our principal goal is to study their stability. A recurrence relation will be said stable if the spectral radius of the associated matrix is less than one. The iteration matrices depend on shape parameters which come either from the connection at the knots, or from the nature of the interpolant between two knots. We obtain various stability domains. Moving the parameters inside these domains leads to interesting shape effects.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 12
    Electronic Resource
    Electronic Resource
    Springer
    Journal of scientific computing 12 (1997), S. 361-369 
    ISSN: 1573-7691
    Keywords: Alternating-direction implicit ; difference scheme ; stability ; convergence
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract A new alternating-direction implicit (ADI) scheme for solving three-dimensional parabolic differential equations has been developed based on the idea of regularized difference scheme. It is unconditionally stable and second-order accurate. Further, it overcomes the drawback of the Douglas scheme and is to be very well to simulate fast transient phenomena and to efficiently capture steady state solutions of parabolic differential equations. Numerical example is illustrated.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 13
    Electronic Resource
    Electronic Resource
    Springer
    Journal of scientific computing 12 (1997), S. 215-231 
    ISSN: 1573-7691
    Keywords: Transport models ; shallow water ; splitting methods ; stability
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract We investigate the use of splitting methods for the numerical integration of three-dimensional transport-chemistry models. In particular, we investigate various possibilities for the time discretization that can take advantage of the parallelization and vectorization facilities offered by multi-processor vector computers. To suppress wiggles in the numerical solution, we use third-order, upwind-biased discretization of the advection terms, resulting in a five-point coupling in each direction. As an alternative to the usual splitting functions, such as co-ordinate splitting or operator splitting, we consider a splitting function that is based on a three-coloured hopscotch-type splitting in the horizontal direction, whereas full coupling is retained in the vertical direction. Advantages of this splitting function are the easy application of domain decomposition techniques and unconditional stability in the vertical, which is an important property for transport in shallow water. The splitting method is obtained by combining the hopscotch-type splitting function with various second-order splitting formulae from the literature. Although some of the resulting methods are highly accurate, their stability behaviour (due to horizontal advection) is quite poor. Therefore we also discuss several new splitting formulae with the aim to improve the stability characteristics. It turns out that this is possible indeed, but the price to pay is a reduction of the accuracy. Therefore, such methods are to be preferred if accuracy is less crucial than stability; such a situation is frequently encountered in solving transport problems. As part of the project TRUST (Transport and Reactions Unified by Splitting Techniques), preliminary versions of the schemes are implemented on the Cray C98 4256 computer and are available for benchmarking.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 14
    Electronic Resource
    Electronic Resource
    Springer
    Journal of scientific computing 12 (1997), S. 353-360 
    ISSN: 1573-7691
    Keywords: Alternating-direction implicit ; difference scheme ; stability ; convergence
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract A generalized Peaceman–Rachford alternating-direction implicit (ADI) scheme for solving two-dimensional parabolic differential equations has been developed based on the idea of regularized difference scheme. It is to be very well to simulate fast transient phenomena and to efficiently capture steady state solutions of parabolic differential equations. Numerical example is illustrated.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 15
    Electronic Resource
    Electronic Resource
    Springer
    Rheologica acta 36 (1997), S. 367-383 
    ISSN: 1435-1528
    Keywords: Viscoelastic flow ; arrays of cylinders ; stability ; porous media
    Source: Springer Online Journal Archives 1860-2000
    Topics: Chemistry and Pharmacology , Physics
    Notes: Abstract Low Reynolds number flow of Newtonian and viscoelastic Boger fluids past periodic square arrays of cylinders with a porosity of 0.45 and 0.86 has been studied. Pressure drop measurements along the flow direction as a function of flow rate as well as flow visualization has been performed to investigate the effect of fluid elasticity on stability of this class of flows. It has been shown that below a critical Weissenberg number (Wec), the flow in both porosity cells is a two-dimensional steady flow, however, pressure fluctuations appear above Wec which is 2.95±0.25 for the 0.45 porosity cell and 0.95±0.08 for the higher porosity cell. Specifically, in the low porosity cell as the Weissenberg number is increased above Wec a transition between a steady two-dimensional to a transient three-dimensional flow occurs. However, in the high porosity cell a transition between a steady two-dimensional to a steady three-dimensional flow consisting of periodic cellular structures along the length of the cylinder in the space between the first and the second cylinder occurs while past the second cylinder another transition to a transient three-dimensional flow occurs giving rise to time- dependent cellular structures of various wavelengths along the length of the cylinder. Overall, the experiments indicate that viscoelastic flow past periodic arrays of cylinders of various porosities is susceptible to purely elastic instabilities. Moreover, the instability observed in lower porosity cells where a vortex is present between the cylinders in the base flow is amplifieds spatially, that is energy from the mean flow is continuously transferred to the disturbance flow along the flow direction. This instability gives rise to a rapid increase in flow resistance. In higher porosity cells where a vortex between the cylinders is not present in the base flow, the energy associated with the disturbance flow is not greatly changed along the flow direction past the second cylinder. In addition, it has been shown that in both flow cells the instability is a sensitive function of the relaxation time of the fluid. Hence, the instability in this class of flows is a strong function of the base flow kinematics (i.e., curvature of streamlines near solid surfaces), We and the relaxation time of the fluid.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 16
    Electronic Resource
    Electronic Resource
    Springer
    Rheologica acta 36 (1997), S. 367-383 
    ISSN: 1435-1528
    Keywords: Key words Viscoelastic flow ; arrays of cylinders ; stability ; porous media
    Source: Springer Online Journal Archives 1860-2000
    Topics: Chemistry and Pharmacology , Physics
    Notes: Abstract Low Reynolds number flow of Newtonian and viscoelastic Boger fluids past periodic square arrays of cylinders with a porosity of 0.45 and 0.86 has been studied. Pressure drop measurements along the flow direction as a function of flow rate as well as flow visualization has been performed to investigate the effect of fluid elasticity on stability of this class of flows. It has been shown that below a critical Weissenberg number (We c ), the flow in both porosity cells is a two-dimensional steady flow, however, pressure fluctuations appear above We c which is 2.95±0.25 for the 0.45 porosity cell and 0.95±0.08 for the higher porosity cell. Specifically, in the low porosity cell as the Weissenberg number is increased above We c a transition between a steady two-dimensional to a transient three-dimensional flow occurs. However, in the high porosity cell a transition between a steady two-dimensional to a steady three-dimensional flow consisting of periodic cellular structures along the length of the cylinder in the space between the first and the second cylinder occurs while past the second cylinder another transition to a transient three-dimensional flow occurs giving rise to time- dependent cellular structures of various wavelengths along the length of the cylinder. Overall, the experiments indicate that viscoelastic flow past periodic arrays of cylinders of various porosities is susceptible to purely elastic instabilities. Moreover, the instability observed in lower porosity cells where a vortex is present between the cylinders in the base flow is amplified spatially, that is energy from the mean flow is continuously transferred to the disturbance flow along the flow direction. This instability gives rise to a rapid increase in flow resistance. In higher porosity cells where a vortex between the cylinders is not present in the base flow, the energy associated with the disturbance flow is not greatly changed along the flow direction past the second cylinder. In addition, it has been shown that in both flow cells the instability is a sensitive function of the relaxation time of the fluid. Hence, the instability in this class of flows is a strong function of the base flow kinematics (i.e., curvature of streamlines near solid surfaces), We and the relaxation time of the fluid.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 17
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 139-162 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; design
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Running a competition for automated theorem proving (ATP) systems is a difficult and arguable venture. However, the potential benefits of such an event by far outweigh the controversial aspects. The motivations for running the CADE-13 ATP System Competition were to contribute to the evaluation of ATP systems, to stimulate ATP research and system development, and to expose ATP systems to researchers both within and outside the ATP community. This article identifies and discusses the issues that determine the nature of such a competition. Choices and motivated decisions for the CADE-13 competition, with respect to the issues, are given.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 18
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 205-210 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; LINUS ; first-order logic ; hyperlinking ; mate saturation
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract LINUS is a theorem prover for clause logic based on hyperlinking. The main new feature of the system is the emphasis on the preference for unit clauses, which are generated as a by-product of the hyperlinking method. The mechanism of unit support also motivates a slightly different interpretation of hyperlinking, namely, as mate saturation. Mate saturation can be viewed as a generalization of unit-resulting resolution that is compatible with any set-of-support strategy. We give a survey on the theoretical background and the architecture of the system, and decribe its performance.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 19
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 227-236 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; Satchmo ; compilation ; incremental evaluation
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Compiling Satchmo and Functional Satchmo are two variants of the model generator Satchmo, incorporating enhancements in different directions. Compiling Satchmo is based on the observation that Satchmo (like any model generator or theorem prover) can be seen as an interpreter for a program given as a logical theory, and that this interpretation layer can be avoided by compilation of the theory into a directly executable program. Functional Satchmo is an implementation of Satchmo's calculus in a purely functional language supporting lazy evaluation.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 20
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 271-286 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; results
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The CADE-13 ATP System Competition tested 18 ATP systems on 50 theorems, in five competition categories, with a time limit of 300 seconds imposed on each system run. This article records the results of the competition. Some analysis of these results is given, and interesting points are highlighted.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 21
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 171-176 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; Barcelona ; data structures and algorithms ; implementation
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Here we describe the equational theorem prover Barcelona, in its version that participated in the CADE-13 ATP System Competition. The system was built on top of our toolkit of data structures and algorithms for automated deduction in first-order logic with equality and was devised mainly to test the performance of this toolkit.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 22
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 189-198 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; DISCOUNT ; distributed theorem proving ; reactive planning ; learning
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The DISCOUNT system is a distributed equational theorem prover based on the teamwork method for knowledge-based distribution. It uses an extended version of unfailing Knuth–Bendix completion that is able to deal with arbitrarily quantified goals. DISCOUNT features many different control strategies that cooperate using the teamwork approach. Competition between multiple strategies, combined with reactive planning, results in an adaptation of the whole system to given problems, and thus in a very high degree of independence from user interaction. Teamwork also provides a suitable framework for the use of control strategies based on learning from previous proof experiences. One of these strategies forms the core of the expert global_learn, which is capable of learning from successful proofs of several problems. This expert, running sequentially, was one of the entrants in the competition (DISCOUNT/GL), while a distributed DISCOUNT system running on two workstations was another en trant.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 23
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 247-252 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; SPASS ; sorts ; superposition
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract This article describes SPASS, Version 0.49, as it was entered in the system competition at CADE-13. SPASS is an automated theorem prover for full first-order logic with equality. It is based on the superposition calculus originally developed by Bachmair and Ganzinger, extended by the sort techniques due to Weidenbach and an inference rule for case analysis.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 24
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 259-264 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; Violet ; resolution ; locking ; term rewriting ; Knuth–Bendix completion
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Violet is an easy-to-use theorem prover based on locking resolution, with integrated equality extensions that use term rewriting and Knuth–Bendix completion. Violet participated in the CADE-13 ATP System Competition.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 25
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 237-246 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; SETHEO ; E-SETHEO ; first-order logic ; model elimination ; equality
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The model elimination theorem prover SETHEO (version V3.3) and its equational extension E-SETHEO are presented. SETHEO employs sophisticated mechanisms of subgoal selection, elaborate iterative deepening techniques, and local failure caching methods. Its equational counterpart E-SETHEO transforms formulae containing equality (using a variant of Brand's modification method) and processes the output with the standard SETHEO system. This article gives an overview of the theoretical background, the system architecture, and the performance of both systems.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 26
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 265-270 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; Waldmeister ; unfailing Knuth–Bendix completion
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Waldmeister is a high-performance theorem prover for unit equational first-order logic. In the making of Waldmeister, we have applied an engineering approach, identifying the critical points with respect to efficiency in time and space. Our logical three-level system model consists of the basic operations on the lowest level, where we put great stress on efficient data structures and algorithms. For the middle level, where the inference steps are aggregated into an inference machine, flexible adjustment has proven essential during experimental evaluation. The top level holds control strategy and reduction ordering. Although at this level only standard strategies are employed, really large proof tasks have been managed in reasonable time.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 27
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 105-134 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; Gentzen system ; natural deduction ; unification algorithm
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract A natural deduction system was adapted from Gentzen system. It enables valid wffs to be deduced in a very ‘natural’ way. One need not transform a formula into other normal forms. Robinson’s unification algorithm is used to handle clausal formulas. Algorithms for eliminating and introducing quantifiers without Skolemization are presented, and unification theorems for them are proved. A natural deduction automated theorem prover based on the algorithms was implemented. The rules for quantifiers are controlled by the algorithms. The Andrews challenge and the halting problem were proved by the system.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 28
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 163-169 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; procedures
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract This article describes the practical procedures that were used to run the CADE-13 ATP System Competition. The article describes the hardware and software environments, the system installation, the soundness testing performed, the preparation of problems for the competition, the choice of the number of problems and the time limit, and the execution of the systems.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 29
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 199-204 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; Gandalf ; resolution ; subsumption
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract We give a brief overview of the first-order classical logic component in the Gandalf family of resolution-based automated theorem provers for classical and intuitionistic logics. The main strength of the described version is a sophisticated algorithm for nonunit subsumption.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 30
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 221-226 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; RRTP ; replacement ; instance based theorem prover ; propositional calculus decision procedure
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The Replacement Rule Theorem Prover (RRTP) is an instance-based, refutational, first-order clausal theorem prover. The prover is motivated by the idea of selectively replacing predicates by their definitions, and operates by selecting relevant instances of the input clauses. The relevant instances are grounded, if necessary, and tested for unsatisfiability by using a fast propositional calculus decision procedure.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 31
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 253-258 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; SPTHEO ; parallel search ; static partitioning with slackness
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract SPTHEO v3.3 is a parallelization of the sequential first-order theorem prover SETHEO v3.3. The parallelization is based on the SPS-model (Static Partitioning with Slackness) for parallel search, an approach that minimizes the processor-to-processor communication. This model allows efficient computations on hardware with weak communication performance, such as workstation networks. SPTHEO offers the utilization of both OR- and independent-AND parallelism. In this article, a detailed description and evaluation of the OR-parallel part used in the CADE-13 ATP System Competition are given.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 32
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 287-296 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; conclusions
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The CADE-13 ATP System Competition was the first large-scale controlled competition for first-order ATP systems. Many people have commented on various aspects of the competition, including some suggestions for future improvement. These comments, and some discussion of them, are contained in this article. An overview of the major issues that will affect future competitions is given.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 33
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 183-188 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; CLIN-S ; semantics ; hyper-linking ; resolution
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract CLIN-S is an instance-based, clause-form first-order theorem prover. CLIN-S employs three inference procedures: semantic hyper-linking, which uses semantics to guide the proof search and performs well on non-Horn parts of the proofs involving small literals, rough resolution, which removes large literals in the proofs, and UR resolution, which proves the Horn parts of the proofs. A semantic structure for the input clauses is given as input. During the search for the proof, ground instances of the input clauses are generated and new semantic structures are built based on the input semantics and a model of the ground clause set. A proof is found if the ground clause set is unsatisfiable. In this article, we describe the system architecture and major inference rules used in CLIN-S.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 34
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 177-182 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; CLIN-E ; hyper-linking ; smallest instance first hyper-linking
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Hyper-linking is an instance-based automated theorem proving strategy that uses unification to generate instances of the input clauses. Lee implemented hyper-linking in the automated theorem prover CLIN, which uses a breadth-first strategy for generating instances of clauses via the hyper-link operation. In attempting to add equality support to CLIN, a number of inefficiencies with Lee's breadth-first strategy for generating instances were encountered. An alternative depth-first strategy, referred to as smallest-instance-first hyper-linking, for generating instances via the hyper-link operation was developed to address these inefficiencies. Smallest-instance-first hyper-linking is implemented in the automated theorem prover CLIN-E.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 35
    Electronic Resource
    Electronic Resource
    Springer
    Journal of automated reasoning 18 (1997), S. 211-220 
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; Otter ; automated reasoning ; equational deduction ; paramodulation ; resolution
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract This article discusses the two incarnations of Otter entered in the CADE-13 Automated Theorem Proving System Competition. Also presented are some historical background, a summary of applications that have led to new results in mathematics and logic, and a general discussion of Otter.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 36
    Electronic Resource
    Electronic Resource
    Springer
    Journal of statistical physics 87 (1997), S. 1145-1164 
    ISSN: 1572-9613
    Keywords: Fisher-Kolmogorov equation ; traveling fronts ; fixed points ; population dynamics ; bifurcations ; stability
    Source: Springer Online Journal Archives 1860-2000
    Topics: Physics
    Notes: Abstract The one-dimensional reaction-diffusion equations for the process (D) $$A + B \to 2A,B + C \to 2B,C + A \to 2C$$ are extended to include the counteracting reactions (R) $$A + 2B \to 3B,B + 2C \to 3C,C + 2A \to 3A$$ which have a reaction rate α relative to the direct process (D). This process can be seen as a three-component version of the reaction which is described by the Fisher-Kolmogorov equation. The fixed points of the equations are studied as a function of α. It is shown that the equations admit solutions which consist of a series of traveling fronts. Other solutions exist which are traveling periodic waves. A very remarkable fact is that for these waves exact expressions can be constructed.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 37
    ISSN: 1573-0778
    Keywords: CHO cells ; DHFR ; IGFBP-1 ; stability
    Source: Springer Online Journal Archives 1860-2000
    Topics: Biology , Medicine , Process Engineering, Biotechnology, Nutrition Technology
    Notes: Abstract Stable expression of human insulin-like growth factor of binding protein-1 (hIGFBP-1)at high levels has been achieved in Chinese hamster ovary (CHO) cells by co-transfection and subsequent co-amplification of expression vectors containing the hIGFBP-1 cDNA and a dihydrofolate reductase (DHFR) cDNA gene into DHFR-deficient cells. Stepwise selection of the DHFR+ transformants in increasing concentrations of methotrexate (MTX) generated cells which had high copy numbers of the hIGFBP-1 gene (around 100 copies in cells amplified in medium containing 100 nM MTX). Expression of hIGFBP-1 in mixed clones was found to increase with increasing copy number and an apparent correlation between intra- and extracellular levels of hIGFBP-1 produced by these cells was observed. It was further observed that continuous cultivation over eight months in medium supplemented with 100 nM MTX increased the production of hIGFBP-1 25 times. The productivity did not increase further after five more months cultivation in MTX containing medium. A subcloning of this cell line gave clones with an even higher productivity. Further amplification in 500 nM or 1 uM MTX did not increase the hIGFBP-1 production.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 38
    Electronic Resource
    Electronic Resource
    Springer
    Journal of elasticity 48 (1997), S. 218-239 
    ISSN: 1573-2681
    Keywords: stability ; nonlinear elasticity ; Mooney-Rivlin material ; incompressible material ; thick-walled tube
    Source: Springer Online Journal Archives 1860-2000
    Topics: Mechanical Engineering, Materials Science, Production Engineering, Mining and Metallurgy, Traffic Engineering, Precision Mechanics , Physics
    Notes: Abstract The problem of instability of a hyperelastic, thick-walled cylindrical tube was first studied by Wilkes [1] in 1955. The solution was formulated within the framework of the theory of small deformations superimposed on large homogeneous deformations for the general class of incompressible, isotropic materials; and results for axially symmetrical buckling were obtained for the neo-Hookean material. The solution involves a certain quadratic equation whose characteristic roots depend on the material response functions. For the neo-Hookean material these roots always are positive. In fact, here we show for the more general Mooney–Rivlin material that these roots always are positive, provided the empirical inequalities hold. In a recent study [2] of this problem for a class of internally constrained compressible materials, it is observed that these characteristic roots may be real-valued, pure imaginary, or complex-valued. The similarity of the analytical structure of the two problems, however, is most striking; and this similarity leads one to question possible complex-valued solutions for the incompressible case. Some remarks on this issue will be presented and some new results will be reported, including additional results for both the neo-Hookean and Mooney–Rivlin materials.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...