Digitisation, representation, and formalisation - Digital libraries of mathematics

One of the main tasks of the mathematical knowledge management community must surely be to enhance access to mathematics on digital systems. In this paper we present a spectrum of approaches to solving the various problems inherent in this task, arguing that a variety of approaches is both necessary and useful. The main ideas presented are about the differences between digitised mathematics, digitally represented mathematics and formalised mathematics. Each has its part to play in managing mathematical information in a connected world. Digitised material is that which is embodied in a computer file, accessible and displayable locally or globally. Represented material is digital material in which there is some structure (usually syntactic in nature) which maps to the mathematics contained in the digitised information. Formalised material is that in which both the syntax and semantics of the represented material, is automatically accessible. Given the range of mathematical information to which access is desired, and the limited resources available for managing that information, we must ensure that these resources are applied to digitise, form representations of or formalise, existing and new mathematical information in such a way as to extract the most benefit from the least expenditure of resources. We also analyse some of the various social and legal issues which surround the practical tasks.

Explicit mathematics and operational set theory: some ontological comparisons

We discuss several ontological properties of explicit mathematics and operational set theory: global choice, decidable classes, totality and extensionality of operations, function spaces, class and set formation via formulas that contain the definedness predicate and applications.

A new model construction by making a detour via intuitionistic theories II: Interpretability lower bound of Feferman's explicit mathematics T0

We partially solve a long-standing problem in the proof theory of explicit mathematics or the proof theory in general. Namely, we give a lower bound of Feferman’s system T0 of explicit mathematics (but only when formulated on classical logic) with a concrete interpretat ion of the subsystem Σ12-AC+ (BI) of second order arithmetic inside T0. Whereas a lower bound proof in the sense of proof-theoretic reducibility or of ordinalanalysis was already given in 80s, the lower bound in the sense of interpretability we give here is new. We apply the new interpretation method developed by the author and Zumbrunnen (2015), which can be seen as the third kind of model construction method for classical theories, after Cohen’s forcing and Krivine’s classical realizability. It gives us an interpretation between classical theories, by composing interpretations between intuitionistic theories.

Sufficiency of Favard's condition for a class of band-dominated operators on the axis

The purpose of this paper is to show that, for a large class of band-dominated operators on $\ell^\infty(Z,U)$, with $U$ being a complex Banach space, the injectivity of all limit operators of $A$ already implies their invertibility and the uniform boundedness of their inverses. The latter property is known to be equivalent to the invertibility at infinity of $A$, which, on the other hand, is often equivalent to the Fredholmness of $A$. As a consequence, for operators $A$ in the Wiener algebra, we can characterize the essential spectrum of $A$ on $\ell^p(Z,U)$, regardless of $p\in[1,\infty]$, as the union of point spectra of its limit operators considered as acting on $\ell^p(Z,U)$.

An integral equation method for a boundary value problem arising in unsteady water wave problems

In this paper we consider the 2D Dirichlet boundary value problem for Laplace’s equation in a non-locally perturbed half-plane, with data in the space of bounded and continuous functions. We show uniqueness of solution, using standard Phragmen-Lindelof arguments. The main result is to propose a boundary integral equation formulation, to prove equivalence with the boundary value problem, and to show that the integral equation is well posed by applying a recent partial generalisation of the Fredholm alternative in Arens et al [J. Int. Equ. Appl. 15 (2003) pp. 1-35]. This then leads to an existence proof for the boundary value problem. Keywords. Boundary integral equation method, Water waves, Laplace’s

A cell by cell anisotropic adaptive mesh ALE method

A cell by cell anisotropic adaptive mesh Arbitrary Lagrangian Eulerian (ALE) method for the solution of the Euler equations is described. An efficient approach to equipotential mesh relaxation on anisotropically refined meshes is developed. Results for two test problems are presented.

A combined BIE-FE method for the Stokes equations

A numerical algorithm for the biharmonic equation in domains with piecewise smooth boundaries is presented. It is intended for problems describing the Stokes flow in the situations where one has corners or cusps formed by parts of the domain boundary and, due to the nature of the boundary conditions on these parts of the boundary, these regions have a global effect on the shape of the whole domain and hence have to be resolved with sufficient accuracy. The algorithm combines the boundary integral equation method for the main part of the flow domain and the finite-element method which is used to resolve the corner/cusp regions. Two parts of the solution are matched along a numerical ‘internal interface’ or, as a variant, two interfaces, and they are determined simultaneously by inverting a combined matrix in the course of iterations. The algorithm is illustrated by considering the flow configuration of ‘curtain coating’, a flow where a sheet of liquid impinges onto a moving solid substrate, which is particularly sensitive to what happens in the corner region formed, physically, by the free surface and the solid boundary. The ‘moving contact line problem’ is addressed in the framework of an earlier developed interface formation model which treats the dynamic contact angle as part of the solution, as opposed to it being a prescribed function of the contact line speed, as in the so-called ‘slip models’. Keywords: Dynamic contact angle; finite elements; free surface flows; hybrid numerical technique; Stokes equations.

Consistent Dirichlet Boundary Conditions for Numerical Solution of Moving Boundary Problems

We consider the imposition of Dirichlet boundary conditions in the finite element modelling of moving boundary problems in one and two dimensions for which the total mass is prescribed. A modification of the standard linear finite element test space allows the boundary conditions to be imposed strongly whilst simultaneously conserving a discrete mass. The validity of the technique is assessed for a specific moving mesh finite element method, although the approach is more general. Numerical comparisons are carried out for mass-conserving solutions of the porous medium equation with Dirichlet boundary conditions and for a moving boundary problem with a source term and time-varying mass.