This page is part of the FMathL - Formal mathematical language web site at http://www.mat.univie.ac.at/~neum/FMathL.html

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:

**
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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

Global Optimization

Interval Methods

Mathematical Software

Computational Mathematics Links

Mathematics Links

Statistics Links

Artificial Intelligence

A Theoretical Physics FAQ

my home page (http://www.mat.univie.ac.at/~neum/)

Arnold Neumaier (Arnold.Neumaier@univie.ac.at)