-
Model Validation of a Low-Speed and Reverse Driving Articulated Vehicle
Authors:
Viral Gosar,
Mohsen Alirezaei,
Igo Besselink,
Henk Nijmeijer
Abstract:
For the autonomous operation of articulated vehicles at distribution centers, accurate positioning of the vehicle is of the utmost importance. Automation of these vehicle poses several challenges, e.g. large swept path, asymmetric steering response, large slide slip angles of non-steered trailer axles and trailer instability while reversing. Therefore, a validated vehicle model is required that ac…
▽ More
For the autonomous operation of articulated vehicles at distribution centers, accurate positioning of the vehicle is of the utmost importance. Automation of these vehicle poses several challenges, e.g. large swept path, asymmetric steering response, large slide slip angles of non-steered trailer axles and trailer instability while reversing. Therefore, a validated vehicle model is required that accurately and efficiently predicts the states of the vehicle. Unlike forward driving, open-loop validation methods can not be used for reverse driving of articulated vehicles due to their unstable dynamics. This paper proposes an approach to stabilize the unstable pole of the system and compares three vehicle models (kinematic, non-linear single track and multibody dynamics model) against real-world test data obtained from low-speed experiments at a distribution center. It is concluded that single track non-linear model has a better performance in comparison to other models for large articulation angles and reverse driving maneuvers.
△ Less
Submitted 1 October, 2023;
originally announced October 2023.
-
Fast fluid heating by adaptive flow reorientation
Authors:
R. Lensvelt,
M. F. M Speetjens,
H. Nijmeijer
Abstract:
Scalar transport (e.g. heat or chemical species) in laminar flows is key to many industrial activities and fluid stirring by flow reorientation is a common way to enhance this process. However, "How best to stir?" remains a major challenge. This study aims to contribute to existing solutions by the development of a dedicated flow-control strategy for the fast heating of a cold fluid via a hot boun…
▽ More
Scalar transport (e.g. heat or chemical species) in laminar flows is key to many industrial activities and fluid stirring by flow reorientation is a common way to enhance this process. However, "How best to stir?" remains a major challenge. This study aims to contribute to existing solutions by the development of a dedicated flow-control strategy for the fast heating of a cold fluid via a hot boundary in a representative case study. Fluid deformation acts as the "thermal actuator" via which the flow affects heat transfer yet this may both enhance and diminish heat exchange between fluid parcels and thus restricts the beneficial impact of flow. Moreover, the impact of fluid deformation on the global fluid heating is primarily confined to the proximity of the moving boundary that drives the flow. These insights make incorporation of thermal behaviour essential for effective flow-based enhancement strategies and expose fluid mixing, the conventional approach in industry, as potentially sub-optimal. The notion that global heating encompasses two concurrent processes, i.e. increasing energy content and thermal homogenisation, yields the relevant metrics for the formulation of the control problem as the minimisation of a dedicated cost function. This facilitates step-wise determination of the "best" flow reorientation from predicted future evolutions of actual intermediate states and thereby paves the way to (real-time) regulation of scalar transport by flow control. Performance analyses reveal that this "adaptive flow reorientation" significantly accelerates fluid heating and thus is superior to conventional periodic schemes (designed for efficient fluid mixing) both in consistency and effectiveness. The controller in fact never selects these periodic schemes and achieves the same superior performance for all flow conditions irrespective of whether said mixing occurs.
△ Less
Submitted 21 December, 2021;
originally announced December 2021.
-
Nonlinear Tracking and Rejection using Linear Parameter-Varying Control
Authors:
Patrick J. W. Koelewijn,
Roland Tóth,
Henk Nijmeijer,
Siep Weiland
Abstract:
The Linear Parameter-Varying (LPV) framework has been introduced with the intention to provide stability and performance guarantees for analysis and controller synthesis for Nonlinear (NL) systems via convex methods. By extending results of the Linear Time-Invariant framework, mainly based on quadratic stability and performance using dissipativity theory, it has been assumed that they generalize t…
▽ More
The Linear Parameter-Varying (LPV) framework has been introduced with the intention to provide stability and performance guarantees for analysis and controller synthesis for Nonlinear (NL) systems via convex methods. By extending results of the Linear Time-Invariant framework, mainly based on quadratic stability and performance using dissipativity theory, it has been assumed that they generalize tracking and disturbance rejection guarantees for NL systems. However, as has been shown in literature, stability and performance through standard dissipativity is not sufficient in order to satisfy the desired guarantees in case of reference tracking and disturbance rejection for nonlinear systems. We propose to solve this problem by the application of incremental dissipativity, which does ensure these specifications. A novel approach is proposed to synthesize and realize an NL controller which is able to guarantee incremental stability and performance for NL systems via convex optimization using methods from the LPV framework. Through simulations and experiments, the presented method is compared to standard LPV controller designs, showing significant performance improvements.
△ Less
Submitted 7 March, 2023; v1 submitted 20 April, 2021;
originally announced April 2021.
-
Linear Parameter-Varying Control of Nonlinear Systems based on Incremental Stability
Authors:
P. J. W. Koelewijn,
R. Tóth,
H. Nijmeijer
Abstract:
The Linear Parameter-Varying (LPV) framework has long been used to guarantee performance and stability requirements of nonlinear (NL) systems mainly through the $\mathcal{L}_2$-gain concept. However, recent research has pointed out that current $\mathcal{L}_2$-gain based LPV synthesis methods can fail to guarantee these requirements if stabilization of a non-zero operating condition (e.g. referenc…
▽ More
The Linear Parameter-Varying (LPV) framework has long been used to guarantee performance and stability requirements of nonlinear (NL) systems mainly through the $\mathcal{L}_2$-gain concept. However, recent research has pointed out that current $\mathcal{L}_2$-gain based LPV synthesis methods can fail to guarantee these requirements if stabilization of a non-zero operating condition (e.g. reference tracking, constant disturbance rejection, etc.) is required. In this paper, an LPV based synthesis method is proposed which is able to guarantee incremental performance and stability of an NL system even with reference and disturbance rejection objectives. The developed approach and the current $\mathcal{L}_2$ LPV synthesis method are compared in a simulation study of the position control problem of a Duffing oscillator, showing performance improvements of the proposed method compared to the current $\mathcal{L}_2$-based approach for tracking and disturbance rejection.
△ Less
Submitted 16 September, 2019;
originally announced September 2019.
-
A Stochastic Model Predictive Control Approach for Driver-Aided Intersection Crossing With Uncertain Driver Time Delay
Authors:
Alexander Katriniok,
Stefan Kojchev,
Erjen Lefeber,
Henk Nijmeijer
Abstract:
We investigate the problem of coordinating human-driven vehicles in road intersections without any traffic lights or signs by issuing speed advices. The vehicles in the intersection are assumed to move along an a priori known path and to be connected via vehicle-to-vehicle communication. The challenge arises with the uncertain driver reaction to a speed advice, especially in terms of the driver re…
▽ More
We investigate the problem of coordinating human-driven vehicles in road intersections without any traffic lights or signs by issuing speed advices. The vehicles in the intersection are assumed to move along an a priori known path and to be connected via vehicle-to-vehicle communication. The challenge arises with the uncertain driver reaction to a speed advice, especially in terms of the driver reaction time delay, as it might lead to unstable system dynamics. For this control problem, a distributed stochastic model predictive control concept is designed which accounts for driver uncertainties. By optimizing over scenarios, which are sequences of independent and identically distributed samples of the uncertainty over the prediction horizon, we can give probabilistic guarantees on constraint satisfaction. Simulation results demonstrate that the scenario-based approach is able to avoid collisions in spite of uncertainty while the non-stochastic baseline controller is not.
△ Less
Submitted 29 March, 2019;
originally announced March 2019.
-
Synchronization in Networks of Diffusively Coupled Nonlinear Systems: Robustness Against Time-Delays
Authors:
Carlos Murguia,
Henk Nijmeijer,
Justin Ruths
Abstract:
In this manuscript, we study the problem of robust synchronization in networks of diffusively time-delayed coupled nonlinear systems. In particular, we prove that, under some mild conditions on the input-output dynamics of the systems and the network topology, there always exists a unimodal region in the parameter space (coupling strength versus time-delay), such that if they belong to this region…
▽ More
In this manuscript, we study the problem of robust synchronization in networks of diffusively time-delayed coupled nonlinear systems. In particular, we prove that, under some mild conditions on the input-output dynamics of the systems and the network topology, there always exists a unimodal region in the parameter space (coupling strength versus time-delay), such that if they belong to this region, the systems synchronize. Moreover, we show how this unimodal region scales with the network topology, which, in turn, provides useful insights on how to design the network topology to maximize robustness against time-delays. The results are illustrated by extensive simulation experiments of time-delayed coupled Hindmarsh-Rose neural chaotic oscillators.
△ Less
Submitted 30 October, 2017;
originally announced October 2017.
-
On Centroidal Dynamics and Integrability of Average Angular Velocity
Authors:
Alessandro Saccon,
Silvio Traversaro,
Francesco Nori,
Henk Nijmeijer
Abstract:
In the literature on robotics and multibody dynamics, the concept of average angular velocity has received considerable attention in recent years. We address the question of whether the average angular velocity defines an orientation framethat depends only on the current robot configuration and provide a simple algebraic condition to check whether this holds. In the language of geometric mechanics…
▽ More
In the literature on robotics and multibody dynamics, the concept of average angular velocity has received considerable attention in recent years. We address the question of whether the average angular velocity defines an orientation framethat depends only on the current robot configuration and provide a simple algebraic condition to check whether this holds. In the language of geometric mechanics, this condition corresponds to requiring the flatness of the mechanical connection associated to the robotic system. Here, however, we provide both a reinterpretation and a proof of this result accessible to readers with a background in rigid body kinematics and multibody dynamics but not necessarily acquainted with differential geometry, still providing precise links to the geometric mechanics literature. This should help spreading the algebraic condition beyond the scope of geometric mechanics,contributing to a proper utilization and understanding of the concept of average angular velocity.
△ Less
Submitted 10 January, 2017;
originally announced January 2017.
-
Switching control for tracking of a hybrid position-force trajectory
Authors:
D. J. F. Heck,
A. Saccon,
N. van de Wouw,
H. Nijmeijer
Abstract:
This work proposes a control law for a manipulator with the aim of realizing desired time-varying motion-force profiles in the presence of a stiff environment. In many cases, the interaction with the environment affects only one degree of freedom of the end-effector of the manipulator. Therefore, the focus is on this contact degree of freedom, and a switching position-force controller is proposed…
▽ More
This work proposes a control law for a manipulator with the aim of realizing desired time-varying motion-force profiles in the presence of a stiff environment. In many cases, the interaction with the environment affects only one degree of freedom of the end-effector of the manipulator. Therefore, the focus is on this contact degree of freedom, and a switching position-force controller is proposed to perform the hybrid position-force tracking task. Sufficient conditions are presented to guarantee input-to-state stability of the switching closed-loop system with respect to perturbations related to the time-varying desired motion-force profile. The switching occurs when the manipulator makes or breaks contact with the environment. The analysis shows that to guarantee closed-loop stability while tracking arbitrary time-varying motion-force profiles, the controller should implement a considerable (and often unrealistic) amount of dam**, resulting in inferior tracking performance. Therefore, we propose to redesign the manipulator with a compliant wrist. Guidelines are provided for the design of the compliant wrist while employing the designed switching control strategy, such that stable tracking of a motion-force reference trajectory can be achieved and bouncing of the manipulator while making contact with the stiff environment can be avoided. Finally, numerical simulations are presented to illustrate the effectiveness of the approach.
△ Less
Submitted 2 March, 2015;
originally announced March 2015.
-
Adaptive observers for nonlinearly parameterized systems subjected to parametric constraints
Authors:
I. Yu. Tyukin,
P. A. Rogachev,
H. Nijmeijer
Abstract:
We consider the problem of adaptive observer design in the settings when the system is allowed to be nonlinear in the parameters, and furthermore they are to satisfy additional feasibility constraints. A solution to the problem is proposed that is based on the idea of universal observers and non-uniform small-gain theorem. The procedure is illustrated with an example.
We consider the problem of adaptive observer design in the settings when the system is allowed to be nonlinear in the parameters, and furthermore they are to satisfy additional feasibility constraints. A solution to the problem is proposed that is based on the idea of universal observers and non-uniform small-gain theorem. The procedure is illustrated with an example.
△ Less
Submitted 17 December, 2014;
originally announced December 2014.
-
Further Results on Lyapunov-Like Conditions of Forward Invariance and Boundedness for a Class of Unstable Systems
Authors:
A. N. Gorban,
I. Yu. Tyukin,
H. Nijmeijer
Abstract:
We provide several characterizations of convergence to unstable equilibria in nonlinear systems. Our current contribution is three-fold. First we present simple algebraic conditions for establishing local convergence of non-trivial solutions of nonlinear systems to unstable equilibria. The conditions are based on the earlier work (A.N. Gorban, I.Yu. Tyukin, E. Steur, and H. Nijmeijer, SIAM Journal…
▽ More
We provide several characterizations of convergence to unstable equilibria in nonlinear systems. Our current contribution is three-fold. First we present simple algebraic conditions for establishing local convergence of non-trivial solutions of nonlinear systems to unstable equilibria. The conditions are based on the earlier work (A.N. Gorban, I.Yu. Tyukin, E. Steur, and H. Nijmeijer, SIAM Journal on Control and Optimization, Vol. 51, No. 3, 2013) and can be viewed as an extension of the Lyapunov's first method in that they apply to systems in which the corresponding Jacobian has one zero eigenvalue. Second, we show that for a relevant subclass of systems, persistency of excitation of a function of time in the right-hand side of the equations governing dynamics of the system ensure existence of an attractor basin such that solutions passing through this basin in forward time converge to the origin exponentially. Finally we demonstrate that conditions developed in (A.N. Gorban, I.Yu. Tyukin, E. Steur, and H. Nijmeijer, SIAM Journal on Control and Optimization, Vol. 51, No. 3, 2013) may be remarkably tight.
△ Less
Submitted 1 December, 2014;
originally announced December 2014.
-
Sensitivity analysis of hybrid systems with state jumps with application to trajectory tracking
Authors:
Alessandro Saccon,
Nathan van de Wouw,
Henk Nijmeijer
Abstract:
This paper addresses the sensitivity analysis for hybrid systems with discontinuous (jum**) state trajectories. We consider state-triggered jumps in the state evolution, potentially accompanied by mode switching in the control vector field as well. For a given trajectory with state jumps, we show how to construct an approximation of a nearby perturbed trajectory corresponding to a small variatio…
▽ More
This paper addresses the sensitivity analysis for hybrid systems with discontinuous (jum**) state trajectories. We consider state-triggered jumps in the state evolution, potentially accompanied by mode switching in the control vector field as well. For a given trajectory with state jumps, we show how to construct an approximation of a nearby perturbed trajectory corresponding to a small variation of the initial condition and input. A major complication in the construction of such an approximation is that, in general, the jump times corresponding to a nearby perturbed trajectory are not equal to those of the nominal one. The main contribution of this work is the development of a notion of error to clarify in which sense the approximate trajectory is, at each instant of time, a firstorder approximation of the perturbed trajectory. This notion of error naturally finds application in the (local) tracking problem of a time-varying reference trajectory of a hybrid system. To illustrate the possible use of this new error definition in the context of trajectory tracking, we outline how the standard linear trajectory tracking control for nonlinear systems -based on linear quadratic regulator (LQR) theory to compute the optimal feedback gain- could be generalized for hybrid systems.
△ Less
Submitted 11 June, 2014;
originally announced June 2014.
-
Supplementary material for: Adaptive Observers and Parameter Estimation for a Class of Systems Nonlinear in the Parameters
Authors:
Ivan Tyukin,
Erik Steur,
Henk Nijmeijer,
Cees van Leeuwen
Abstract:
This supplement illustrates application of adaptive observer design from (Tyukin et al, 2013) for systems which are not uniquely identifiable. It also provides an example of adaptive observer design for a magnetic bearings benchmark system (Lin, Knospe, 2000).
This supplement illustrates application of adaptive observer design from (Tyukin et al, 2013) for systems which are not uniquely identifiable. It also provides an example of adaptive observer design for a magnetic bearings benchmark system (Lin, Knospe, 2000).
△ Less
Submitted 16 April, 2013; v1 submitted 15 April, 2013;
originally announced April 2013.
-
Collective Almost Synchronization in Complex Networks
Authors:
M. S. Baptista,
Hai-Peng Ren,
J. C. M. Swarts,
R. Carareto,
H. Nijmeijer,
C. Grebogi
Abstract:
This work introduces the phenomenon of Collective Almost Synchronization (CAS), which describes a universal way of how patterns can appear in complex networks even for small coupling strengths. The CAS phenomenon appears due to the existence of an approximately constant local mean field and is characterized by having nodes with trajectories evolving around periodic stable orbits. Common notion bas…
▽ More
This work introduces the phenomenon of Collective Almost Synchronization (CAS), which describes a universal way of how patterns can appear in complex networks even for small coupling strengths. The CAS phenomenon appears due to the existence of an approximately constant local mean field and is characterized by having nodes with trajectories evolving around periodic stable orbits. Common notion based on statistical knowledge would lead one to interpret the appearance of a local constant mean field as a consequence of the fact that the behavior of each node is not correlated to the behaviors of the others. Contrary to this common notion, we show that various well known weaker forms of synchronization (almost, time-lag, phase synchronization, and generalized synchronization) appear as a result of the onset of an almost constant local mean field. If the memory is formed in a brain by minimising the coupling strength among neurons and maximising the number of possible patterns, then the CAS phenomenon is a plausible explanation for it.
△ Less
Submitted 9 April, 2012;
originally announced April 2012.
-
Observers for canonic models of neural oscillators
Authors:
David Fairhurst,
Ivan Tyukin,
Henk Nijmeijer,
Cees van Leeuwen
Abstract:
We consider the problem of state and parameter estimation for a wide class of nonlinear oscillators. Observable variables are limited to a few components of state vector and an input signal. The problem of state and parameter reconstruction is viewed within the classical framework of observer design. This framework offers computationally-efficient solutions to the problem of state and parameter re…
▽ More
We consider the problem of state and parameter estimation for a wide class of nonlinear oscillators. Observable variables are limited to a few components of state vector and an input signal. The problem of state and parameter reconstruction is viewed within the classical framework of observer design. This framework offers computationally-efficient solutions to the problem of state and parameter reconstruction of a system of nonlinear differential equations, provided that these equations are in the so-called adaptive observer canonic form. We show that despite typical neural oscillators being locally observable they are not in the adaptive canonic observer form. Furthermore, we show that no parameter-independent diffeomorphism exists such that the original equations of these models can be transformed into the adaptive canonic observer form. We demonstrate, however, that for the class of Hindmarsh-Rose and FitzHugh-Nagumo models, parameter-dependent coordinate transformations can be used to render these systems into the adaptive observer canonical form. This allows reconstruction, at least partially and up to a (bi)linear transformation, of unknown state and parameter values with exponential rate of convergence. In order to avoid the problem of only partial reconstruction and to deal with more general nonlinear models in which the unknown parameters enter the system nonlinearly, we present a new method for state and parameter reconstruction for these systems. The method combines advantages of standard Lyapunov-based design with more flexible design and analysis techniques based on the non-uniform small-gain theorems. Effectiveness of the method is illustrated with simple numerical examples.
△ Less
Submitted 18 June, 2010; v1 submitted 1 May, 2009;
originally announced May 2009.
-
Semi-passivity and synchronization of diffusively coupled neuronal oscillators
Authors:
Erik Steur,
Ivan Tyukin,
Henk Nijmeijer
Abstract:
We discuss synchronization in networks of neuronal oscillators which are interconnected via diffusive coupling, i.e. linearly coupled via gap junctions. In particular, we present sufficient conditions for synchronization in these networks using the theory of semi-passive and passive systems. We show that the conductance-based neuronal models of Hodgkin-Huxley, Morris-Lecar, and the popular reduc…
▽ More
We discuss synchronization in networks of neuronal oscillators which are interconnected via diffusive coupling, i.e. linearly coupled via gap junctions. In particular, we present sufficient conditions for synchronization in these networks using the theory of semi-passive and passive systems. We show that the conductance-based neuronal models of Hodgkin-Huxley, Morris-Lecar, and the popular reduced models of FitzHugh-Nagumo and Hindmarsh-Rose all satisfy a semi-passivity property, i.e. that is the state trajectories of such a model remain oscillatory but bounded provided that the supplied (electrical) energy is bounded. As a result, for a wide range of coupling configurations, networks of these oscillators are guaranteed to possess ultimately bounded solutions. Moreover, we demonstrate that when the coupling is strong enough the oscillators become synchronized. Our theoretical conclusions are confirmed by computer simulations with coupled \HR and \ML oscillators. Finally we discuss possible "instabilities" in networks of oscillators induced by the diffusive coupling.
△ Less
Submitted 20 March, 2009;
originally announced March 2009.
-
Adaptive Observers and Parameter Estimation for a Class of Systems Nonlinear in the Parameters
Authors:
Ivan Y. Tyukin,
Erik Steur,
Henk Nijmeijer,
Cees van Leeuwen
Abstract:
We consider the problem of asymptotic reconstruction of the state and parameter values in systems of ordinary differential equations. A solution to this problem is proposed for a class of systems of which the unknowns are allowed to be nonlinearly parameterized functions of state and time. Reconstruction of state and parameter values is based on the concepts of weakly attracting sets and non-unifo…
▽ More
We consider the problem of asymptotic reconstruction of the state and parameter values in systems of ordinary differential equations. A solution to this problem is proposed for a class of systems of which the unknowns are allowed to be nonlinearly parameterized functions of state and time. Reconstruction of state and parameter values is based on the concepts of weakly attracting sets and non-uniform convergence and is subjected to persistency of excitation conditions. In absence of nonlinear parametrization the resulting observers reduce to standard estimation schemes. In this respect, the proposed method constitutes a generalization of the conventional canonical adaptive observer design.
△ Less
Submitted 21 June, 2013; v1 submitted 13 March, 2009;
originally announced March 2009.
-
Lyapunov-like Conditions of Forward Invariance and Boundedness for a Class of Unstable Systems
Authors:
A. Gorban,
I. Tyukin,
E. Steur,
H. Nijmeijer
Abstract:
We provide Lyapunov-like characterizations of boundedness and convergence of non-trivial solutions for a class of systems with unstable invariant sets. Examples of systems to which the results may apply include interconnections of stable subsystems with one-dimensional unstable dynamics or critically stable dynamics. Systems of this type arise in problems of nonlinear output regulation, parameter…
▽ More
We provide Lyapunov-like characterizations of boundedness and convergence of non-trivial solutions for a class of systems with unstable invariant sets. Examples of systems to which the results may apply include interconnections of stable subsystems with one-dimensional unstable dynamics or critically stable dynamics. Systems of this type arise in problems of nonlinear output regulation, parameter estimation and adaptive control.
In addition to providing boundedness and convergence criteria the results allow to derive domains of initial conditions corresponding to solutions leaving a given neighborhood of the origin at least once. In contrast to other works addressing convergence issues in unstable systems, our results require neither input-output characterizations for the stable part nor estimates of convergence rates. The results are illustrated with examples, including the analysis of phase synchronization of neural oscillators with heterogenous coupling.
△ Less
Submitted 11 June, 2013; v1 submitted 22 January, 2009;
originally announced January 2009.
-
Non-uniform Small-gain Theorems for Systems with Unstable Invariant Sets
Authors:
Ivan Tyukin,
Erik Steur,
Henk Nijmeijer,
Cees van Leeuwen
Abstract:
We consider the problem of asymptotic convergence to invariant sets in interconnected nonlinear dynamic systems. Standard approaches often require that the invariant sets be uniformly attracting. e.g. stable in the Lyapunov sense. This, however, is neither a necessary requirement, nor is it always useful. Systems may, for instance, be inherently unstable (e.g. intermittent, itinerant, meta-stabl…
▽ More
We consider the problem of asymptotic convergence to invariant sets in interconnected nonlinear dynamic systems. Standard approaches often require that the invariant sets be uniformly attracting. e.g. stable in the Lyapunov sense. This, however, is neither a necessary requirement, nor is it always useful. Systems may, for instance, be inherently unstable (e.g. intermittent, itinerant, meta-stable) or the problem statement may include requirements that cannot be satisfied with stable solutions. This is often the case in general optimization problems and in nonlinear parameter identification or adaptation. Conventional techniques for these cases rely either on detailed knowledge of the system's vector-fields or require boundeness of its states. The presently proposed method relies only on estimates of the input-output maps and steady-state characteristics. The method requires the possibility of representing the system as an interconnection of a stable, contracting, and an unstable, exploratory part. We illustrate with examples how the method can be applied to problems of analyzing the asymptotic behavior of locally unstable systems as well as to problems of parameter identification and adaptation in the presence of nonlinear parametrizations. The relation of our results to conventional small-gain theorems is discussed.
△ Less
Submitted 14 December, 2006;
originally announced December 2006.
