Mathematical Software – ICMS 2016

Science priorities lead to scientific models, and models are implemented in the form of algorithms.

UniMath, short for “Univalent Mathematics”, refers to both a language (a.k.a. a formal system) for mathematics, as well as to a computer-checked library of mathematics formalized in that system. The UniMath library, under active development, aims to coherently integrate machine-checked proofs of mathematical results from many different branches of mathematics.The UniMath language is a dependent type theory, augmented by the univalence axiom. One goal is to keep the language as small as possible, to ease verification of the theory. In particular, general inductive types are not part of the language.In this work, we partially remedy this lack by constructing some inductive (families of) sets. This involves a formalization of a standard category-theoretic result on the construction of initial algebras, as well as a mechanism to conveniently use the inductive sets thus obtained.The present work constitutes one part of a construction of a framework for specifying, via a signature, programming languages with binders as nested datatypes. To this end, we are going to combine our work with previous work by Ahrens and Matthes (itself based on work by Matthes and Uustalu) on an axiomatisation of substitution for languages with variable binding. The languages specified via the framework will automatically be equipped with the structure of a monad, where the monadic operations and axioms correspond to a well-behaved substitution operation.

Nuprl is an interactive theorem prover that implements an extensional constructive type theory, where types are interpreted as partial equivalence relations on closed terms. Nuprl is both computationally and type-theoretically open-ended in the sense that both its computation system and its type theory can be extended as needed by checking a handful of conditions. For example, Doug Howe characterized the computations that can be added to Nuprl in order to preserve the congruence of its computational equivalence relation. We have implemented Nuprl’s computation and type systems in Coq, and we have showed among other things that it is consistent. Using our Coq framework we can now easily and rigorously add new computations and types to Nuprl by mechanically verifying that all the necessary conditions still hold. We have recently exercised Nuprl’s open-endedness by adding nominal features to Nuprl in order to prove a version of Brouwer’s continuity principle, as well as choice sequences in order to prove truncated versions of the axiom of choice and of Brouwer’s bar induction principle. This paper illustrate the process of extending Nuprl with versions of the axiom of choice.

Lean is a new open source dependently typed theorem prover which is mainly being developed by Leonardo de Moura at Microsoft Research. It is suited to be used for proof irrelevant reasoning as well as for proof relevant formalizations of mathematics. In my talk, I will present my experiences doing a formalization project in Lean. One of the interesting aspects of homotopy type theory is the ability to perform synthetic homotopy theory on higher types. While for the first homotopy group the choice of a suitable algebraic structure to capture the homotopic information is obvious – it’s a group –, implementing a structure to capture the information about both the first and the second homotopy group (or groupoid) of a type and their interactions is more involved. Following Ronald Brown’s book on Nonabelian Algebraic Topology, I formalized two structures: Double groupoids with thin structures and crossed modules on groupoids. I furthermore attempted to prove their equivalence. The project can be seen as a usability and performance test for the new theorem prover.

Considerable attention and efforts have been given to the implementation of automatic reasoning tools in interactive geometric environments. Nevertheless, the main goal in such works focused on theorem proving, cf. Java Geometry Expert or GeoGebra. A related issue, automatic discovery, remains almost unexplored in the field of dynamic geometry software.This extended abstract sketches our initial results towards the incorporation into GeoGebra, a worldwide spread software with tenths of millions of users, of automatic discovery abilities. As a first result, currently available in the official version, we report on a new command allowing the automatic discovery of loci of points in diagrams. Besides the standard mover-tracer locus finding, the approach also deals with loci constrained by implicit conditions. Hence, our proposal successfully automates a kind of bound dragging in dynamic geometry, the ‘dummy locus dragging’. In this way, the cycle of conjecturing-checking-proving will be accessible for general learners in elementary geometry.

We present an interactive and automated theorem prover for free higher-order logic. Our implementation on top of the Isabelle/HOL framework utilizes a semantic embedding of free logic in classical higher-order logic. The capabilities of our tool are demonstrated with first experiments in category theory.

We apply SAT and #-SAT to problems of computational topology: knot detection and recognition. Quandle coloring can be viewed as associations of elements of algebraic structures, called quandles, to arcs of knot diagrams such that certain algebraic relations hold at each crossing. The existence of a coloring (called colorability) and the number of colorings of a knot by a quandle are knot invariants that can be used to distinguish knots. We realise coloring instances as SAT and #-SAT instances, and produce experimental data demonstrating that a SAT-based approach to colorability is a practically efficient method for knot detection and #-SAT can be utilised for knot recognition.

In this talk we will report on three useful tools recently implemented in the frame of the Theorema project: a graphical user interface for interactive proof development, a higher-order rewriting mechanism, and a tool for automatically analyzing the logical structure of Theorema-theories. Each of these three tools already proved extremely useful in the extensive formal exploration of a non-trivial mathematical theory, namely the theory of Gröbner bases and reduction rings, in Theorema 2.0.

Pover9/Mace4 or its predecessor Otter is one of the powerful automated theorem provers for first-order and equational logic. In this paper we explore various possibilities of using Prover9 in ring theory and semiring theory, in particular, associative rings, rings with involutions, semirings with cancellation laws and near-rings. We code the corresponding axioms in Prover9, check some well-known theorems, for example, Jacobson’s commutativity theorem, give some new proofs, and also present some new results.

In the Leo-III project, a new agent-based deduction system for classical higher-order logic is developed. Leo-III combines its predecessor’s concept of cooperating external specialist systems with a novel agent-based proof procedure. Key goals of the system’s development involve parallelism on various levels of the proof search, adaptability for different external specialists, and native support for reasoning in expressive non-classical logics.

“Todai Robot Project” is a project of artificial intelligence launched by National Institute of Informatics for re-unifying the artificial intelligence field subdivided in 1980s and afterwards. We focus towards attaining a high score in National Center Test for University Admissions, and use Quantifier Elimination (QE) over the real closed fields as a main tool for solving problems in mathematics. However, it is not applicable for several kinds of problems such as one with sequence. In this article, we propose an algorithm for solving problems of sequence at the National Center Test for University Admissions.

Computations over the rational numbers often suffer from intermediate coefficient swell. One solution to this problem is to apply the given algorithm modulo a number of primes and then lift the modular results to the rationals. This method is guaranteed to work if we use a sufficiently large set of good primes. In many applications, however, there is no efficient way of excluding bad primes. In this note, we describe a technique for rational reconstruction which will nevertheless return the correct result, provided the number of good primes in the selected set of primes is large enough. We give a number of illustrating examples which are implemented using the computer algebra system Singular and the programming language Julia. We discuss applications of our technique in computational algebraic geometry.

Normaliz is an open-source software for the computation of lattice points in rational polyhedra, or, in a different language, the solutions of linear diophantine systems. The two main computational goals are (i) finding a system of generators of the set of lattice points and (ii) counting elements degree-wise in a generating function, the Hilbert Series. In the homogeneous case, in which the polyhedron is a cone, the set of generators is the Hilbert basis of the intersection of the cone and the lattice, an affine monoid.We will present some improvements to the Normaliz algorithm by subdividing simplicial cones with huge volumes. In the first approach the subdivision points are found by integer programming techniques. For this purpose we interface to the integer programming solver SCIP to our software. In the second approach we try to find good subdivision points in an approximating overcone that is faster to compute.

Singular is a comprehensive and steadily growing computer algebra system, with particular emphasis on applications in algebraic geometry, commutative algebra, and singularity theory. Singular can easily be extended by other tools provided as C or C++ library: gfan and polymake will be discussed as an example.

3D printing and other layer manufacturing processes are challenged by dimensional accuracy. Various techniques are used to validate and calibrate dimensional accuracy through the complete building envelope. The validation process involves the growing and measuring of a shape with known parameters. The measured result is compared with the intended digital model. Processes with the risk of deformation after time or post-processing may find this technique beneficial. We propose to use objects from algebraic geometry as test shapes. A cubic surface is given as the zero set of a degree 3 polynomial in 3 variables. A class of cubics in real 3D space contains exactly 27 real lines. These lines can be used for dimensional calibration. Due to the thin shape geometry the material required to produce an algebraic surface is minimal. We provide a library for the computer algebra system Singular which, from 6 given points in the plane, constructs a cubic and the lines on it.

A core computation in numerical algebraic geometry is the decomposition of the solution set of a system of polynomial equations into irreducible components, called the numerical irreducible decomposition. One approach to validate a decomposition is what has come to be known as the “trace test.” This test, described by Sommese, Verschelde, and Wampler in 2002, relies upon path tracking and hence could be called the “tracking trace test.” We present a new approach which replaces path tracking with local computations involving derivatives, called a “local trace test.” We conclude by demonstrating this local approach with examples from kinematics and tensor decomposition.

We study a method of calibration of accelerometers usable on field. No tools are required except a computer. Since the method is purely mathematical, free from measurement tools errors, it is both precise and affordable. We prove that the calibration of an accelerometer with three axis is possible with 9 random measurements exactly when the sphere is the unique quadric containing the nine directions of measurements.

Designing experiments for generalized linear models is difficult because optimal designs depend on unknown parameters. The local optimality approach is to study the regions in parameter space where a given design is optimal. In many situations these regions are semi-algebraic. We investigate regions of optimality using computer tools such as yalmip, qepcad, and Mathematica.

Associated to every coherent system there is a canonical ideal whose Hilbert series encodes the reliability of the system. We study various ideals arising in the theory of system reliability. Using ideas from the theory of orientations, and matroids on graphs we associate a polyhedral complex to our system so that the non-cancelling terms in the reliability formula can be read from the labeled faces of this complex. Algebraically, this polyhedron resolves the minimal free resolution of these ideals. In each case, we give an explicit combinatorial description of non-cancelling terms in terms of acyclic orientations of graph and the number of regions in the graphic hyperplane arrangement. This resolves open questions posed by Giglio-Wynn and develops new connections between the theory of oriented matroid, the theory of divisors on graphs, and the theory of system reliability.

Polynomial Systems, or at least their algorithms, have the reputation of being doubly-exponential in the number of variables (see the classic papers of Mayr & Mayer from 1982 and Davenport & Heintz from 1988). Nevertheless, the Bezout bound tells us that number of zeros of a zero-dimensional system is singly-exponential in the number of variables. How should this contradiction be reconciled?We first note that Mayr and Ritscher in 2013 showed the doubly exponential nature of Gröbner bases is with respect to the dimension of the ideal, not the number of variables. This inspires us to consider what can be done for Cylindrical Algebraic Decomposition which produces a doubly-exponential number of polynomials of doubly-exponential degree.We review work from ISSAC 2015 which showed the number of polynomials could be restricted to doubly-exponential in the (complex) dimension using McCallum’s theory of reduced projection in the presence of equational constraints. We then discuss preliminary results showing the same for the degree of those polynomials. The results are under primitivity assumptions whose importance we illustrate.

A CGS real QE method is a real quantifier elimination (QE) method which is composed of the computation of comprehensive Gröbner systems (CGSs) based on the theory of real root counting. Its fundamental algorithm was first introduced by Weispfenning in 1998. We further improved the algorithm in 2015 so that we can make a satisfactorily practical implementation. For its efficient implementation, there are several key issues we have to take into account. In this extended abstract we introduce them together with some important techniques for making an efficient CGS real QE implementation.

We present generic, type safe (non-unique) common divisors of solvable polynomials software. The solvable polynomial rings are defined with non-commuting variables, moreover, in case of parametric (solvable) coefficients the main variables may not commute with the coefficients. The interface, class organization is described in the object-oriented programming environment of the Java Algebra System (JAS). The implemented algorithms can be applied, for example, in solvable extension field and root construction. We show the design and feasibility of the implementation in the mentioned applications.

A Web-based knowledge database and computing platform for nonlinear differential equations is presented, which could provide computing and graphing based on symbolic computing system Maple and some of its built-in packages. Users can not only calculate specific types of analytical solutions of nonlinear differential systems by calling the packages, but also carry out any symbolic computations associated with equations and other kinds of simple computations in an interactive mode with visual output. The knowledge database of differential equations has all functions of the general database. Furthermore, each equation has a web page to show its properties and research results. In addition, each mathematica formula is stored in its infix form in the knowledge database and can be displayed visually.

The classical problem of studying the topology of a plane algebraic curve is typically handled by the computation of braid monodromies. The existence of arithmetic Zariski pairs implies that purely algebraic methods cannot provide those braids, so we need numerical methods at some point. However, numerical methods usually have the problem that floating point arithmetic introduces rounding errors that must be controlled to ensure certified results. We present SIROCCO (The source code and documentation is available in: https://github.com/miguelmarco/sirocco), a library for certified polynomial root continuation, specially suited for this task. It computes piecewise linear approximations of the paths followed by the roots. The library ensures that there exist disjoint tubular neighborhoods that contain both the actual path and the computed approximation. This fact proves that the braids corresponding to the approximation are equal to the ones corresponding to the actual curve. The validation is based on interval floating point arithmetic, the Interval Newton Criterion and auxiliary lemmas. We also provide a SageMath interface and auxiliary routines that perform all the needed pre and post-processing tasks. Together this is an “out of the box” solution to compute, for instance, the fundamental group of the complement of an affine complex curve.

Mixed volumes of lattice polytopes play a central role in numerical and tropical algebraic geometry. We present an implementation of a new algorithm for their computation based on tropical homotopy continuation, which is a combinatorial procedure using ideas from numerical algebraic geometry. While the mathematical aspects of the algorithm are presented elsewhere, here we mainly address technical details of the implementation, in particular how it was made fast and reliable. The implementation is distributed as part of the library gfanlib.

Singular is a comprehensive and steadily growing computer algebra system, with particular emphasis on applications in algebraic geometry, commutative algebra, and singularity theory.Singular provides highly efficient core algorithms, a multitude of advanced algorithms in the above fields, an intuitive, C-like programming language, easy ways to make it user-extendable through libraries, and a comprehensive online manual and help function.Singular’s core algorithms handle Gröbner resp. standard bases and free resolutions, polynomial factorization, resultants, characteristic sets, and numerical root finding. Symbolic-numeric solving in Singular starts with a decomposition to a triangular system or the primary decomposition of (the radical of) an ideal. New developments for primary decomposition will be presented in this paper: identifying sub problems allows an early split of the radical. A primary decomposition of these sub problems can be lifted to (not necessary primary) decomposition of the original problem: the subsequent primary decomposition will be faster.After the symbolic preprocessing numerical solving of these smaller and easier to solve systems can be achieved by Singular’s implementation of Laguerre’s algorithm or by integrating other systems.

We describe the software package borderbasix dedicated to the computation of border bases and the solutions of polynomial equations. We present the main ingredients of the border basis algorithm and the other methods implemented in this package: numerical solutions from multiplication matrices, real radical computation, polynomial optimization. The implementation parameterized by the coefficient type and the choice function provides a versatile family of tools for polynomial computation with modular arithmetic, floating point arithmetic or rational arithmetic. It relies on linear algebra solvers for dense and sparse matrices for these various types of coefficients. A connection with SDP solvers has been integrated for the combination of relaxation approaches with border basis computation. Extensive benchmarks on typical polynomial systems are reported, which show the very good performance of the tool.

We propose a new fixed precision arithmetic package called RecInt. It uses a recursive double-size data-structure. Contrary to arbitrary precision packages like GMP, that create vectors of words on the heap, RecInt large integers are created on the stack. The space allocated for these integers is a power of two and arithmetic is performed modulo that power. Operations are thus easily implemented recursively by a divide and conquer strategy. Among those, we show that this packages is particularly well adapted to Newton-Raphson like iterations or Montgomery reduction. Recursivity is implemented via doubling algorithms on templated data-types. The idea is to extend machine word functionality to any power of two and to use template partial specialization to adapt the implemented routines to some specific sizes and thresholds. The main target precision is for cryptographic sizes, that is up to several tens of machine words. Preliminary experiments show that good performance can be attained when comparing to the state of art GMP library: it can be several order of magnitude faster when used with very few machine words. This package is now integrated within the Givaro C++ library and has been used for efficient exact linear algebra computations.

Many scientific computing applications demand massive numerical computations on parallel architectures such as Graphics Processing Units (GPUs). Usually, either floating-point single or double precision arithmetic is used. Higher precision is generally not available in hardware, and software extended precision libraries are much slower and rarely supported on GPUs. We develop CAMPARY: a multiple-precision arithmetic library, using the CUDA programming language for the NVidia GPU platform. In our approach, the precision is extended by representing real numbers as the unevaluated sum of several standard machine precision floating-point numbers. We make use of error-free transforms algorithms, which are based only on native precision operations, but keep track of all rounding errors that occur when performing a sequence of additions and multiplications. This offers the simplicity of using hardware highly optimized floating-point operations, while also allowing for rigorously proven rounding error bounds. This also allows for easy implementation of an interval arithmetic. Currently, all basic multiple-precision arithmetic operations are supported. Our target applications are in chaotic dynamical systems or automatic control.

We present an efficient algorithm for the confluent hypergeometric functions when the imaginary part of b and z is large. The algorithm is based on the steepest descent method, applied to a suitable representation of the confluent hypergeometric functions as a highly oscillatory integral, which is then integrated by using various quadrature methods. The performance of the algorithm is compared with open-source and commercial software solutions with arbitrary precision, and for many cases the algorithm achieves high accuracy in both the real and imaginary parts. Our motivation comes from the need for accurate computation of the characteristic function of the Arcsine distribution or the Beta distribution; the latter being required in several financial applications, for example, modeling the loss given default in the context of portfolio credit risk.

Many optimization problems arising in practice can be modeled as mixed integer programs (MIPs). In this paper, we present the new parallelization concept for the state-of-the-art MIP solver FICO Xpress-Optimizer. A natural precondition to achieving reasonabling speedups from parallelization is maintaining a high workload of the available computational resources. At the same time, reproducibility and reliability are key requirements for mathematical optimization software; solvers like the FICO Xpress-Optimizer are expected to be deterministic. The resulting synchronization latencies render the goal of a satisfying workload a challenge in itself.We address this challenge by following a partial information approach and separating the concepts of simultaneous tasks and independent threads from each other. Our computational results indicate that this leads to a much higher CPU workload and thereby to an improved scaling on modern high-performance CPUs. As an added value, the solution path that the FICO Xpress-Optimizer takes is not only deterministic in a fixed environment, but, to a certain extent, thread-independent.

PolySCIP [1] is a new solver for multi-criteria integer and multi-criteria linear programs handling an arbitrary number of objectives. It is available as an official part of the non-commercial constraint integer programming framework SCIP. It utilizes a lifted weight space approach to compute the set of supported extreme non-dominated points and unbounded non-dominated rays, respectively. The algorithmic approach can be summarized as follows: At the beginning an arbitrary non-dominated point is computed (or it is determined that there is none) and a weight space polyhedron created. In every next iteration a vertex of the weight space polyhedron is selected whose entries give rise to a single-objective optimization problem via a combination of the original objectives. If the optimization of this single-objective problem yields a new non-dominated point, the weight space polyhedron is updated. Otherwise another vertex of the weight space polyhedron is investigated. The algorithm finishes when all vertices of the weight space polyhedron have been investigated. The file format of PolySCIP is based on the widely used MPS format and allows a simple generation of multi-criteria models via an algebraic modelling language.

In this talk, we present our ongoing research project. The objective of this project is to develop advanced computing and optimization infrastructures for extremely large-scale graphs on post peta-scale supercomputers. We explain our challenge to Graph 500 and Green Graph 500 benchmarks that are designed to measure the performance of a computer system for applications that require irregular memory and network access patterns. The 1st Graph500 list was released in November 2010. The Graph500 benchmark measures the performance of any supercomputer performing a BFS (Breadth-First Search) in terms of traversed edges per second (TEPS). In 2014 and 2015, our project team was a winner of the 8th, 10th, and 11th Graph500 and the 3rd to 6th Green Graph500 benchmarks, respectively. We also present our parallel implementation for large-scale SDP (SemiDefinite Programming) problem. The semidefinite programming (SDP) problem is a predominant problem in mathematical optimization. The primal-dual interior-point method (PDIPM) is one of the most powerful algorithms for solving SDP problems, and many research groups have employed it for developing software packages. We solved the largest SDP problem (which has over 2.33 million constraints), thereby creating a new world record. Our implementation also achieved 1.774 PFlops in double precision for large-scale Cholesky factorization using 2,720 CPUs and 4,080 GPUs on the TSUBAME 2.5 supercomputer.

We describe the main design features of DSJM (Determine Sparse Jacobian Matrices), a software toolkit written in standard C++ that enables direct determination of sparse Jacobian matrices. Our design exploits the recently proposed unifying framework “pattern graph” and employs cache-friendly array-based sparse data structures. The DSJM implements a greedy grouping (coloring) algorithm and several ordering heuristics. In our numerical testing on a suite of large-scale test instances DSJM consistently produced better timing and partitions compared with a similar software.

We present software for investigations with cut-generating functions in the Gomory–Johnson model and extensions, implemented in the computer algebra system SageMath.

Akaike’s information criterion (AIC) is a measure of the quality of a statistical model for a given set of data. We can determine the best statistical model for a particular data set by the minimization based on the AIC. Since it is difficult to find the best statistical model from a set of candidates by this minimization in practice, stepwise methods, which are local search algorithms, are commonly used to find a better statistical model though it may not be the best.We formulate this AIC minimization as a mixed integer nonlinear programming problem and propose a method to find the best statistical model. In particular, we propose ways to find lower and upper bounds and a branching rule for this minimization. We then combine them with SCIP, which is a mathematical optimization software and a branch-and-bound framework. We show that the proposed method can provide the best statistical model based on AIC for small-sized or medium-sized benchmark data sets in UCI Machine Learning Repository. Furthermore, we show that this method can find good quality solutions for large-sized benchmark data sets.

SCIP is a solver for a wide variety of mathematical optimization problems. It is written in C and extendable due to its plug-in based design. However, dealing with all C specifics when extending SCIP can be detrimental to development and testing of new ideas. This paper attempts to provide a remedy by introducing PySCIPOpt, a Python interface to SCIP that enables users to write new SCIP code entirely in Python. We demonstrate how to intuitively model mixed-integer linear and quadratic optimization problems and moreover provide examples on how new Python plug-ins can be added to SCIP.

The Ubiquity Generator (UG) is a general framework for the external parallelization of mixed integer programming (MIP) solvers. It has been used to develop ParaSCIP, a distributed memory, massively parallel version of the open source solver SCIP, running on up to 80,000 cores. In this paper, we present a first implementation of ParaXpress, a distributed memory parallelization of the powerful commercial MIP solver FICOXpress. Besides sheer performance, an important difference between SCIP and Xpress is that Xpress provides an internal parallelization for shared memory systems. When aiming for a best possible performance of ParaXpress on a supercomputer, the question arises how to balance the internal Xpress parallelization and the external parallelization by UG against each other. We provide computational experiments to address this question and we show preliminary computational results for running a first version of ParaXpress on 6,144 cores in parallel.

The CindyJS Project brings interactive mathematical visualization to a broad variety of devices. Using projective geometry, homotopy methods and well tuned algorithms the CindyJS project is one of the first real time capable software projects in this field that at the same time approaches high-level mathematical descriptions and performance.

CindyJS is a framework for creating interactive (mathematical) content for the web. It can be extended using plugins, two of which are presented here.Cindy3D enables displaying 3D content via WebGL.The KaTeX plugin typesets formulas within CindyJS.We also discuss the general structure of plugins in CindyJS.

KeTpic is a macro package which generates the graphical code that can be used in LaTeX. In 2014, commands for generating data in obj format were added to KeTpic. The data can also be converted to stl format, with which 3D printers can make 3D models. KeTCindy is a Cinderella plug-in that generates data for a variety of teaching materials along with 3D models without much additional effort. In this paper, we show a variety of KeTCindy commands for doing that, and present the actual teaching materials that result.

Today, various tools have been developed to visualize mathematical objects dynamically. For example, graphical user interfaces have been implemented on many computer algebra systems like Mathematica in which a dynamic presentation of geometric shapes and function graphs can be generated by using sliders. Among such tools, dynamic geometry software like Cinderella are quite excellent in that they allow us to control those objects more interactively. At the same time, static presentation of those objects on printed matters is also indispensable for mathematical activities since it is through paper and pencil-based activities that we can most easily synchronize computation and observation. Thus, especially for educational purposes, the selection and the usage of these methods at each stage of the learning process is crucial. Since , which we have recently developed, serves a direct linkage between interactive presentation of graphics on Cinderella and its exported image into , it can be expected that using enables mathematics learners to unify their intuitive reasoning through observation of the interactive presentation on PC and their discursive inference with the use of documents including finely tuned graphics. In this paper, the effect of such unifiability on the learners’ reasoning processes is illustrated through time-series detection of learners’ activities during some case study in which system is used.

In Japan, some wooden plaques presenting geometrical puzzles (SANGAKU) show problems of drawing smaller circles within a larger circle in contact with it or a circle in contact with a quadratic curve, such as an oval. Problems of these kinds can be interesting teaching materials. Dynamic geometry software such Cinderella or GeoGebra is useful to solve these problems. One can use high-quality TeX graphics with KeTCindy (Cinderella plug-in) to draw these figures. One can also draw figures by solving simultaneous equations using a computer algebra system such as Maxima or Risa/Asir. Although simultaneous equations can be solved in Maxima, the solution takes time. Alternatively, it does not work when too many variables are included. In such cases, one can convert it to a system of equations that are easier to solve using a Grobner base in Risa/Asir. Then a user can solve them by giving the result to Maxima. A user can accomplish this on Cinderella through KeTCindy, and can draw circles using the result. This method can also be applied to other difficult circumstances. This paper presents some examples.

CindyJS is a framework for creating interactive (mathematical) content for the web. The plugin CindyGL extends this framework and leverages WebGL for parallelized computations.CindyGL provides access to the GPU fragment shader for CindyJS. Among other tasks, the plugin CindyGL is used for real-time colorplots.We introduce the main principles, concepts and application of CindyGL and describe the encountered technical challenges. Special focus is put on a novel visualization scheme that uses feedback loops, which were among the motivating forces of developing CindyGL. They can be used for a wide range of applications. Some of them are numerical simulations, cellular automatons and fractal generation, which are described here.

The conceptual aspects of the majority of physical phenomena readily are comprehensible, yet their analysis conducive to justifiable output require mathematical justifications. Applied mathematics is the backbone of theoretical physics. No field in physics in particular and science in general is immune. Within the last couple of decades advances in computer science introduced a fresh pathway, computational physics, augmenting the field. The offspring of these innovations is the scientific software capable of performing operations that could not be accomplished traditionally. The impact of these spectacular innovative technologies is evidence in scientific literature. The focus of this article is to demonstrate the graphical usefulness of one such scientific software, Mathematica analyzing the electrostatic features of discrete charge distributions. This is an example of a theoretical physics problem focusing on the overlap of physics, graphics and math. Ever since its birth a quarter century ago, Mathematica steadily has been growing in popularity and practicality. This article embodies the codes compatible with the latest version of the software including one, two and three dimensional sliders. Practitioner physicists, interested individuals and mathematicians may adjust the code to meet their needs.

We introduce KeTCindy, which is the right combination of Cinderella and KeTpic we developed to produce high-quality LaTeX graphics using free mathematical software such as Scilab and R. In KeTCindy, Cinderella works as a GUI of KeTpic, so the interactive operation on PC display can be reflected directly on the generated image on LaTeX final output. The generated image can be finely tuned using KeTCindy commands embedded into CindyScript, the scripting language of Cinderella. KeTCindy can be regarded as a prominent scheme to establish an effective linkage between visualization tools and editing tools. Moreover, KeTCindy enables the importation of data calculated or simulated using other mathematical software such as Maxima, Fricas, Risa/Asir and R, and to combine them with the graphical data, so that an extremely wide range of mathematical objects can be presented. We will show some eminent capabilities of KetCindy and also its usage.

When we use TeX to edit a document, it is sometimes necessary to place the figure of a preferred shape into a suitable position. In this presentation, we propose a method using KeTCindy for this purpose. KeTCindy is a plug-in to Cinderella that converts the procedure to generate geometric shapes into TeX readable code to generate the corresponding image on TeX final output. One merit of using KeTCindy is its interactive character. On the Cinderella screen, a user can control the shape of the figure as desired. When we place the resulting image at the exterior side of text part, simple conversion to TeX graphical image through KeTCindy is sufficient. However, when it is necessary to place it onto the text part, some extra elaboration is necessary to ensure that both the text part and the generated figure are finely balanced. The key idea is making the screen of Cinderella semi-transparent using software named feewhee.

To produce class materials with figures using TeX, the KeTpic Development Group (KDG), comprising S. Takato, the author and several Japanese mathematics education researchers, completed KeTpic in 2011 as a plug-in for the Scilab numerical analysis software package. We describe KeTpic programs with the command line user interface Scinotes. KeTpic users produce KeTpic programs based on their original programming styles. This leads other KeTpic users to a shortcoming that renders it difficult to use their KeTpic programs. To resolve this situation, KDG has developed the KeTpic programming style for drawings in 2013. KeTpic programs include three parts: a preamble part that describes setting commands, a part for making plot data and a part for extracting plot data into a figure TeX file. Since 2014, KDG has improved KeTCindy as a plug-in for an interactive geometry software Cinderella. Cinderella has two screens: the interactive geometric screen and a screen that describes Cinderella commands called Script Editors. When a KeTCindy command is run in Script Editors, the corresponding KeTpic commands are extracted to the proper position of the three parts in a Scilab executable file described above. This paper explains the KeTCindy system from the viewpoint of the programming style for drawings and introduces the author’s related website, which describes the utilization of KeTCindy.

swMATH with its web interface www.swmath.org is an open access portal for mathematical software and mathematical research data. After 5 years in operation, it provides information on more than 12,500 items in all mathematical fields and lists nearly 120,000 scientific publications citing the software (May 2016). A unique and novel feature of swMATH besides its scope is the so-called publication-based approach, which uses the information of the scientific database Zentralblatt MATH (zbMATH) for identifying mathematical software and extracting relevant information about them.

We describe an XML file format for storing data from computations in algebra and geometry. We also present a formal specification based on a RELAX-NG schema.

One of the goals of the SymbolicData Project is to set up a navigational structure on the research data associated with the project. In 2009 we started to refactor the data and metadata along standard semantic web concepts based on the Resource Description Framework (RDF) thus opening the door to the Linked Open Data world.One of the main metadata concepts used for navigational purposes is that of semantic-aware fingerprints as semantically sound invariants of the given data. We applied this principle, first used to navigate within polynomial systems data, to the data sets on polytopes and on transitive groups newly integrated with SymbolicData version 3, and also within the recompiled version of test sets from integer programming.The RDF based representation of fingerprints allows for a unified navigation and even cross navigation within such data using the SPARQL query mechanism as a generic web service, a clear advantage compared to metadata management traditionally in use within the domain of computer algebra.In this paper we discuss merely the conceptual background of our fingerprinting approach and refer to the SymbolicData wiki for more details and examples how to use that service.

The Web is our primary source of all kinds of information today. This includes information about software as well as associated materials, like source code, documentation, related publications and change logs. Such data is of particular importance in research in order to conduct, comprehend and reconstruct scientific experiments that involve software. swMATH, a mathematical software directory, attempts to identify software mentions in scientific articles and provides additional information as well as links to the Web. However, just like software itself, the Web is dynamic and most likely the information on the Web has changed since it was referenced in a scientific publication. Therefore, it is crucial to preserve the resources of a software on the Web to capture its states over time.We found that around 40 % of the websites in swMATH are already included in an existing Web archive. Out of these, 60 % of contain some kind of documentation and around 45 % even provide downloads of software artifacts. Hence, already today links can be established based on the publication dates of corresponding articles. The contained data enable enriching existing information with a temporal dimension. In the future, specialized infrastructure will improve the coverage of software resources and allow explicit references in scientific publications.

Mathematical modeling and simulation (MMS) has now been established as an essential part of the scientific work in many disciplines and application areas. It is common to categorize the involved numerical data and to some extend the corresponding scientific software as research data. Both have their origin in mathematical models. In this contribution we propose a holistic approach to research data in MMS by including the mathematical models and discuss the initial requirements for a conceptual data model for this field.

In the last centuries mathematical research results were published on paper, as articles, reports, monographs, etc. The permanently increasing number of mathematical publications required to develop powerful information management services and tools for search and access to mathematical knowledge. 1868, the ‘Jahrbuch über die Fortschritte der Mathematik’ was founded to inform the mathematical community and interested scientists on the progress of mathematical knowledge. Also today, its successors, the bibliographic databases zbMATH and MathSciNet, provide an overview about recent developments in mathematics. But the digital era has changed the situation dramatically. All kinds of information are stored in digital form. Mathematical research results are not longer limited to mathematical publications. New types and formats of mathematical data and knowledge tackle new challenges also to information services. The talk addresses the subject of Mathematical SoftWare (MathSW) in the context of Mathematical Research Data (MathRD) and describes some challenges to create information services for this data from a personal view.

In the frame of the work of the Working Group “Global Digital Mathematical Library”, Jim Pitman proposed Aart Stam’s collection of combinatorial identities as a benchmark for “digitizing” mathematical knowledge. This collection seems to be a challenge for “digitization” because of its size (1300 pages in a .pdf file) and because of the fact that, for the most part, it is hand-written. However, after an in-depth analysis, it turns out that the real challenges are of mathematical and logical nature. In this talk we discuss what digitization of such a piece of mathematics means and report on various tools that may help in this endeavor. The tools range from technical tools for typing formulae all the way to sophisticated algebraic and reasoning algorithms. The experiments for applying these tools to Stam’s collection are currently carried out by two of the working groups at RISC.

We give a report on the EuKIM project, which was recently submitted to the EU Horizon 2020 program, INFRAIA-02-2017 (Integrating Activities for Starting Communities) topic, by a consortium of twelve European research groups. The project aims at building up a “Global Digital Math Library” (knowledge base) integrating and extending current efforts worldwide. A central part of the project is the design and implementation of a software system that organizes open and one-stop access to mathematical knowledge and to various tools for processing mathematical knowledge. Recent progress in automated reasoning is an important issue for achieving more sophisticated levels in this endeavor.

In this article we give a brief description of the method for constructing a collection of conference talks applied in the Math-Net.Ru project.

Mathematical vernacular – the everyday language we use to communicate about mathematics is characterized by a special vocabulary. If we want to support humans with mathematical documents, we need to extract their semantics and for that we need a resource that captures the terminological, linguistic, and ontological aspects of the mathematical vocabulary. In the SMGloM project and system, we aim to do just this. We present the glossary system prototype, the content organization, and the envisioned community aspects.

A decade after a resolution in 2006 by the International Mathematical Union endorsing the notion of a global digital mathematics library, and following a thorough report on possibilities written under the auspices of the US National Research Council in 2012, an 8-person Working Group, set up in 2014, is still working toward implementations of some of the ideas. There are difficulties with mobilizing the mathematical community toward building worthwhile infrastructure in times that are both perilous and well off, depending on where you stand. But progress continues.

The On-line Encyclopedia of Integer Sequences (OEIS) is an important resource for mathematicians. The database is well-structured and rich in mathematical content but is informal in nature, so knowledge management services are not directly applicable. In this paper we provide a partial parser for the OEIS that leverages the fact that, in practice, the syntax used in its formulas is fairly regular. Then, we import the result into OMDoc to make the OEIS accessible to OMDoc-based knowledge management applications. We exemplify this with a formula search application based on the MathWebSearch system and a program that finds relations between the OEIS sequences.

Scientific videos often are supplementary material to otherwise published research material or contain additional material on their own. Especially in the mathematical context there are four main categories of accompanying media: (1) visual demonstrations of numerical simulations, (2) video recordings of conference talks, (3) video abstracts for journal submissions, and (4) lecture videos. TIB’s AV portal links its videos to all kinds of supplementary research information if it is freely available. Furthermore, a user’s query to the portal is automatically expanded to a query in TIB’s discovery system in order to retrieve supplementary material for further reading indexed therein. This article discusses the four categories of media combinations listed above and how to interlink them in order to guarantee easy access.

Two questions often come up when the author discusses integration: what is the complexity of the integration process, and for what special values of parameters is an unintegrable function actually integrable. These questions have not been much considered in the formal literature, and where they have been, there is one recent development indicating that the question is more delicate than had been supposed.

We address a variant of the classical Steiner tree problem defined over undirected graphs. The objective is to determine the Steiner tree rooted at a source node with minimum cost and such that the number of edges is less than or equal to a given threshold. The link constrained Steiner tree problem ($$\mathcal {LCSTP}$$) belongs to the NP-hard class. We formulate a Lagrangian relaxation for the $$\mathcal {LCSTP}$$ in order to determine valid bounds on the optimal solution. To solve the Lagrangian dual, we develop a dual ascent heuristic based on updating one multiplier at time. The proposed heuristic relies on the execution of some sub-gradient iterations whenever the multiplier update procedure is unable to generate a significant increase of the Lagrangian dual objective. We calculate an upper bound on the $$\mathcal {LCSTP}$$ by adjusting the infeasibility of the solution obtained at each iteration. The solution strategy is tested on instances inspired by the scientific literature.

Describing a three dimensional object requires a computer code whose maintenance is difficult. Part of the problem is the gap between the 3D-software languages based on coordinates and the natural geometric description of the object which is primarily coordinate free.Pycao is a software built to reduce the gap between the natural language and the software language in 3D-modelisation. The Pycao language is designed to avoid coordinates as much as possible. The available concepts include CSG geometry, the framework of affine geometry in a massic space, an intuitive “box model”, and several systems of measurements which mimic the operations in the workshop. It is developed as a python module to get a code compact and easy to read.

We propose a general algorithmic approach to noncommutative operator algebras generated by linear operators using quotients of tensor algebras. In order to work with reduction systems in tensor algebras, Bergman’s setting provides a tensor analog of Gröbner bases. We discuss a modification of Bergman’s setting that allows for smaller reduction systems and tends to make computations more efficient. Verification of the confluence criterion based on S-polynomials has been implemented as a Mathematica package. Our implementation can also be used for computer-assisted construction of Gröbner bases starting from basic identities of operators. We illustrate our approach and the software using differential and integro-differential operators as examples.

Voronoi diagrams tessellate the space where each cell corresponds to an associated generator under an a priori defined distance and have been extensively used to solve geometric problems of various disciplines. Additively-weighted Voronoi diagrams, also called the Voronoi diagram of disks and spheres, have many critical applications and a few algorithms are known. However, algorithmic robustness remains a major hurdle to use these Voronoi diagrams in practice. There are two important yet different approaches to design robust algorithms: the exact-computation and topology-oriented approaches. The former uses high-precision arithmetic and guarantees the correctness mathematically with the cost of a significant use of computational resources. The latter focuses on topological properties to keep consistency using logical computation rather than numerical computation. In this paper, we present a robust and efficient algorithm for computing the Voronoi diagram of disks using a topology-oriented incremental method. The algorithm is rather simple as it primarily checks topological changes only during each disk is incrementally inserted into a previously constructed Voronoi diagram of some other disks.

Currently, only a limited number of fonts are available for high quality mathematical typesetting, such as Knuth’s computer modern font, the Stix font, and several fonts from the Gyre family. An interesting challenge is to develop tools which allow users to pick any existing favorite font and to use it for writing mathematical texts. We will present progress on this problem as part of recent developments in the GNU scientific text editor.