Mathematical Software – ICMS 2020

The solution and a portable implementation of the inverse kinematics computation of a 3 degree-of-freedom (DOF) robot manipulator using Gröbner bases are presented. The main system was written Python with computer algebra system SymPy. Gröbner bases are computed with computer algebra system Risa/Asir, called from Python via OpenXM infrastructure for communicating mathematical software systems. For solving a system of algebraic equations, several solvers (both symbolic and numerical) are used from Python, and their performance has been compared. Experimental results with different solvers for solving a system of algebraic equations are shown.

This paper is part of our ongoing research on the adaptation of Lazard’s CAD to benefit from equational constraints in formulae. In earlier work we combined the CAD methods of McCallum and Lazard so as to produce an efficient algorithm for decomposing a hypersurface rather than the whole of $$\mathbb {R}^n$$ (exploiting an equational constraint $$f=0$$ ). That method, however, fails if f is nullified (in McCallum’s terminology): we call the set where this happens a curtain. Here we provide a further modification which, at the cost of a trade off in terms of complexity, is valid for any hypersurface, including one containing curtains.

In this paper, we first prove that the incremental algorithm for computing triangular decompositions proposed by Chen and Moreno Maza in ISSAC’ 2011 in its original form preserves chordality, which is an important property on sparsity of variables. On the other hand, we find that the current implementation in Triangularize command of the RegularChains library in Maple may not always respect chordality due to the use of some simplification operations. Experimentation show that modifying these operations, together with some other optimizations, brings significant speedups for some super sparse polynomial systems.

We use an extension of quadratic Chabauty to number fields, recently developed by the author with Balakrishnan, Besser and Müller, combined with a sieving technique, to determine the integral points over on the Mordell curve $$y^2 = x^3-4$$ .

We develop a numerical nonlinear algebra approach for computing the Euler characteristic of an affine variety. Our approach is to relate Euler characteristics of a smooth affine variety with the number of critical points using Morse theory. In general, we stratify a variety into the union of smooth affine varieties to obtain results on singular varieties.

Polynomials which arise via elimination can be difficult to compute explicitly. By using a pseudo-witness set, we develop an algorithm to explicitly compute the restriction of a polynomial to a given line. The resulting polynomial can then be used to evaluate the original polynomial and directional derivatives along the line at any point on the given line. Several examples are used to demonstrate this new algorithm including examples of computing the critical points of the discriminant locus for parameterized polynomial systems.

In the theory of special functions, a particular kind of multidimensional integral appears frequently. It is called the Euler integral. In order to understand the topological nature of the integral, twisted de Rham cohomology theory plays an important role. We propose an algorithm of computing an invariant cohomology intersection number of a given basis of the twisted cohomology group. We also develop an algorithm of computing the Paffian system that a given basis satisfies. These algorithms are based on the fact that the Euler integral satisfies GKZ system and utilizes algorithms to find rational function solutions of differential equations. We provide software to perform this algorithm.

Computations with algebraic number fields and algebraic curves have been carried out for a long time. They resulted in many interesting examples and the formation of various conjectures.The aim of this talk is to report on some computations with algebraic surfaces that are currently possible.

We present a method for evaluating the reverse Grünwald-Letnikov fractional derivatives of the Riemann Zeta function $$\zeta (s)$$ and use it to explore the location of zeros of integral and fractional derivatives on the left half plane.

We present the ideas behind an algorithm to compute normalizers of primitive groups with non-regular socle in polynomial time. We highlight a concept we developed called permutation morphisms and present timings for a partial implementation of our algorithm. This article is a collection of results from the author’s PhD thesis.

This paper is a compressed summary of some principal definitions and concepts in the approach to the black box algebra being developed by the authors [6–8]. We suggest that black box algebra could be useful in cryptanalysis of homomorphic encryption schemes [11], and that homomorphic encryption is an area of research where cryptography and black box algebra may benefit from exchange of ideas.

We describe the functionality of the package zalgs for the computer algebra system GAP. The package contains an implementation of the nilpotent quotient algorithm for finitely presented associative $$\mathbb {Z}$$ -algebras described in [3]. As an application of this algorithm we calculate augmentation quotients, i.e. successive quotients of powers of the augmentation ideal I(G) of the integral group ring $$\mathbb {Z} G$$ , where G is a finitely presented group. We apply these methods to obtain conjectures for augmentation quotients of the Baumslag-Solitar groups BS(m, n) with $$\vert m - n \vert $$ equal to 0, 1 or a prime p.

A symbolic Lie p-ring defines a family of Lie rings with $$p^n$$ elements for infinitely many different primes p and a fixed positive integer n. Symbolic Lie p-rings are used to describe the classification of isomorphism types of nilpotent Lie rings of order $$p^n$$ for all primes p and all $$n \le 7$$ . This classification is available as the LiePRing package of the computer algebra system GAP. We give a brief description of this package, including an approach towards computing the automorphism group of a symbolic Lie p-ring.

A convex polyhedron is the convex hull of a finite set of points in $${\mathbb R}^3.$$ A triangulation of a convex polyhedron is a decomposition into a finite number of 3-simplices such that any two intersect in a common face or are disjoint. A simplicial dissection is a decomposition into a finite number of 3-simplices such that no two share an interior point. We present an algorithm to classify the simplicial dissections of a regular polyhedron under the symmetry group of the prolyhedron.

A hyperoval of a point-line geometry is a nonempty set of points meeting each line in either 0 or 2 points. We discuss a combination of theoretical and practical techniques that are helpful for classifying hyperovals of generalized quadrangles. These techniques are based on the connection between hyperovals, even sets and pseudo-embeddings of point-line geometries.

We consider the computer-aided constructive classification of parallelisms with predefined automorphism groups in small finite projective spaces. The usage of a backtrack search algorithm makes it very important to filter away equivalent partial solutions as soon as possible and to use a fast method for checking for isomorphism of any two parallelisms. The rejection of most of the equivalent solutions can be done by a test which uses the normalizer of the predefined automorphism group. We consider the applicability and effectiveness of such a test, and present sensitive invariants of resolutions of Steiner 2-designs. They can be used to facilitate any type of test for isomorphism of parallelisms.

An approach for classification of linear codes with given parameters starting from their proper residual codes or subcodes is presented. The base of the algorithm is the concept of canonical augmentation which is important for parallel implementations. The algorithms are implemented in the programs LengthExtension and DimExtension of the package QextNewEdition. As an application, the nonexistence of binary [41, 14, 14] codes is proved.

This paper is devoted to the program Generation which is a self-containing console application for classification of linear codes. It can be used for codes over fields with $$q<8$$ elements and with wide-range parameters. The base of the implemented algorithm is the concept of canonical augmentation.

We describe the implementation of algebraic polyhedra in Normaliz. In addition to convex hull computation/vertex enumeration, Normaliz computes triangulations, volumes, lattice points, face lattices and automorphism groups. The arithmetic is based on the package e-antic by V. Delecroix.

An implementation of Viro’s patchworking in polymake is presented, and a census of Betti numbers of real tropical surfaces serves as a showcase. The latter is relevant in the context of Hilbert’s 16th Problem.

We study the problem of estimating the volume of convex polytopes, focusing on zonotopes. Although a lot of effort is devoted to practical algorithms for polytopes given as an intersection of halfspaces, there is no such method for zonotopes. Our algorithm is based on Multiphase Monte Carlo (MMC) methods, and our main contributions include: (i) a new uniform sampler employing Billiard Walk for the first time in volume computation, (ii) a new simulated annealing generalizing existing MMC by making use of adaptive convex bodies which fit to the input, thus drastically reducing the number of phases. Extensive experiments on zonotopes show our algorithm requires sub-linear number of oracle calls in the dimension, while the best theoretical bound is cubic. Moreover, our algorithm can be easily generalized to any convex body. We offer an open-source, optimized C++ implementation, and analyze its performance. Our code tackles problems intractable so far, offering the first efficient algorithm for zonotopes which scales to high dimensions (e.g. one hundred dimensions in less than 1 h).

Recently Gouveia, Thomas and the authors introduced the slack realization space, a new model for the realization space of a polytope. It represents each polytope by its slack matrix, the matrix obtained by evaluating each facet inequality at each vertex. Unlike the classical model, the slack model naturally mods out projective transformations. It is inherently algebraic, arising as the positive part of a variety of a saturated determinantal ideal, and provides a new computational tool to study classical realizability problems for polytopes. We introduce the package SlackIdeals for Macaulay2, that provides methods for creating and manipulating slack matrices and slack ideals of convex polytopes and matroids. Slack ideals are often difficult to compute. To improve the power of the slack model, we develop two strategies to simplify computations: we scale as many entries of the slack matrix as possible to one; we then obtain a reduced slack model combining the slack variety with the more compact Grassmannian realization space model. This allows us to study slack ideals that were previously out of computational reach. As applications, we show that the well-known Perles polytope does not admit rational realizations and prove the non-realizability of a large simplicial sphere.

Hyperplane arrangements form the latest addition to the zoo of combinatorial objects dealt with by polymake. We report on their implementation and on a algorithm to compute the associated cell decomposition. The implemented algorithm performs significantly better than brute force alternatives, as it requires fewer convex hulls computations. The implementation is included in polymake since release 4.0.

We exhibit a class of classical or tropical posynomial systems which can be solved by reduction to linear or convex programming problems. This relies on a notion of colorful vectors with respect to a collection of Newton polytopes. This extends the convex programming approach of one player stochastic games.

We designed a user-extensible judgemental equality checking algorithm for general type theories that supports computation rules and extensionality rules. The user needs only provide the equality rules they wish to use, after which the algorithm devises an appropriate notion of normal form. The algorithm is a generalization of type-directed equality checking for Martin-Löf type theory, and we implemented it in the Andromeda 2 prover.

Domain of mathematical logic in computers is dominated by automated theorem provers (ATP) and interactive theorem provers (ITP). Both of these are hard to access by AI from the human-imitation approach: ATPs often use human-unfriendly logical foundations while ITPs are meant for formalizing existing proofs rather than problem solving. We aim to create a simple human-friendly logical system for mathematical problem solving. We picked the case study of Euclidean geometry as it can be easily visualized, has simple logic, and yet potentially offers many high-school problems of various difficulty levels. To make the environment user friendly, we abandoned strict logic required by ITPs, allowing to infer topological facts from pictures. We present our system for Euclidean geometry, together with a graphical application GeoLogic, similar to GeoGebra, which allows users to interactively study and prove properties about the geometrical setup.

Formal mathematics is getting increasing attention in mathematics and computer science. In particular, the formalization of calculus has important applications in engineering design and analysis. In this paper, we present a formal proof of some fundamental theorems of continuous functions on closed intervals based on the Coq proof assistant. In this formalization, we build a real number system referring to Landau’s Foundations of Analysis. Then we complete the formalization of the basic definitions of interval, function, and limit and formally prove the theorems including completeness theorem, intermediate value theorem, uniform continuity theorem and others in Coq. The proof process is normalized, rigorous and reliable.

Cylindrical algebraic decomposition (CAD) is a fundamental tool in computational real algebraic geometry. Previous studies have shown that machine learning (ML) based approaches may outperform traditional heuristic ones on selecting the best variable ordering when the number of variables $$n\le 4$$ . One main challenge for handling the general case is the exponential explosion of number of different orderings when n increases. In this paper, we propose an iterative method for generating candidate variable orderings and an ML approach for selecting the best ordering from them via learning neural network classifiers. Experimentations show that this approach outperforms heuristic ones for $$n=4,5,6$$ .

This paper considers the application of machine learning to automatically generating heuristics for real polynomial constraint solvers. We consider a specific choice-point in the algorithm for constructing an open Non-uniform Cylindrical Algebraic Decomposition (NuCAD) for a conjunction of constraints, and we learn a heuristic for making that choice. Experiments demonstrate the effectiveness of the learned heuristic. We hope that the approach we take to learning this heuristic, which is not a natural fit to machine learning, can be applied effectively to other choices in constraint solving algorithms.

We are interested in the application of Machine Learning (ML) technology to improve mathematical software. It may seem that the probabilistic nature of ML tools would invalidate the exact results prized by such software, however, the algorithms which underpin the software often come with a range of choices which are good candidates for ML application. We refer to choices which have no effect on the mathematical correctness of the software, but do impact its performance.In the past we experimented with one such choice: the variable ordering to use when building a Cylindrical Algebraic Decomposition (CAD). We used the Python library Scikit-Learn (sklearn) to experiment with different ML models, and developed new techniques for feature generation and hyper-parameter selection.These techniques could easily be adapted for making decisions other than our immediate application of CAD variable ordering. Hence in this paper we present a software pipeline to use sklearn to pick the variable ordering for an algorithm that acts on a polynomial system. The code described is freely available online.

We present the Mathematical Functions Grimoire (FunGrim), a website and database of formulas and theorems for special functions. We also discuss the symbolic computation library used as the backend and main development tool for FunGrim, and the Grim formula language used in these projects to represent mathematical content semantically.

The Open Research Knowledge Graph (ORKG) provides machine-actionable access to scholarly literature that habitually is written in prose. Following the FAIR principles, the ORKG makes traditional, human-coded knowledge findable, accessible, interoperable, and reusable in a structured manner in accordance with the Linked Open Data paradigm. At the moment, in ORKG papers are described manually, but in the long run the semantic depth of the literature at scale needs automation. Operational Research is a suitable test case for this vision because the mathematical field and, hence, its publication habits are highly structured: A mundane problem is formulated as a mathematical model, solved or approximated numerically, and evaluated systematically. We study the existing literature with respect to the Assembly Line Balancing Problem and derive a semantic description in accordance with the ORKG. Eventually, selected papers are ingested to test the semantic description and refine it further.

Scientists increasingly rely on computer algebra systems and digital mathematical libraries to compute, validate, or experiment with mathematical formulae. However, the focus in digital mathematical libraries and scientific documents often lies more on an accurate presentation of the formulae rather than providing uniform access to the semantic information. But, presentational math formats do not provide exclusive access to the underlying semantic meanings. One has to derive the semantic information from the context. As a consequence, the workflow of experimenting and publishing in the Sciences often includes time-consuming, error-prone manual conversions between presentational and computational math formats. As a contribution to improve this workflow, we propose a context-sensitive approach that extracts semantic information from a given context, embeds the information into the given input, and converts the semantically enhanced expressions to computer algebra systems.

We discuss design aspects of the open-source Basic Polynomial Algebra Subprograms (BPAS) library. We build on standard C++11 template mechanisms to improve ease of use and accessibility. The BPAS computer algebra library looks to enable end-users to do work more easily and efficiently through optimized C code wrapped in an object-oriented and user-friendly C++ interface. Two key aspects of this interface to be discussed are the encoding of the algebraic hierarchy as a class hierarchy and a mechanism to support the combination of algebraic types as a new type. Existing libraries, if encoding the algebraic hierarchy at all, use runtime value checks to determine if two elements belong to the same ring for an incorrect false sense of type safety in an otherwise statically-typed language. On the contrary, our template metaprogramming mechanism provides true compile-time type safety and compile-time code generation. The details of this mechanism are transparent to end-users, providing a very natural interface for an end-user mathematician.

The purpose of this project is to test and evaluate an approach for Formula Concept Discovery (FCD). FCD aims at retrieving a formula concept (in the form of a Wikidata item) together with its defining formula within documents, in this case 100 English Wikipedia articles. To correctly identify the defining formula of a Wikipedia article, this approach searches for shared formulae across Wikipedia articles available in different languages. The formula shared in the most languages is then assumed to be the defining formula. The results show that neither this approach alone nor a combination with an existing approach that considers the order of the formulae inside an article leads to satisfying results. It is thus concluded that the number of times a formula is shared across a Wikipedia article in different languages is not a good indicator to determine the defining formula with the current approach. Consequently, several ideas for further research are proposed which could improve the results.

Software, and software source code in particular, is widely used in modern research. It must be properly archived, referenced, described and cited in order to build a stable and long lasting corpus of scientific knowledge. In this article we show how the Software Heritage universal source code archive provides a means to fully address the first two concerns, by archiving seamlessly all publicly available software source code, and by providing intrinsic persistent identifiers that allow to reference it at various granularities in a way that is at the same time convenient and effective.We call upon the research community to adopt widely this approach.

We present the Julia interface to polymake, a software for research in polyhedral geometry. We describe the technical design and how the integration into Julia makes it possible to combine polymake with state-of-the-art numerical software.

Since 2012, web based notebooks have been used as interface for computer algebra systems in teaching mathematics courses at Universidad de Zaragoza. We present an overview of the experience, detailing the advantages and problems that have been noticed during this time.

In this extended abstract, we present how to compute and visualize phase portraits of bi-dimensional Zeta Values. Such technology is useful to explore bi-dimensional Zeta Values and in long-term quest to discover a 2D-Riemann hypothesis.To reach this goal, we need two preliminary steps: $$\bullet $$ the notion of phase portraits and a general tool to visualize phase portrait based on interactive Jupyter widgets. $$\bullet $$ the ability to compute numerical approximations of bi-dimensional Zeta values, using mpmath, a Python library for arbitrary-precision floating-point arithmetic. To this end, we develop a theory to numerically compute double sums and produce the first algorithm to compute bi-dimensional Zeta Values with complex parameters.

The Grammatical Logical Framework (GLF) is a framework for prototyping the translation of natural language sentences into logic. The motivation behind GLF was to apply it to mathematical language, as the classical compositional approach to semantics construction seemed most suitable for a domain where high precision was mandatory—even at the price of limited coverage. In particular, software for formal mathematics (such as proof checkers) require formal input languages. These are typically difficult to understand and learn, raising the entry barrier for potential users. A solution is to design input languages that closely resemble natural language. Early results indicate that GLF can be a useful tool for quickly prototyping such languages. In this paper, we will explore how GLF can be used to prototype such languages and present a new Jupyter kernel that4 adds visual support for the development of GLF-based syntax/semantics interfaces.

When studying mathematics, it is important to solve exercises of an appropriate level. Recently, web-based assessment systems with a computer algebra system (CAS), e.g., Moodle with Stack and the Möbius platform with Maple, have become popular. Such web-based systems are convenient; however, they have some problems relative to inputting and evaluating mathematical formulas. In addition, when considering and solving mathematical problems, handwriting mathematics is important. We want management system of paper-oriented exercises. Auto multiple choice (AMC), which was developed by Alexis Bienvenüe, is open source software for creating and managing multiple choice questionnaires with automated marking. is the native AMC language for questionnaire descriptions. We propose to combine AMC and CAS using Lua , which is a -based computer typesetting system with an embedded Lua scripting engine. We can embed CAS scripts into Lua source, and, by creating exercises with CAS, we can generate various problems with random coefficients or terms. By providing various patterns of practice problems and facilitating discussions with each student, we expect sufficient educational benefits of providing opportunities to communicate about mathematical concepts and algorithms among students.

In this article, we show a flow-based programming environment for interactive geometry software. Flow-based programming is one of the programming paradigms. All of the processes and data are represented as nodes, and we connect processes and data with edges. We call the figure with nodes and edges graph because the figure looks like a planar graph.There is a lot of software implementing flow-based programming. However, there are few mathematical software based on a flow-based programming environment. So, we develop experimental interactive geometry software to generate kaleidoscope patterns based on flow-based programming.The software shows us some advantages of flow-based programming. First, it is easy to understand the procedure of construction. Second, flow-based programming is flexible. Third, flow-based programming has high extensibility. We seek possibilities of practical use of the geometrical construction software with flow-based programming.

When synthesizing feedback controllers for large-scale dynamical systems, often a reduction of the plant model by model order reduction is required. This is a typical task in computer-aided control system design environments. Therefore, in the last years, model order reduction became an essential tool for the practical use of mathematical models in engineering processes. For the integration of established model order reduction methods into those processes, software solutions are needed. In this paper, we describe the MORLAB (Model Order Reduction LABoratory) toolbox as such a software solution in MathWorks MATLAB® and GNU Octave, and its featured integration into established software tools used in simulations and controller design. We give benchmark examples for two important extensions of the toolbox.

In this paper we present the SageMath package FlexRiLoG (short for flexible and rigid labelings of graphs). Based on recent results the software generates motions of graphs using special edge colorings. The package computes and illustrates the colorings and the motions. We present the structure and usage of the package.

Computer software interfaces for mathematics collaboration and problem solving rely, as all interfaces do, on user identification and recognition of symbols (via icons and other contextual widgets). In this paper we examine the results of a short study which examined users interacting with mathematics software (Mathematics Classroom Communicator, MC $$^2$$ ) designed for education, real-time communication and collaboration. Videos were recorded of 14 users working through seven comprehensive problems in the MC $$^2$$ interface. Extensive second-by-second coding was completed of the user’s actions and status throughout their work, and a set of transition matrices were tabulated, estimating transition probabilities between symbols, operators and other aspects of mathematical expressions. We discuss the results of these matrices, and their implications in the translation of abstract mathematical concepts into software interfaces, and further conclude with a brief discussion of suggestions for mathematical software interface design. This study also has applications in mathematical software usability and accessibility.

We consider the question of certifying that a polynomial in $${\mathbb Z}[x]$$ or $${\mathbb Q}[x]$$ is irreducible. Knowing that a polynomial is irreducible lets us recognise that a quotient ring is actually a field extension (equiv. that a polynomial ideal is maximal). Checking that a polynomial is irreducible by factorizing it is unsatisfactory because it requires trusting a relatively large and complicated program (whose correctness cannot easily be verified). We present a practical method for generating certificates of irreducibility which can be verified by relatively simple computations; we assume that primes and irreducibles in $${\mathbb F}_p[x]$$ are self-certifying.

It is observed that some OpenMath objects may benefit from containing comments. A content dictionary with suitable attribution symbols is proposed. This content dictionary also provides application symbols for constructing comments that are somewhat more than just plain text strings.

The tangent Graeffe method has been developed for the efficient computation of single roots of polynomials over finite fields with multiplicative groups of smooth order. It is a key ingredient of sparse interpolation using geometric progressions, in the case when blackbox evaluations are comparatively cheap. In this paper, we improve the complexity of the method by a constant factor and we report on a new implementation of the method and a first parallel implementation.