Mathematical Software – ICMS 2014

Long before current graphic, visualisation and geometric tools were available, John E. Littlewood (1885-1977) wrote in his delightful

Miscellany

:

A heavy warning used to be given [by lecturers] that pictures are not rigorous; this has never had its bluff called and has permanently frightened its victims into playing for safety. Some pictures, of course, are not rigorous, but I should say most are (and I use them whenever possible myself). [p. 53]

Over the past five years, the role of visual computing in my own research has expanded dramatically. In part this was made possible by the increasing speed and storage capabilities—and the growing ease of programming—of modern multi-core computing environments.

But, at least as much, it has been driven by my group’s paying more active attention to the possibilities for graphing, animating or simulating most mathematical research activities.

In this talk we argue that mathematics is essentially software. In fact, from the beginning of mathematics, it was the goal of mathematics to automate problem solving. By systematic and deep thinking, for problems whose solution was difficult in each individual instance, systematic procedures were found that allow to solve each instance without further thinking. In each round of automation in mathematics, the deep thinking on spectra of problem instances is reflected by deep theorems with deep proofs.

The formalisation of mathematics by use of theorem provers has reached the stage where previously questioned mathematical proofs have been formalised. However, sceptics will argue that lingering doubts remain about the efficacy of these formalisations. In this paper we motivate and describe a capability for addressing such concerns. We concentrate on the nearly-complete Flyspeck Project, which uses the HOL Light system to formalise the Kepler Conjecture proof. We first explain why a sceptic might doubt the formalisation. We go on to explain how the formal proof can be ported to the highly-trustworthy HOL Zero system and then independently audited, thus resolving any doubts.

Symbolic Computing package is an add-on package that facilitates symbolic computation in Mathematica. It enables display and interpretation of derivatives, integrals, sums, products, vector operators, brackets, and various forms of subscripts and superscripts using the traditional mathematical notation based on the low-level box language and contains over 700 functions for notation, algebraic manipulation and evaluation of mathematical expressions. The package function categories include: basic algebra, complex variables, differential calculus, elementary functions, equation solving, equations, formula manipulation, Fourier analysis, function analysis, integral calculus, operator analysis, polynomials and series, products, sums, trigonometric functions, vectors and matrices. The package has its own interpreter language, complete on-line documentation and two palettes for entering mathematical expressions and execution control of functions. This provides a powerful platform for streamlined manipulation of all or parts of an expression and will significantly enhance the capabilities of the kernel and user-defined functions. Development of the package and its applications to various topics of mathematics and related disciplines will be presented.

There is an interesting duality between the forms and extents of mathematical knowledge that is verbally expressed (published in articles, scribbled on blackboards, or presented in talks/discussions) and the forms that are needed to successfully extend and apply mathematics. To “do mathematics”, we need to judge the veracity, extract the relevant structures, and reconcile them with the context of our existing knowledge - recognizing parts as already known and identifying those that are new to us. In this process we may abstract from syntactic differences, and even employ interpretations via non-trivial mappings as long as they are meaning-preserving.

There are new roles for software in mathematical knowledge management (MKM). Three simple initial examples of MKM roles will be considered here. The first is software applied to the Mathematical Subject Classification (MSC). The second example is MathML (Mathematics Markup Language), a standard from the W3C, now in its third edition, and hoping to become an ISO standard. The third example of software in the service of mathematical knowledge is the use of programs to analyze the nature of our subject as represented by its literature seen as a network. How these tools have already been deployed makes clear that mathematical knowledge management, even in its primitive present form, can aid further development of mathematics. These examples above are just starting points.

Representation formats based on theory graphs have been successful in formalized mathematics as they provide valuable logic-compatible modularity and foster reuse. Theories - sets of symbols and axioms – serve as modules and theory morphisms - truth-preserving mappings from the (language of the) source theory to the target theory – formalize inheritance and applicability of theorems. The MMT [4] system re-developed the formal part of the OMDoc theory graph into a foundation-independent meta-system for formal mathematics and implemented it in the MMT API.

In this talk we present the formalization and formal verification of the complexity analysis of Buchberger’s algorithm in the bivariate case in the computer system

Theorema

as a case study for using the system in mathematical theory exploration.

We describe how Buchberger’s original complexity proof for Groebner bases can be carried out within the

Theorema

system. As in the original proof, the whole setting is transferred from rings of bivariate polynomials over fields to the discrete space of pairs of natural numbers by mapping each polynomial to the exponent vector of its leading monomial. The complexity analysis is then carried out in the discrete space, mostly by means of combinatorial methods that require many tedious case distinctions, making this proof a natural candidate for automated theorem proving. However, following our

Theorema

philosophy, we do not expect general theorem provers (like resolution provers) to carry out this task in a natural and efficient way. Rather, we designed and implemented a special prover for such proofs. We show how the

Theorema

philosophy of working in parallel both on the meta level (designing and implementing special provers) and on the object level (design of the notions and theorems) of a theory can lead to a new quality and style of mathematical research.

Theorema 2.0 stands for a re-design including a complete re-implementation of the Theorema system, which was originally designed, developed, and implemented by Bruno Buchberger and his Theorema group at RISC. In this talk, we want to present the current status of the new implementation, in particular the new user interface of the system.

We introduce a new approach in black box group theory which deals with black box group problems in the category of black boxes and their morphisms. This enables us to enrich black box groups by actions of outer automorphisms such as Frobenius maps or graph automorphisms of simple groups of Lie type. As an application of this new technique, we present a number of new results, including a solution of an old problem about constructing unipotent elements in groups of Lie type of odd characteristic.

We report on the functionality and the underlying theory of the GAP package

CoReLG

(

Computing with Real Lie Groups

); it provides functionality to construct real semisimple Lie algebras, to check for isomorphisms, and to compute Cartan decompositions, Cartan subalgebras, and nilpotent orbits.

Bacterial genomes can be modelled as permutations of conserved regions. These regions are sequences of nucleotides that are identified for a set of bacterial genomes through sequence alignment, and are presumed to be preserved through the underlying process, whether through chance or selection. Once a correspondence is established between genomes and permutations, the problem of determining the evolutionary distance between genomes (in order to construct phylogenetic trees) can be tackled by use of group-theoretical tools. Here we review some of the resulting problems in computational group theory and describe

BioGAP

, a computer algebra package for genome rearrangement calculations, implemented in

GAP

.

We describe how the

SgpDec

computer algebra package can be used for composing and decomposing permutation groups and transformation semigroups hierarchically by directly constructing substructures of wreath products, the so called cascade products.

We exhibit an implementation in the computer algebra system

GAP

of a method to

approximate

generators of an integral arithmetic group.

Some problems in algorithmic group theory have good, well-understood, solutions as far as theory is concerned. This often is because of considering problems from other areas as solved, or because of ignoring practical aspects that are rarely if ever spelled out. This article considers some such aspects that have turned out to be difficult in the context of writing group theoretic software.

A tool package for computing genus 0 Belyi functions is presented, including simplification routines, computation of moduli fields, decompositions, dessins d’enfant. The main algorithm for computing the Belyi functions themselves is based on implied transformations of the hypergeometric differential equation to Fuchsian equations, preferably with few singular points. This gives a fast way to compute the Belyi functions (of degree 60 and beyond) with nearly regular branching patterns.

The Baues–Wirsching cohomology is one of the cohomologies of a small category. Our aim is to describe the first Baues–Wirsching cohomology of the small category generated by a finite quiver freely. We consider the case where the coefficient is a natural system obtained by the composition of a functor and the target functor. We give an algorithm to obtain generators of the vector space of inner derivations. It is known that there exists a surjection from the vector space of derivations of the small category to the first Baues–Wirsching cohomology whose kernel is the vector space of inner derivations.

In this work, we study the structure of skew constacyclic codes over the ring

R

 = 

F

4

[

v

]/〈

v

2

 − 

v

〉 which is a non chain ring with 16 elements where

F

4

denotes the field with 4 elements and

v

an indeterminate. We relate linear codes over

R

to codes over

F

4

by defining a Gray map between

R

and

$F_{4}^{2}.$

Next, the structure of all skew constacyclic codes is completely determined. Furthermore, we construct DNA codes over

R

.

Dougherty et al. calculated some of the weight enumerators of the projections of the 2-adic Golay code of length 24 to finite rings [Lifted codes and their weight enumerators, Discrete Mathematics, 305 (2005) 123–135]. In this paper, we calculate the missing values so that we complete the calculation of the weight enumerators of the projections of the 2-adic Golay code of length 24 to all the finite rings.

It is well known that there are exactly five inequivalent doubly-even binary self-dual codes of length 32 and minimum distance 8. The first proof was done by Conway and Pless in 1980. The second proof was given by H. Koch in 1989 by using the balance principle. Both proofs require nontrivial mathematical arguments. In this talk, we give a computer-aided proof of this fact.

Goppa’s codes on algebraic curves defined over finite fields, called AG codes, are usually regarded as the most successful class of error correcting codes in theory as well as in practice. Despite the splendid history of theoretic achievements though, an efficient algorithm decoding general AG codes appeared only recently. The decoding algorithm requires some precomputed data about the Riemann-Roch spaces of functions or differentials of the given curve of positive genus. As Magma is particularly good at computing with these spaces, the algorithm was implemented on Magma. We present its Magma implementation and describe certain details of the implementation.

In this study we focus on codes over a special family of commutative rings where we are able to construct a map that gives a correspondence between

k

-bases (

k

-letter words) of DNA with elements of the ring. By making use of so called coterm polynomials, we are able to solve the reversibility and complement problems in DNA codes and construct DNA codes over this ring.

The computation of persistent homology has proven a fundamental component of the nascent field of topological data analysis and computational topology. We describe a new software package for topological computation, with design focus on needs of the research community. This tool, replacing previous jPlex and Plex, enables researchers to access state of the art algorithms for persistent homology, cohomology, hom complexes, filtered simplicial complexes, filtered cell complexes, witness complex constructions, and many more essential components of computational topology.

We describe, herewithin, the design goals we have chosen, as well as the resulting software package, and some of its more novel capabilities.

PHAT is a C

++

library for the computation of persistent homology by matrix reduction. We aim for a simple generic design that decouples algorithms from data structures without sacrificing efficiency or user-friendliness. This makes PHAT a versatile platform for experimenting with algorithmic ideas and comparing them to state of the art implementations.

Persistence modules on commutative ladders naturally arise in topological data analysis. It is known that all isomorphism classes of indecomposable modules, which are the counterparts to persistence intervals in the standard setting of persistent homology, can be derived for persistence modules on commutative ladders of finite type. Furthermore, the concept of persistence diagrams can be naturally generalized as functions defined on the Auslander-Reiten quivers of commutative ladders. A previous paper [4] presents an algorithm to compute persistence diagrams by inductively applying echelon form reductions to a given persistence module. In this work, we show that discrete Morse reduction can be generalized to this setting. Given a quiver complex

$\mathbb{X}$

, we show that its persistence module

$H_q(\mathbb{X})$

is isomorphic to the persistence module

$H_q(\mathbb{A})$

of its Morse quiver complex

$\mathbb{A}$

. With this preprocessing step, we reduce the computation time by computing

$H_q(\mathbb{A})$

instead, since

$\mathbb{A}$

is generally smaller in size. We also provide an algorithm to obtain such Morse quiver complexes.

The problem of determining whether a given (finite abstract) simplicial complex is homeomorphic to a sphere is undecidable. Still, the task naturally appears in a number of practical applications and can often be solved, even for huge instances, with the use of appropriate heuristics. We report on the current status of suitable techniques and their limitations. We also present implementations in

polymake

and relevant test examples.

We present an efficient software package for computing homology of sets, maps and filtrations represented as cubical, simplicial and regular CW complexes. The core homology computation is based on classical Smith diagonalization, but the efficiency of our approach comes from applying several geometric and algebraic reduction techniques combined with smart implementation.

We present the main algorithmic and design choices that have been made to represent complexes and compute persistent homology in the Gudhi library. The Gudhi library (Geometric Understanding in Higher Dimensions) is a generic C++ library for computational topology. Its goal is to provide robust, efficient, flexible and easy to use implementations of state-of-the-art algorithms and data structures for computational topology. We present the different components of the software, their interaction and the user interface. We justify the algorithmic and design decisions made in Gudhi and provide benchmarks for the code. The software, which has been developped by the first author, will be available soon at

project.inria.fr/gudhi/software/

.

Bertini_real

is a command line program for numerically decomposing the real portion of a one- or two-dimensional complex irreducible algebraic set in any reasonable number of variables. Using numerical homotopy continuation to solve a series of polynomial systems via regeneration from a witness set, a set of real vertices is computed, along with connection information and associated homotopy functions. The challenge of embedded singular curves is overcome using isosingular deflation. This decomposition captures the topological information and can be used for further computation and refinement.

Homotopy continuation methods have been proved to be an efficient and reliable class of numerical methods for solving systems of polynomial equations which occur frequently in various fields of mathematics, science, and engineering. Based on the successful software package Hom4PS-2.0 for solving such polynomial systems, Hom4PS-3 has a new fully modular design which allows it to be easily extended. It implements many different numerical homotopy methods including the Polyhedral Homotopy continuation method. Furthermore, it is capable of carrying out computation in parallel on a wide range of hardware architectures including multi-core systems, computer clusters, distributed environments, and GPUs with great efficiency and scalability. Designed to be user-friendly, it includes interfaces to a variety of existing mathematical software and programming languages such as Python, Ruby, Octave, Sage and Matlab.

Cgal

, the Computational Geometry Algorithms Library, provides easy access to efficient and reliable geometric algorithms. Since its first release in 1997,

Cgal

is reducing the the gap between theoretical algorithms and data structure and implementations that can be used in practical scenarios.

Cgal

’s philosophy dictates correct results for any given input, even if intermediate round-off errors occur. This is achieved by its design, which separates numerical constructions and predicates from combinatorial algorithms and data structures. A naive implementation of the predicates and constructions still leads to wrong results, but reliable versions are shipped with the library.

Cgal

is successful in academic prototypical development and widely spread among industrial users. It follows the design principles of C++’s Standard Template Library.

Cgal

, now available in version 4.4, is already quite comprehensive. Nevertheless, it is still growing and improving.

We first introduce the library, its design and basics and then present major packages, such as triangulations and arrangements. We also illustrate showcases of how

Cgal

is used for real world applications asking for reliable geometric computing. The second part covers recent additions and contributions to the project: We discuss periodic and hyperbolic triangulations. The arrangement package has seen improvements for point location, rational functions and multi-part curves. It has also been extended with support for algebraic curves. This relies on several new packages that enable operations on (multivariate) polynomials and topology computation of such curves. Geometric objects in higher dimensions can now be represented using combinatorial maps; the instance for linear objects, namely the linear cell complex, is of particular interest.

Cgal

also provides data structures and algorithms for geometric sorting in arbitrary dimensions. Finally we present

Cgal

’s achievements to replace serial implementations with versions that support up-to-date multi-core architectures.

In this work we present a CGAL (Computational Geometry Algorithm Library) implementation of the line segment Voronoi diagram under the

L

 ∞ 

metric, building on top of the existing line segment Voronoi diagram under the Euclidean (

L

2

) metric in CGAL. CGAL is an open-source collection of geometric algorithms implemented in C++, used in both academia and industry. We also discuss an application of the

L

 ∞ 

segment Voronoi diagram in the area of VLSI pattern analysis. In particular, we identify potentially critical locations in VLSI design patterns, where a pattern, when printed, may differ substantially from the original intended VLSI design, improving on existing methods.

Libraries are available for the power diagram and the ordinary Voronoi diagram of points upon which application programs can be easily built. However, its counterpart for the Voronoi diagram of spheres does not exist despite of enormous applications, particularly those in molecular worlds. In this paper, we present the BULL! library which abbreviates “Beta Universe Library Liberandam!” for computing the Voronoi diagram of spheres, transforming it to the quasi-triangulation, and extracting the beta-complex. Being an engine library implemented in the standard C++, application programmers can simply call API-functions of BULL! to build application programs correctly, efficiently, and easily. The BULL! engine is designed so that the application programs developed by embedding API-functions are completely independent of the future modifications of the engine.

This paper describes computations of the relations between circumradius

R

and area

S

of cyclic polygons given by the lengths of the sides. Classic results by Heron and Brahmagupta clearly show the relation of circumradius and area for triangles and cyclic quadrilaterals. In contrast, formulae for the circumradius and the area of cyclic pentagons have been studied separately. D.P.Robbins obtained the area formula in 1994, which is a polynomial equation in (4

S

)

2

with degree 7. The circumradius formula was given by P.Pech in 2006, which is also a polynomial equation in

R

2

with degree 7. In this study, we succeeded in computing the

integrated formula

for the circumradius and the area of cyclic pentagons. It is found to be a polynomial equation in (4

SR

) with degree 7. This equation is easily transformed into the equation in (4

SR

)

2

with degree 7, hence both the expressions are meaningful. The existence of the latter form of formula was pointed out by D.Svrtan et al. in 2004, but somehow their result seems to contain typographical errors. Therefore, we believe that our results correspond to the correction and extension of already known formulae.

This paper presents a software to work with 3D dynamic geometry and multivariate calculus. It provides many resources to define and manipulate diverse 0D, 1D, 2D and 3D objects. Functions are defined explicitly or as the result of operations. Functions can (for example) be associated to 3D objects to calculate an iterated or a surface integral. The embedded CAS uses a novel and efficient scheme of representation for the common transcendental functions. Applications range from mathematical education to scientific simulation events passing by banal or utilities applications.

Among a large number of digital educational resources, high-quality resources are very scarce. For quite some time, the shortage of high-quality resources is the bottleneck problem of education informatization. In this paper, we will introduce an innovational feature of digital educational resources – sustainability, which includes interactivity, transparency, and openness. The transparency means that users can obtain the original creating process of educational resources by their contents. The openness means that users can conveniently edit the contents of educational resources. Sustainable educational resources will become better and better in quality through continuous optimization. The sustainable optimization of educational resources needs intelligent subject knowledge platform. We will demonstrate several cases of sustainable optimization based on Super Sketchpad (SSP) which is an excellent intelligent subject knowledge platform.

GeometryTouch is a dynamic geometry software system with touch operation. Developed by JavaScript and SVG, GeometryTouch is a Web-based application which can run on browsers of mobile devices. When using GeometryTouch, users can draw geometric figures and create or modify geometry-based interactive manipulatives. A virtual cursor is designed to implement precise operations in GeometryTouch. Geometric operations consist of 4 continuous actions and it is a challenge to implement the action of “the first point confirming”. Three methods have been investigated to tackle the problem in the paper.

OpenGeo is an enhanced version of the geometric knowledge base developed by Chen, Huang, and Wang, which is equipped with web-based interfaces and new management facilities and made open and online. The kernel of the knowledge base consists of typical geometric knowledge objects such as definitions, theorems, and proofs. Several tools have been developed to support users to manage the knowledge objects contained in OpenGeo. Users can create new knowledge objects and add them to OpenGeo.

Numerical algorithms for decomposing the real points of a complex curve or surface in any number of variables have been developed and implemented in the new software package

Bertini_real

. These algorithms use homotopy continuation to produce a cell decomposition. The previously existing algorithm for surfaces is restricted to the “almost smooth” case, i.e., the given surface must contain only finitely many singular points. We describe the use of isosingular deflation to remove this almost smooth condition and describe an implementation of deflation via

Bertini

with

MATLAB

.

Computing with curved geometric objects forms the basis for many algorithms in areas such as geometric modeling, computer aided design and robot motion planning. In general, such computations cannot be carried out reliably with standard machine precision arithmetic.

Slightly more than a decade ago robustly and efficiently dealing with conics and Bézier curves in 2D and quadrics and splines in 3D was considered an enormous challenge. This picture has changed. Our first successes were achieved for conics and quadrics, mainly relying on properties of the involved low-degree polynomials. In a second step, to tackle general algebraic curves and surfaces, we exploited more involved mathematical tools such as subresultants. In addition with clever filtering techniques, these methods already beat the previous specialized solutions. The most recent

drastical

success in performance gain for algebraic curves is due to several ingredients: The central one consists of a cylindrical algebraic decomposition with a revised lifting step. Using results from algebraic geometry we avoid any change of coordinates and replace the costly symbolic operations by numerical tools. The new algorithms for curve topology computation only need to compute the resultant and the gcd of bivariate polynomials and to perform numerical root finding. For the symbolic operations, we can rely on implementations exploiting graphics hardware, which is several magnitudes faster than corresponding CPU implementations.

All algorithms have been implemented as contributions to the C++! project

Cgal

. Excellent practical behavior of our algorithms has been shown in exhaustive sets of experiments, where we compared them with our previous and recent competing approaches. Beyond, the algorithms are also proven to be efficient in theory. Recent work shows that our implemented and practical algorithm needs

$\tilde{O}(d^6 + d^5\tau)$

bit operations (

d

degree,

τ

bitsize of coefficients) to compute the topology of an algebraic curve and for solving bivariate systems.

Joint work with Pavel Emeliyanenko, Michael Kerber, Kurt Mehlhorn, Michael Sagraloff, Alexander Kobel, and Pengming Wang.

This paper presents three algorithms to compute orthogonal projection of rational curves onto rational parameterized surface. One of them, based on regular systems, is able to compute the exact parametric loci of projection. The one based on Gröbner basis can compute the minimal variety that contains the parametric loci. The rest one computes a variety that contains the parametric loci via resultant. Examples show that our algorithms are efficient and valuable.

In this paper, we will introduce our implementation for isotopic approximation of plane and space algebraic curves. The important basic algorithm used in our implementation is real solving of zero-dimensional polynomial systems, especially for bivariate polynomial systems. For the topology computation of plane curves, compared to other symbolic methods, the novelty of our method is that we can get many simple roots on the fibers when computing the critical points of the plane curve, which greatly improves the lifting step. After the topology is computed, we also give a certified approximation for the plane curve, which is a basic operation for approximating a space curve and further for an algebraic surface. As to space curve case, the topology and approximation are recovered from that of their projection plane curves. We implemented our algorithms in Maple 15. The benchmarks show the high efficiency of the implementation.

We present a purely numerical (i.e., non-algebraic) subdivision algorithm for computing an isotopic approximation of a simple arrangement of curves. The arrangement is “simple” in the sense that any three curves have no common intersection, any two curves intersect transversally, and each curve is non-singular. A curve is given as the zero set of an analytic function on the plane, along with effective interval forms of the function and its partial derivatives. Our solution generalizes the isotopic curve approximation algorithms of Plantinga-Vegter (2004) and Lin-Yap (2009). We use certified numerical primitives based on interval methods. Such algorithms have many favorable properties: they are practical, easy to implement, suffer no implementation gaps, integrate topological with geometric computation, and have adaptive as well as local complexity. A preliminary implementation is available in Core Library.

Quantifier elimination (QE) over real closed fields has found numerous applications. Cylindrical algebraic decomposition (CAD) is one of the main tools for handling quantifier elimination of nonlinear input formulas. Despite of its worst case doubly exponential complexity, CAD-based quantifier elimination remains interesting for handling general quantified formulas and producing simple quantifier-free formulas.

In this paper, we report on the implementation of a QE procedure, called

QuantifierElimination

, based on the CAD implementations in the

RegularChains

library. This command supports both standard quantifier-free formula and extended Tarski formula in the output. The use of the QE procedure is illustrated by solving examples from different applications.

We consider the following problem of Quantifier Elimination (QE). Given a Boolean CNF formula

F

where some variables are existentially quantified, find a logically equivalent CNF formula that is free of quantifiers. Solving this problem comes down to finding a set of clauses depending only on free variables that has the following property: adding the clauses of this set to

F

makes all the clauses of

F

with quantified variables redundant. To solve the QE problem we developed a tool meant for handling a more general problem called partial QE. This tool builds a set of clauses adding which to

F

renders a specified subset of clauses with quantified variables redundant. In particular, if the specified subset contains all the clauses with quantified variables, our tool performs QE.

Linear equalities, disequalities and inequalities on fixed-width bit-vectors, collectively called linear modular constraints, form an important fragment of the theory of fixed-width bit-vectors. We present an efficient and bit-precise algorithm for quantifier elimination from conjunctions of linear modular constraints. Our algorithm uses a layered approach, whereby sound but incomplete and cheaper layers are invoked first, and expensive but complete layers are called only when required. We have extended the above algorithm to work with boolean combinations of linear modular constraints as well. Experiments on an extensive set of benchmarks demonstrate that our techniques significantly outperform alternative quantifier elimination techniques based on bit-blasting and Presburger Arithmetic.

Combining classical automated theorem proving techniques with theory based reasoning, such as satisfiability modulo theories, is a new approach to first-order reasoning modulo theories. Skolemization is a classical technique used to transform first-order formulas into

equisatisfiable

form. We show how Skolemization can benefit from a new satisfiability modulo theories based simplification technique of formulas called

monadic decomposition

. The technique can be used to transform a theory dependent formula over multiple variables into an equivalent form as a Boolean combination of unary formulas, where a unary formula depends on a single variable. In this way, theory specific variable dependencies can be eliminated and consequently, Skolemization can be refined by minimizing variable scopes in the decomposed formula in order to yield simpler Skolem terms.

The logic of quantified Boolean formulae (QBF) extends propositional logic by explicit existential and universal quantification of the variables. We present the search-based QBF solver DepQBF which allows to solve a sequence of QBFs incrementally. The goal is to exploit information which was learned when solving previous formulae in the process of solving the next formula in a sequence. We illustrate incremental QBF solving and potential usage scenarios by examples. Incremental QBF solving has the potential to considerably improve QBF-based workflows in many application domains.

NLCertify

is a software package for handling formal certification of nonlinear inequalities involving transcendental multivariate functions. The tool exploits sparse semialgebraic optimization techniques with approximation methods for transcendental functions, as well as formal features. Given a box and a transcendental multivariate function as input,

NLCertify

provides

OCaml

libraries that produce nonnegativity certificates for the function over the box, which can be ultimately proved correct inside the

Coq

proof assistant.

We are developing linear algebra packages on Risa/Asir, a computer algebra system. The aim is to provide programs for efficiently and exactly solving eigenproblems on the computer algebra system for large scale square matrices over integers or rational numbers. The software package consists of some programs. The followings are currently prepared for solving eigenproblems: computing eigenspaces, the spectral decomposition, Jordan chains and minimal annihilating polynomials.

The high-quality mathematical software for the computation of modified

Bessel

functions of the second kind with integer, imaginary and complex order and real argument is elaborated. The value of function may be evaluated with high precision for given value of the independent argument

x

and order

r

. These codes are addressed to the wide audience of scientists, engineers and technical specialists. The tables of these functions are published. This software improves significantly the capability of computer libraries. These functions arise naturally in boundary value problems involving wedge-shaped or cone-shaped geometries. They are fundamental to mathematical modeling activities in applied science and engineering. Methods of mathematical and numerical analysis are adapted for the creation of appropriate algorithms for these functions, computer codes are written and tested. Power series, Tau method and numerical quadratures of trapezoidal kind are used for the construction of subroutines. New realization of the Lanczos Tau method with minimal residue is proposed for the constructive approximation of the second order differential equations solutions with polynomial coefficients. A Tau method computational scheme is applied for the constructive approximation of a system of differential equations solutions related to the differential equation of hypergeometric type. Various vector perturbations are discussed. Our choice of the perturbation term is a shifted

Chebyshev

polynomial with a special form of selected transition and normalization. The minimality conditions for the perturbation term are found for one equation. They are sufficiently simple for verification in a number of important cases. Tau method’s approach gives a big advantage in the economy of computer’s time. The mathematical software for kernels of

Lebedev

type index transforms – modified

Bessel

functions of the second kind with complex order is elaborated in detail. The software for new applications of

Lebedev

type integral transforms and related dual integral equations for the numerical solution of problems of mathematical physics is constructed. The algorithm of numerical solution of some mixed boundary value problems for the Helmholtz equation in wedge domains is developed. Observed examples admitting complete analytical solution demonstrate the efficiency of this approach for applied problems.

The

side-chain prediction problem

(SCP-problem), is a computational problem to predict the optimal structure of proteins by finding the optimal dihedral angles. The SCP-problem is one of key computational cornerstones for many important problems such as protein design, flexible docking of proteins, homology modeling, etc. The SCP-problem can be formulated as a minimization problem of an integer linear program which is NP-hard thus inevitably invites heuristic approach to find the solution. In this paper, we report a heuristic algorithm, called BetaSCP2, which quickly finds an excellent solution of the SCP-problem. The solution process of the BetaSCP2 is facilitated by the Voronoi diagram and its dual structure called the quasi-triangulation. The BetaSCP2 is entirely implemented using the Molecular Geometry engine called BULL! which has been developed by Voronoi Diagram Research Center (VDRC) in C++ programming language. The benchmark test of the BetaSCP2 with other programs is also provided. The BetaSCP2 program is available as both a stand-alone and a web server program from VDRC.

Our most recent computations tell us that any counterexample to Giuga’s 1950 primality conjecture must have at least 19,908 decimal digits. Equivalently, any number which is both a Giuga and a Carmichael number must have at least 19,908 decimal digits. This bound has not been achieved through exhaustive testing of all numbers with up to 19,908 decimal digits, but rather through exploitation of the properties of Giuga and Carmichael numbers. This bound improves upon the 1996 bound of Borwein, Borwein, Borwein, and Girgensohn. We present the algorithm used, and discuss technical challenges and challenges to further computation.

We propose an efficient method for calculating “matrix polynomials” by extending the Horner’s rule for univariate polynomials. We extend the Horner’s rule by partitioning it by a given degree to reduce the number of matrix-matrix multiplications. By this extension, we show that we can calculate matrix polynomials more efficiently than by using naive Horner’s rule. An implementation of our algorithm is available on the computer algebra system Risa/Asir, and our experiments have demonstrated that, at suitable degree of partitioning, our new algorithm needs significantly shorter computing time as well as much smaller amount of memory, compared to naive Horner’s rule. Furthermore, we show that our new algorithm is effective for matrix polynomials not only over multiple-precision integers, but also over fixed-precision (IEEE standard) floating-point numbers by experiments.

CoCoA is a well-established Computer Algebra System for Computations in Commutative Algebra, and specifically for Gröbner bases.

In the last few years CoCoA has undergone a profound change: the code has been totally re-written in C++, and includes an integral open source C++ library, called CoCoALib.

The new CoCoA-5 language still resembles the CoCoA-4 language, and maintains or improves the naturalness and ease of use for which CoCoA-4 was noted, but the clearly defined semantics of the new language make it both more robust and more flexible than CoCoA-4.

Also its C++ mathematical core, CoCoALib, focusses on ease of use and robustness, so that other software can use it as a library for multivariate polynomial computations and other Commutative Algebra operations.

Moreover the internal design makes it easy to render new extensions to the library accessible also via the interactive CoCoA-5 system.

Nowadays, surface reconstruction from point clouds generated by laser scanning technology has become a fundamental task in many fields, such as robotics, computer vision, digital photogrammetry, computational geometry, digital building modeling, forest planning and operational activities. The point clouds produced by laser scanning, however, are limited due to the occurrence of occlusions, multiple reflectance and noise, and off-surface points (outliers), thus necessitating the need for robust fitting techniques. These techniques require repeated parameter estimation while eliminating outliers. Employing maximum likelihood estimation, the parameters of the model are estimated by maximizing the likelihood function, which maps the parameters to the likelihood of observing the given data. The transformation of this optimization problem into the solution of a multivariate polynomial system via computer algebra can provide two advantages. On the one hand, since all of the solutions can be computed, a single solution that provides global maximum can be selected. On the other hand, once the symbolic result has been computed, it can be used in numerical evaluations in a split second, which reduces the computation time. In our presentation, we applied Groebner basis to solve the maximization of the likelihood function in various robust techniques. A numerical example with data from a real laser scanner experiment illustrates the method. Computations have been carried out in the

Mathematica

environment.

In geodesy and geoinformatics, most problems are nonlinear in nature and often require the solution of systems of polynomial equations. Before 2002, solutions of such systems of polynomial equations, especially of higher degree remained a bottleneck, with iterative solutions being the preferred approach. With the entry of

Groebner basis

as algebraic solution to nonlinear systems of equations in geodesy and geoinformatics in the pioneering work “

Gröbner bases, multipolynomial resultants and the Gauss Jacobi combinatorial algorithms : adjustment of nonlinear GPS/LPS observations

”, the playing field changed. Most of the hitherto unsolved nonlinear problems, e.g., coordinate transformation, global navigation satellite systems (GNSS)’s pseudoranges, resection-intersection in photogrammetry, and most recently, plane fitting in point clouds in laser scanning have been solved. A comprehensive overview of such applications are captured in the first and second editions of our book

Algebraic Geodesy and Geoinformatics

published by Springer. In the coming

third edition

, an updated summary of the newest techniques and methods of combination of Groenbner basis with symbolic as well as numeric methods will be treated. To quench the appetite of the reader, this presentation considers an illustrative example of a two-dimension coordinate transformation problem solved through the combination of symbolic regression and Groebner basis.

In this talk we show how the theory of Groebner bases can be represented in the computer system

Theorema

, a system initiated by Bruno Buchberger in the mid-nineties. The main purpose of

Theorema

is to serve mathematical theory exploration and, in particular, automated reasoning. However, it is also an essential aspect of the

Theorema

philosophy that the system also provides good facilities for carrying out computations. The main difference between

Theorema

and ordinary computer algebra systems is that in

Theorema

one can both program (and, hence, compute) and prove (generate and verify proofs of theorems and algorithms). In fact, algorithms / programs in

Theorema

are just equational (recursive) statements in predicate logic and their application to data is just a special case of simplification w.r.t. equational logic as part of predicate logic.

We present one representation of Groebner bases theory among many possible “views” on the theory. In this representation, we use functors to construct hierarchies of domains (e. g. for power products, monomials, polynomials, etc.) in a nicely structured way, which is meant to be a model for gradually more efficient implementations based on more refined and powerful theorems or at least programming tricks, data structures, etc.

The most expensive part of the known algorithms in the calculation of primary fundamental invariants (of rings of polynomial invariants of finite linear groups over an arbitrary field) is the computation of the radicals of complete intersection ideals. Thus, in this paper, we develop effective methods for such calculation. For this purpose, we introduce first a new notion of genericity (called

D-quasi stable position

) and exhibit a novel

deterministic

algorithm to put an ideal in Nœther position (we show that this new notion of genericity is equivalent to Nœther position). Then, we use this algorithm and also the algorithm due to Krick and Logar (to compute radicals of ideals) to present an efficient algorithm to calculate the radical of a complete intersection ideal. Furthermore, we apply this algorithm, to improve the classical methods of computing primary invariants which are based on radical computation. Finally, we have implemented in

Maple

the mentioned algorithms (to put an ideal in Nœther position, to compute the radical of ideals and also primary invariants) and compare the proposed algorithms, via a set of benchmarks, with the corresponding functions in

Maple

and

Magma

. The experiments we made seem to show that these first implementations are already more efficient than the corresponding functions of

Maple

and

Magma

.

We present generic, type safe Groebner bases software. The implemented algorithms distinguish Groebner base computation in polynomials rings over fields, rings with pseudo division, parameter rings, regular rings, Euclidean rings, non-commutative fields in commuting, solvable and free-non-commuting main variables. The interface, class organization is described in the object-oriented programming environment of the Java Algebra System (JAS). Different critical pair selection strategies and reduction algorithms can be provided by dependency injection. Different implementations can be selected for the mentioned coefficient rings through factory classes and methods. Groebner bases algorithms can be composed according to application needs and/or hardware availability. For example, versions for shared memory sequential or parallel computation, term order optimization or fraction free coefficient ring computation can be composed. For distributed memory compute clusters there are OpenMPI and MPJ implementations of Buchberger’s algorithm with optimized distributed storage of reduction polynomials.

The application of the Groebner basis methodology to four nonlinear mechanics problems is discussed. The MAPLE software package is used in all cases to implement the Groebner basis calculation which converts a set of coupled polynomial algebraic equations into an equivalent set of uncoupled polynomial algebraic equations (the reduced Groebner basis). Observations concerning implementation of Groebner basis methodology are reported.

We present the canonical

Gröbner Cover

method for discussing parametric polynomial systems of equations. Its objective is to decompose the parameter space into subsets (

segments

) for which it exists a

generalized reduced Gröbner basis

in the whole segment with fixed set of leading power products on it. Wibmer’s Theorem guarantees its existence. The

Gröbner Cover

is designed in a joint paper of the authors, and the Singular grobcov.lib library [15] implementing it, is developed by Montes. The algorithm is canonic and groups the solutions having the same kind of properties into different disjoint segments. Even if the algorithms involved have high complexity, we show how in practice it is effective in many applications of medium difficulty. An interesting application to automatic deduction of geometric theorems is roughly described here, and another one to provide a taxonomy for exact geometrical loci computations, that is experimentally implemented in a web based application using the dynamic geometry software Geogebra, is explained in another session.

An algorithm is introduced for transforming a standard basis of a zero-dimensional ideal, in the formal power series ring, into another standard basis with respect to any given local ordering. The key ingredient of the proposed algorithm is an efficient method for solving membership problems for Jacobi ideals in local rings, that utilizes the Grothendieck local duality theorem. Namely, a new algorithm for computing a standard basis of a given zero-dimensional ideal with respect to any given local ordering, is derived by using algebraic local cohomology. Its implementation is introduced, too.

We propose a modular method for verifying the correctness of a Gröbner basis candidate. For an inhomogeneous ideal

I

, we propose to check that a Gröbner basis candidate

G

is a subset of

I

by computing an exact generating relation for each

g

in

G

by the given generating set of

I

via a modular method. The whole procedure is implemented in Risa/Asir, which is an open source general computer algebra system. By applying this method we succeeded in verifying the correctness of a Gröbner basis candidate computed in Romanovski et al (2007). In their paper the candidate was computed by a black-box software system and it has been necessary to verify the candidate for ensuring the mathematical correctness of the paper.

Cylindrical algebraic decomposition (CAD) is a fundamental tool in computational real algebraic geometry and has been implemented in several software. While existing implementations are all based on Collins’ projection-lifting scheme and its subsequent ameliorations, the implementation of CAD in the

RegularChains

library is based on triangular decomposition of polynomial systems and real root isolation of regular chains. The function in the

RegularChains

library for computing CAD is called

CylindricalAlgebraicDecompose

. In this paper, we illustrate by examples the functionality, the underlying theory and algorithm, as well the implementation techniques of

CylindricalAlgebraicDecompose

. An application of it is also provided.

The concept of

comprehensive triangular decomposition

(CTD) was first introduced by Chen

et al.

in their CASC’2007 paper and could be viewed as an analogue of comprehensive Gröbner systems for parametric polynomial systems. The first complete algorithm for computing CTD was also proposed in that paper and implemented in the

RegularChains

library in Maple. Following our previous work on generic regular decomposition for parametric polynomial systems, we introduce in this paper a so-called

hierarchical

strategy for computing CTDs. Roughly speaking, for a given parametric system, the parametric space is divided into several sub-spaces of different dimensions and we compute CTDs over those sub-spaces one by one. So, it is possible that, for some benchmarks, it is difficult to compute CTDs in reasonable time while this strategy can obtain some “partial” solutions over some parametric sub-spaces. The program based on this strategy has been tested on a number of benchmarks from the literature. Experimental results on these benchmarks with comparison to

RegularChains

are reported and may be valuable for developing more efficient triangularization tools.

Motivated by the problem of determining the Jordan and Weyr canonical forms of parametric matrices, we present a

Maple

package for doing symbolic linear algebra. The coefficients of our input matrices are multivariate rational functions, whose indeterminates are regarded as parameters and are subject to a system of polynomial equations and inequalities. Our proposed algorithms rely on the theory of regular chains and are implemented on top of the

RegularChains

library.

Cylindrical algebraic decomposition (CAD) is a key tool for solving problems in real algebraic geometry and beyond. In recent years a new approach has been developed, where regular chains technology is used to first build a decomposition in complex space. We consider the latest variant of this which builds the complex decomposition incrementally by polynomial and produces CADs on whose cells a sequence of formulae are truth-invariant. Like all CAD algorithms the user must provide a variable ordering which can have a profound impact on the tractability of a problem. We evaluate existing heuristics to help with the choice for this algorithm, suggest improvements and then derive a new heuristic more closely aligned with the mechanics of the new algorithm.

Cylindrical algebraic decomposition (CAD) is an important tool, both for quantifier elimination over the reals and a range of other applications. Traditionally, a CAD is built through a process of projection and lifting to move the problem within Euclidean spaces of changing dimension. Recently, an alternative approach which first decomposes complex space using triangular decomposition before refining to real space has been introduced and implemented within the

RegularChains

Library of

Maple

. We here describe a freely available package

ProjectionCAD

which utilises the routines within the

RegularChains

Library to build CADs by projection and lifting. We detail how the projection and lifting algorithms were modified to allow this, discuss the motivation and survey the functionality of the package.

In their paper Boulier et al. (2009) described the Rosenfeld-Gröbner algorithm for computing a regular decomposition of a radical differential ideal generated by a set of polynomial differential equations, ordinary or with partial derivatives. In order to enhance the efficiency of this algorithm, they proposed their analog of Buchberger’s criteria to avoid useless reductions to zero. For example, they showed that if

p

and

q

are two differential polynomials which are linear, homogeneous, in one differential indeterminate, with constant coefficients and with leaders

θu

and

ϕu

, respectively so that

θ

and

ϕ

are disjoint then the delta-polynomial of

p

and

q

reduces to zero w.r.t. the set {

p

,

q

}. In this paper we generalize this result showing that it remains true if

p

and

q

are products of differential polynomials which are linear, homogeneous, in the same differential indeterminate, with constant coefficients and

θ

and

ϕ

are disjoint where

θu

and

ϕu

are leaders of

p

and

q

, respectively. We have implemented the Rosenfeld-Gröbner algorithm and our refined version on the same platform in

Maple

and compare them via a set of benchmarks.

Traditionally, Groebner bases and cylindrical algebraic decomposition are the fundamental tools of computational algebraic geometry. Recent progress in the theory of regular chains has exhibited efficient algorithms for doing local analysis on algebraic varieties. In this note, we present the implementation of these new ideas within the module

AlgebraicGeometryTools

of the

RegularChains

library. The functionalities of this new module include the computation of the (non-trivial) limit points of the quasi-component of a regular chain. This type of calculation has several applications like computing the Zarisky closure of a constructible set as well as computing tangent cones of space curves, thus providing an alternative to the standard approaches based on Groebner bases and standard bases, respectively. From there, we have derived an algorithm which, under genericity assumptions, computes the intersection multiplicity of a zero-dimensional variety at any of its points. This algorithm relies only on the manipulations of regular chains.

Multivariate Birkhoff rational interpolation is the most general algebraic interpolation scheme. There is few literature on this problem due to the complex structure of the rational function and the non-continuity of the orders of the derivative interpolating conditions. In this paper, by adding the lacking derivative conditions and setting the artificial interpolating values as undetermined parameters, we propose a parametric linearization method to convert the problem of finding a multivariate Birkhoff rational interpolation function into solving a parametric polynomial system in which the coefficients in the numerator and denominator are the unknowns. We use the parametric triangular decomposition to solve the system and prove the solution provides a Birkhoff rational interpolation function as long as there exist proper parameters such that the denominator does not vanish at each interpolating point. The algorithm is implemented in Maple 15.

In this paper we define and discuss the generalized inverse and Moore-Penrose inverse for Ore polynomial matrices. Based on GCD computations and Leverrier-Faddeeva method, some fast algorithms for computing these inverses are constructed, and the corresponding Maple package including quaternion case is developed.

We describe here a properly recent application of the

Gröbner Cover

algorithm (GC) providing an algebraic support to Dynamic Geometry computations of geometrical loci. It provides a complete algebraic solution of locus computation as well as a suitable taxonomy allowing to distinguish the nature of the different components. We included a new algorithm

Locus

into the Singular grobcov.lib library for this purpose. A web prototype has been implemented using it in Geogebra.

We report a preliminary discussion on the usability of the RegularChains library of

Maple

for the automatic computation of plane geometric loci and envelopes in graphical interactive environments. We describe a simple implementation of a recently proposed taxonomy of algebraic loci, and its extension to envelopes of families of curves is also discussed. Furthermore, we sketch how currently unsolvable problems in interactive environments can be approached by using the RegularChains library.

In the authors’ previous work, the concept of comprehensive triangular decomposition of parametric semi-algebraic systems (RCTD for short) was introduced. For a given parametric semi-algebraic system, say S, an RCTD partitions the parametric space into disjoint semi-algebraic sets, above each of which the real solutions of S are described by a finite family of triangular systems. Such a decomposition permits to easily count the number of distinct real solutions depending on different parameter values as well as to conveniently describe the real solutions as continuous functions of the parameters. In this paper, we present the implementation of RCTD in the

RegularChains

library, namely the

RealComprehensiveTriangularize

command. The use of RCTD is illustrated by the stability analysis of several biological systems.

We introduce two quantifier elimination softwares, one is in the domain of an algebraically closed field and another is of a real closed field. Both softwares are based on the computations of comprehensive Gröbner systems.

We introduce various aspects of the design and the implementation of a symbolic/symbolic-numeric computation toolbox, called

SyNRAC

.

SyNRAC

is a package of commands written in the Maple language and the C language. This package indeed provides an environment for dealing with first-order formulas over the reals.

Algebraic local cohomology classes attached to semi-quasiho-mogeneous hypersurface isolated singularities are considered. A new algorithm, that utilizes local cohomology classes with parameter, is proposed to compute Tjurina stratifications associated with

μ

-constant deformations of weighted homogeneous isolated singularities. The proposed algorithm has been implemented in a computer algebra system. Usage of the implementation is also described.

We study an implementation method to compute Boolean Gröbner bases introduced in our previous work [15] in more detail. We extend our method for computing comprehensive Boolean Gröbner bases with a technique introduced in [10]. Our work has been implemented on the computer algebra system Risa/Asir. It enables us to do our recent work of a non-trivial application of Boolean Gröbner bases.

The comprehensive Gröbner systems of parametric polynomial ideal were first introduced by Volker Weispfenning. Since then, many improvements have been made to improve these algorithms to make them useful for different applications. In contract to reduced Groebner bases, which is uniquely determined by the polynomial ideal and the term ordering, however, comprehensive Groebner systems do not have such a good property. Different algorithm may give different results even for a same parametric polynomial ideal. In order to treat this issue, we give a decision method to determine whether two comprehensive Groebner systems are equal. The polynomial ideal membership problem has been solved for the non-parametric case by the classical Groebner bases method, but there is little progress on this problem for the parametric case until now. An algorithm is given for solving this problem through computing comprehensive Groebner systems. What’s more, for two parametric polynomial ideals and a constraint over the parameters defined by a constructible set, an algorithm will be given to decide whether one ideal contains the other under the constraint.

Most of computer algebra systems were designed to have a command line interface. However, the interaction with CAS engine through terminal on tablets is too inefficient. A user have to switch the software keyboard over and over again to complete the input operation. We need a GUI for computer algebra system on tablets. This article describes an implementation method of a handwriting CAS app.

Many students face problems when studying Quantum Mechanics to grasp the stochastic interpretation of the wave functions. In this talk, we show the special solutions of Schrödinger equations, and describe our approach to explain the stochastic interpretation, which is based on these special solutions. We also present some examples of the special solutions, and the teaching materials we developed concerning such solutions, which have been obtained by using a special software called KETpic.

This paper presents a new interactive, user-friendly graphical user interface (GUI) for generation and visualization of IFS. The program, called

IFSGen4LaTeX

, is particularly designed for proper

editing in a WYSIWYG mode. During a working session, IFS are created interactively from scratch and visualized by using the

IFSGen4LaTeX

GUI; simultaneously, its engine generates source code that, once inserted in

and compiled, displays the same fractal images in

Ṫhis process leads to substantial savings in CPU time and memory storage, since the resulting source code is astonishingly small, but still of excellent visual quality because the number of iterations is decided by the user.

GNU

$_{\scriptsize{\rm MACS}}$

is a free mathematical text editor, which can also be used as an interface for several computer algebra systems and other mathematical software, such as Scilab, GNU R, etc. Its primary aim is to offer an alternative to

, which achieves a similar typesetting quality, but also provides a user friendly WYSIWYG interface. This user friendliness makes

$_{\scriptsize{\rm MACS}}$

suitable for a broader audience, such as high school education.

Free-form parametric curves are becoming increasingly popular in many theoretical and applied domains because of their ability to model a wide variety of complex shapes. In real-world applications those shapes are usually given in terms of data points, for which a fitting curve is to be obtained. Unfortunately, this is a very difficult task for classical optimization techniques. Recently, it has been shown that bio-inspired optimization techniques can be successfully applied to overcome this limitation. This paper introduces a new interactive, user-friendly computer software program for the representation and visualization of free-form parametric curves from sets of data points. Given a cloud of data points as initial input, the user is prompted to a graphical interface where he/she can choose the bio-inspired technique of his/her preference, set up the control parameters interactively, and obtain the mathematical representation and graphical visualization of the underlying shape. The paper discusses the main features of this software. An illustrative example of its application is also briefly reported.

In this paper, we will show some of our attempts to verify the effect of using high-quality graphics in collegiate mathematics education through two types of experiments. In the first experiment, we gave a lesson on the law of logarithms usually done without using graphics. We used teaching materials containing graphics to give students some hints. To prepare the graphics, we utilized an extension of TeX capabilities for flexible page layout. Then we estimated the effects of the lesson through a statistical approach. In the second experiment, we detected the change of students’ brain activity by making behavioral observation and neuroimaging simultaneously. For this lesson, we chose the comparison of the degree of growth between two functions as the theme, and prepared some graphs for them. To generate these graphs, we utilized the programmability of the computer algebra system for automatically changing the scale. We showed them to three students and observed their responses. Simultaneously we monitored their brain activities through EEG (ElectroEncephaloGram) measurements. We observed that the judgment of these students changed when they saw a triggering figure, and some change in the trend of the EEG signal was observed at that time. From the results of these experiments, it is indicated that using effective figures in materials might have a great influence on learners’ reasoning processes.

New technologies and interfaces are changing the way users engage with technology, mathematicians are no exception. In a previous study we found some interesting attitudes/practices of professional mathematicians with respect to search interfaces, that sets them apart from other web searchers. In a nutshell, this study explores whether and if so, how math search interfaces are distinctly perceived by younger and older mathematicians and we offer first design implications.

PISA survey research revealed that Japanese high school students have difficulty using mathematics. Responding to those survey results and aiming at improving this situation, the Japanese Ministry of Education, Culture, Sports, Science and Technology created a new subject designated as “Application of Mathematics” in which mathematics is developed with close involvement in culture. The design of the subject “Application of Mathematics” is based on two fundamental pillars: “human activity and mathematics”, and “mathematical considerations for social life”. In this talk, the author wants to add a new perspective: “Application of Mathematics to Mathematics”. Accordingly, the talk will present some examples from WASAN problems of this concept using Computer Algebra Systems (CAS), such as Mathematica, Maple, Maxima, Scilab and R, and TeX documents used as classroom materials through KETpic. The talk encompasses the author’s practice in the teacher-training course and high school classes with CAS. This approach is particularly effective for students in the field of geometry.

We have evaluated the orthant probabilities (i.e., all components are positive) and the upper probabilities of bivariate normal distributions by using Scilab software. The calculated values are presented here in a tabular form. They may be used as a teaching aid material in statistics courses at colleges. We have explained the orthant and upper probabilities using 3D diagrams as a visual aid teaching material in the present work. Moreover, we have evaluated probabilities for more generalized domains by using Scilab software.

In teaching mathematics, there are instances when we need to graphically present mathematical concepts and solid figures to clarify students’ understanding of them. For the last few years, we have been creating graphics that illustrate these various concepts dynamically through careful utilization of KETpic. Examples we will look at include an interactive graphic developed to clearly illustrate the line of intersection of two solid surfaces. In this case, we can easily show the cross-section of the intersection following the cut. A second example is of an interactive graphic produced in order to dynamically present the correspondence relation between the

z

 −plane and

w

 −plane in a complex function

w

 = 

f

(

z

). Here, by using the navigation buttons embedded in the graphic, we can demonstrate how the regions on the

w

 −plane change in relation to the

z

 −plane. Other graphics we have produced will also be introduced.

Mathematical novices – including students in introductory mathematics and statistics service courses – increasingly need to engage in online mathematical collaboration. Using currently-available interfaces for their mobile and touch-enabled devices, however, this group faces difficulties, for those interfaces are text-based and not directly suitable for mathematical communication and collaboration.

To address the deficiency of digital input methods and interfaces for mathematics, we introduce a cross-platform synchronous communication interface for mathematical collaboration. The interface is designed to be intuitive for multiple user groups ranging from novices to experts. We demonstrate that it is possible to create a Web-based communication interface that simultaneously incorporates TeX-, palette- and pen-based input methods, and that is compatible with both touch-enabled tablet and traditional keyboard-mouse user interface principles. The design principles we introduce may be valuable for the design of other mathematical user interfaces on touch-enabled devices, such as with Computer Algebra System interaction.

We present a web-based drill system named DIGITAL-WORK which assists learners in mastering some basic formulae using a new interactive math input method. This method enables users to format any mathematical expression in WYSIWYG by converting from colloquial style strings in fuzzy mathematical notation. The purpose of this study is to investigate whether students can smoothly learn basic math formulae with our drill system. In this paper, we report the results from a field survey that was conducted in an actual remedial math class of 20 junior high school students. The results of our survey showed that 85% of them found this system to be more fun than learning on paper.

KETpic has the capability to create graphic objects which are used in

documents. These features alone make KETpic an ideal portable code language for printing mathematical materials for in-class use or textbooks for publication, and are available at no cost. The latest version of KETpic supports the making of easy-to-use 3D graphs. Recently new commands for generating data in obj format have been introduced in KETpic. The data is easily converted to stl format, making prints of 3D models possible. As a result, a

document with a figure and a 3D model are obtained simultaneously. It is the view of the authors that combining printed materials and 3D models is the preferred mode of approach in math education.

MathEdit is an interactive tool for creating and editing mathematical expressions on the Web. It is an open-source program implemented in standard XHTML and JavaScript to run in regular browsers. The tool supports both WYSIWYG editing and command-line editing operations. Recently, a touch version of MathEdit is under development. In MathEdit touch version, we design a virtual mathematical keyboard for users to enter mathematical symbols and expression templates conveniently. The navigation method of highlighting current node instead of blinking cursor is used in MathEdit. Users can select a sub-expression via a virtual key or touch move operation.

When collegiate mathematics teachers make their original teaching materials, they often use TeX and CAS in order to insert figures and tables into the materials. TeX and CAS have their own programming languages, respectively. Programs must be written in a good style so that other people can read them. KETpic is a plug-in based on CAS to enable teachers to create figures as they like. KETpic has a programming language for drawing but its programming style is not yet established as a good programming style. In this paper we propose the requirements for a good KETpic programming style.

libnormaliz

is a C++ library for computations with rational cones and affine monoids and

CoCoALib/CoCoA-5

offers a general environment for computations in Commutative Algebra. For mutual benefit we have developed a simple and fast interface between the two software libraries.

We present how this integration was designed, and then describe in detail the Normaliz functions we have made available in CoCoALib (and also in CoCoA-5).

We describe in this paper new design techniques used in the

C++

exact linear algebra library

LinBox

, intended to make the library safer and easier to use, while keeping it generic and efficient. First, we review the new simplified structure for containers, based on our

founding scope allocation

model. We explain design choices and their impact on coding: unification of our matrix classes, clearer model for matrices and submatrices,

etc.

Then we present a variation of the

strategy

design pattern that is comprised of a controller–plugin system: the controller (solution) chooses among plug-ins (algorithms) that always call back the controllers for subtasks. We give examples using the solution

mul

. Finally we present a benchmark architecture that serves two purposes: Providing the user with easier ways to produce graphs; Creating a framework for automatically tuning the library and supporting regression testing.

The software Normaliz implements algorithms for rational cones and affine monoids. In this note we present recent developments. They include the support for (unbounded) polyhedra and semi-open cones. Furthermore, we report on improved algorithms and parallelization, which allow us to compute significantly larger examples.

The Basic Polynomial Algebra Subprograms (

BPAS

) provides arithmetic operations (multiplication, division, root isolation, etc.) for univariate and multivariate polynomials over prime fields or with integer coefficients. The code is mainly written in

CilkPlus

[10] targeting multicore processors. The current distribution focuses on dense polynomials and the sparse case is work in progress. A strong emphasis is put on adaptive algorithms as the library aims at supporting a wide variety of situations in terms of problem sizes and available computing resources. One of the purposes of the

BPAS

project is to take advantage of hardware accelerators in the development of polynomial systems solvers. The

BPAS

library is publicly available in source at

www.bpaslib.org

.

We propose an arithmetic of

function intervals

as a basis for convenient rigorous numerical computation. Function intervals can be used as mathematical objects in their own right or as

enclosures

of functions over the reals. We present two areas of application of function interval arithmetic and associated software that implements the arithmetic: (1) Validated ordinary differential equation solving using the AERN library and within the Acumen hybrid system modeling tool. (2) Numerical theorem proving using the PolyPaver prover.

Sparse Matrix Vector multiplication (SpMV) is one of the most important operation for exact sparse linear algebra. A lot of research has been done by the numerical community to provide efficient sparse matrix formats. However, when computing over finite fields, one need to deal with multi-precision values and more complex operations. In order to provide highly efficient SpMV kernel over finite field, we propose a code generation tool that uses heuristics to automatically choose the underlying matrix representation and the corresponding arithmetic.

swMATH is a novel information service for mathematical software. It offers open access to a comprehensive database with information on mathematical software and provides a systematic collection of references and linking to software-relevant mathematical publications.

MathLibre is a project to archive open source mathematical software and documents and offer them with a Live Linux. Anyone can build modified and localized version of MathLibre, very easily.

We present software packages for the holonomic gradient method (HGM). These packages compute normalizing constants and the probabilities of some regions. While many algorithms which compute integrals over high-dimensional regions utilize the Monte-Carlo method, our HGM utilizes algorithms for solving ordinary differential equations such as the Runge-Kutta-Fehlberg method. As a result, our HGM can evaluate many integrals with a high degree of accuracy and moderate computational time. The source code of our packages is distributed on our web page [12].

There are several different libraries with code for mathematical functions such as exp, log, sin, cos, etc. They provide only one implementation for each function. As there is a link between accuracy and performance, that approach is not optimal. Sometimes there is a need to rewrite a function’s implementation with the respect to a particular specification.

In this paper we present a code generator for parametrized implementations of mathematical functions. We discuss the benefits of code generation for mathematical libraries and present how to implement mathematical functions. We also explain how the mathematical functions are usually implemented and generalize this idea for the case of arbitrary function with implementation parameters.

Our code generator produces C code for parametrized functions within a known scheme: range reduction (domain splitting), polynomial approximation and reconstruction. This approach can be expanded to generate code for black-box functions, e.g. defined only by differential equations.

Using mathematics within computer software almost always includes the necessity to compute with real (or complex) numbers. However, implementations often just use the 64-bit double precision data type. This may lead to serious stability problems even for mathematically correct algorithms. There are many ways to reduce these software-induced stability problems, for example quadruple or multiple-precision data types, interval arithmetic, or even symbolic computation. We propagate

Exact Real Arithmetic

(ERA) as a both convenient and practically efficient framework for rigorous numerical algorithms.

CUMODP is a CUDA library for exact computations with dense polynomials over finite fields. A variety of operations like multiplication, division, computation of subresultants, multi-point evaluation, interpolation and many others are provided. These routines are primarily designed to offer GPU support to polynomial system solvers and a bivariate system solver is part of the library. Algorithms combine FFT-based and plain arithmetic, while the implementation strategy emphasizes reducing parallelism overheads and optimizing hardware usage.