Some FMathL-related papers by our group

This page is part of the FMathL - Formal mathematical language web site at

While many of the papers whose abstract (and link for download) is given below are not directly relevant to the FMathL project, they give some background information explaining part of our motivation for embarking on this project:

  • the quest for rigorous error bounds in numerical analysis, partly using interval analysis
  • computer assisted proofs in analysis
  • modeling languages for large scale numerical problems (optimization, constraint satisfaction, partial differential equations)

    A. Neumaier, A modeling system for mathematics, Manuscript, 2008
    pdf file (144K)
    This project aims at the development of a flexible modeling system for the specification of models for large-scale numerical work in optimization, data analysis, and partial differential equations.
    Its input should be provided in a form natural for the working mathematician, while the choice of the numerical solvers and the transformation to the format required by the solvers is done by the interface system. The input format should combine the simplicity of LaTeX source code with the semantic conciseness and modularity of current modeling languages such as AMPL, and it should be as close as possible to the mathematical language people use to explain and communicate their models in publications and lectures.
    In order that the system is useful for the intended applications, interfaces translating the model formulated in the proposed system into the input required for current state of the art solvers, and into the dominant current modeling languages are needed and shall be provided.
    Moreover, certain shortcomings of the current generation of modeling languages, such as the lack of support for the correct treatment of uncertainties and rounding errors, shall be overcome.
    The experience gained in this project will be useful in future work in the more general context of mathematical knowledge management.

    A. Neumaier, Computer-assisted proofs, in: (W. Luther and W. Otten, eds.) Proc. 12th GAMM-IMACS Symp. Sci. Comp., (SCAN 2006). IEEE Computer Society, 2007.
    ps.gz file (102K), pdf file (111K)
    This paper discusses the problem what makes a computer-assisted proof trustworthy, the quest for an algorithmic support system for computer-assisted proof, relations to global optimization, an analysis of some recent proofs, and some current challenges which appear to be amenable to a computer-assisted treatment.

    T. Rage, A. Neumaier and C. Schlier, Rigorous verification of chaos in a molecular model, Phys. Rev. E. 50 (1994), 2682-2688.

    The Thiele-Wilson system, a simple model of a linear, triatomic molecule, has been studied extensively in the past. The system exhibits complex molecular dynamics including dissociation, periodic trajectories and bifurcations. In addition, it has for a long time been suspected to be chaotic, but this has never been proved with mathematical rigor.

    In this paper, we present numerical results that, using interval methods, rigorously verify the existence of transversal homoclinic points in a Poincare map of this system. By a theorem of Smale, the existence of transversal homoclinic points in a map rigorously proves its mixing property, i.e., the chaoticity of the system.

    D. Daney, Y. Papegay and A. Neumaier, Interval methods for certification of the kinematic calibration of parallel robots, pp. 191-198 in: Proc. 2004 IEEE Int. Conf. Robotics Automation, New Orleans, LA, April 2004.
    pdf file (261K)
    In this paper, we demonstrate how methods based on interval arithmetic and interval analysis can be used to achieve numerical certification of the kinematic calibration of a parallel robots. After describing the usual calibration methods and the motivations for a numerical certification, we briefly present the interval methods we used and the kinematic calibration problem. In the main part, we develop our certified approach of this problem in the case of a Gough platform, and we show with numerical examples how this approach avoids wrong solutions produced by classical approach. Details on implementation and performance are also given.

    W. Huyer and A. Neumaier, Integral approximation of rays and verification of feasibility, Reliable Computing 10 (2004), 195-207.
    ps.gz file (134K), pdf file (423K)
    An algorithm is presented that produces an integer vector nearly parallel to a given vector. The algorithm can be used to discover exact rational solutions of homogeneous or inhomogeneous linear systems of equations, given a sufficiently accurate approximate solution.
    As an application, we show how to verify rigorously the feasibility of degenerate vertices of a linear program with integer coefficients, and how to recognize rigorously certain redundant linear constraints in a given system of linear equations and inequalities. This is a first step towards the handling of degeneracies and redundandies within rigorous global optimization codes.

    A. Neumaier, Certified error bounds for uncertain elliptic equations, J. Comput. Appl. Math. 218 (2008), 125-136.
    pdf file (382K) ps.gz file (190K)
    In many applications, partial differential equations depend on parameters which are only approximately known.
    Using tools from functional analysis and global optimization, methods are presented for obtaining certificates for rigorous and realistic error bounds on the solution of linear elliptic partial differential equations in arbitrary domains, either in an energy norm, or of key functionals of the solutions, given an approximate solution.
    Uncertainty in the parameters specifying the partial differential equations can be taken into account, either in a worst case setting, or given limited probabilistic information in terms of clouds.

    H. Schichl and A. Neumaier, Transposition theorems and qualification-free optimality conditions, Siam J. Optimization 17 (2006), 1035-1055.
    ps.gz file (175K), pdf file (211K)
    New theorems of the alternative for polynomial constraints (based on the Positivstellensatz from real algebraic geometry) and for linear constraints (generalizing the transposition theorems of Motzkin and Tucker) are proved. Based on these, two Karush-John optimality conditions - holding without any constraint qualification - are proved for single- or multi-objective constrained optimization problems. The first condition applies to polynomial optimization problems only, and gives for the first time necessary and sufficient global optimality conditions for polynomial problems. The second condition applies to smooth local optimization problems and strengthens known local conditions. If some linear or concave constraints are present, the new version reduces the number of constraints for which a constraint qualification is needed to get the Kuhn-Tucker conditions.

    A. Neumaier, Mathematical Model Building, Chapter 3 in: Modeling Languages in Mathematical Optimization (J. Kallrath, ed.), Kluwer, Boston 2004.
    html version
    dvi.gz file (20K), ps.gz file (47K), pdf file (74K)
    Some notes on mathematical modeling, listing motivations, applications, a numerical toolkit, general modeling rules, modeling conflicts, useful attitudes, and structuring the modeling work into 16 related activities by means of a novel modeling diagram.

    H. Schichl, A. Neumaier and S. Dallwig, The NOP-2 modeling language, Ann. Oper. Research 104 (2001), 281-312.
    dvi.gz file (32K), ps.gz file (97K)
    An enhanced version NOP-2 of the NOP language for specifying global optimization problems is described. Because of its additional features, NOP-2 is comparable to other modeling languages like AMPL and GAMS, and allows the user to define a wide range of problems arising in real life applications such as global constrained (and even stochastic) optimization programs.
    NOP-2 permits named variables, parameters, indexing, loops, relational operators, extensive set operations, matrices and tensors, and parameter arithmetic.
    The main advantage that makes NOP-2 look and feel considerably different from other modeling languages is the display of the internal analytic structure of the problem. It is fully flexible for interfacing with solvers requiring special features such as automatic differentiation or interval arithmetic.

    A. Neumaier, Improving interval enclosures, Manuscript (2009).
    pdf file (244K)
    This paper serves as background information for the Vienna proposal for interval standardization, explaining what is needed in practice to make competent use of the interval arithmetic provided by an implementation of the standard to be.
    Discussed are methods to improve the quality of interval enclosures of the range of a function over a box, considerations of possible hardware support facilitating the implementation of such methods, and the results of a simple interval challenge that I had posed to the reliable computing mailing list on November 26, 2008.
    Also given is an example of a bound constrained global optimization problem in 4 variables that has a 2-dimensional continuum of global minimizers. This makes standard branch and bound codes extremely slow, and therefore may serve as a useful degenerate test problem.

    A. Neumaier, Towards optimization-based error bounds for uncertain PDEs, Slides, 2008
    pdf file (347K)
    Using tools from functional analysis and global optimization, methods are presented for obtaining, given an approximate solution of a partial differential equation, realistic error bounds for some response functional of the solution.

    The method is based on computable bounds for the inverse of linear elliptic operators. Like in the dual weighted residual (DWR) method, our error bounds for response functionals have the quadratic approximation property (so that they are asymptotically optimal), but in contrast to DWR, our bounds are rigorous and also capture the higher order contributions to the error.

    Using global optimization techniques, bounds can be found that not only cover the errors in solving the differential equations but also the errors caused by the uncertainty in the parameters. This provides reliable tools for the assessment of uncertainty in the solution of elliptic partial differential equations. Our bounds are independent of the way the approximations are obtained, hence can be used to independently verify the quality of an approximation computed by an arbitrary solver. The bounds not only account for discretization errors but also for other numerical errors introduced through numerical integration and boundary aproximations.

    We also discuss how to represent model uncertainty in terms of so-called clouds, which describe the rough shapes of typical samples of various size, without fixing the details of the distribution. Clouds use only information from 1- and 2-dimensional marginal distributions, readily available in practice.

    F. Domes and A. Neumaier, Directed Cholesky factorizations and applications, submitted, 2008.
    pdf file (261K)
    In exact arithmetic, the Cholesky factorization of a nonsingular symmetric matrix exists iff the matrix is positive definite. Several applications require safe tests for definiteness or to derive valid inequalities that use computations involving a Cholesky factorization.This paper introduces directed versions of the Cholesky factorization, from which rigorous conclusions can be drawn in spite of rounding errors. Applications are given to checking definiteness and to finding tight box enclosures for ellipsoids defined by strictly convex quadratic inequalities. This also provides a convenient preprocessing step for constrained optimization problems. Numerical tests show that even nearly singular problems can be handled successfully.

    Some of My Other Pages

    Global Optimization
    Interval Methods
    Mathematical Software
    Computational Mathematics Links
    Mathematics Links
    Statistics Links
    Artificial Intelligence
    A Theoretical Physics FAQ

    my home page (

    Arnold Neumaier (