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 modeling system for mathematics,
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
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
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.
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
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
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
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.
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.
Mathematical Model Building,
Chapter 3 in: Modeling Languages in Mathematical Optimization
(J. Kallrath, ed.),
Kluwer, Boston 2004.
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)
NOP-2 permits named variables, parameters, indexing, loops, relational
operators, extensive set operations, matrices and tensors, and
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.
Improving interval enclosures,
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.
Towards optimization-based error bounds for uncertain PDEs,
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
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,
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
Computational Mathematics Links
A Theoretical Physics FAQ
home page (http://www.mat.univie.ac.at/~neum/)
Arnold Neumaier (Arnold.Neumaier@univie.ac.at)