Mathematical Software
An open partition \pi{} [Cod09a, Cod09b] of a tree T is a partition of the vertices of T with the property that, for each block B of \pi, the upset of B is a union of blocks of \pi. This paper deals with the number, NP(n), of open…
In this work we solve a special case of the problem of building an n-dimensional parallelepiped using a given set of n-dimensional parallelepipeds. Consider the identity x^3 = x(x-1)(x-2)+3x(x-1+x). For sufficiently large x, we associate…
With this work we aim to show how Mathematica can be a useful tool to investigate properties of combinatorial structures. Specifically, we will face enumeration problems on independent subsets of powers of paths and cycles, trying to…
The IEEE 754-2008 standard recommends the correct rounding of some elementary functions. This requires to solve the Table Maker's Dilemma which implies a huge amount of CPU computation time. We consider in this paper accelerating such…
The Agora system is a prototype "Wiki for Formal Mathematics", with an aim to support developing and documenting large formalizations of mathematics in a proof assistant. The functions implemented in Agora include in-browser editing, strong…
ZKCM is a C++ library developed for the purpose of multiprecision matrix computation, on the basis of the GNU MP and MPFR libraries. It provides an easy-to-use syntax and convenient functions for matrix manipulations including those often…
To find the discrete symmetries of a Hamilton operator $\hat H$ is of central importance in quantum theory. Here we describe and implement a brute force method to determine the discrete symmetries given by permutation matrices for Hamilton…
Generalized linear mixed-effects models in the context of genome-wide association studies (GWAS) represent a formidable computational challenge: the solution of millions of correlated generalized least-squares problems, and the processing…
We report on highlights of the ACL2 enhancements introduced in ACL2 releases since the 2011 ACL2 Workshop. Although many enhancements are critical for soundness or robustness, we focus in this paper on those improvements that could benefit…
In many scientific and engineering applications, one has to solve not one but a sequence of instances of the same problem. Often times, the problems in the sequence are linked in a way that allows intermediate results to be reused. A…
We describe an interface and an implementation for performing Kronecker product actions on NVIDIA GPUs for multiple small 2-D matrices and 3-D arrays processed in parallel as a batch. This method is suited to cases where the Kronecker…
We present an interface and an implementation of the General Matrix Multiply (GEMM) routine for multiple small matrices processed simultaneously on NVIDIA graphics processing units (GPUs). We focus on matrix sizes under 16. The…
We present the Unified Form Language (UFL), which is a domain-specific language for representing weak formulations of partial differential equations with a view to numerical approximation. Features of UFL include support for variational…
Waves are all around us--be it in the form of sound, electromagnetic radiation, water waves, or earthquakes. Their study is an important basic tool across engineering and science disciplines. Every wave solver serving the computational…
This article introduces yet another representation of rotations in 3-space. The rotations form a 3-dimensional projective space, which fact has not been exploited in Computer Science. We use the four affine patches of this projective space…
Modern platforms used for high-performance computing (HPC) include machines with both general-purpose CPUs, and "accelerators", often in the form of graphical processing units (GPUs). StarPU is a C library to exploit such platforms. It…
Modelling, parameter identification, and simulation play an important role in systems biology. Usually, the goal is to determine parameter values that minimise the difference between experimental measurement values and model predictions in…
Graph rewrite systems are powerful tools to model and study complex problems in various fields of research. Their successful application to chemical reaction modelling on a molecular level was shown but no appropriate and simple system is…
This paper proposes a type of pseudorandom number generator, Mersenne Twister for Graphic Processor (MTGP), for efficient generation on graphic processessing units (GPUs). MTGP supports large state sizes such as 11213 bits, and uses the…
We present a set of tools for rewriting modulo associativity and commutativity (AC) in Coq, solving a long-standing practical problem. We use two building blocks: first, an extensible reflexive decision procedure for equality modulo AC;…