next day
all days

View: session overviewtalk overview

10:00-10:50 Session 2: SYNASC Invited Talk (1)
Computation models in e-origami system Eos

ABSTRACT. We discuss the computation models incorporated in Eos. Suppose that we practice origami with a square sheet of paper to create a shape of interest. Furthermore, we also want to consider origami as a process of creation in the era of digital transformation (often coined as DX). That is to say; we interact with a computer to create the intended shape in the computer’s memory and visualize it on the computer’s screen.

The advantages of this approach are improved precision, provability of properties of the created structures, fine-tuning of shapes, and deference to other kinds of DX processes such as 3D printing. This approach leads us to the notion of computational origami discipline. Eos is a software tool for studying computational origami.

We discuss the mechanism of Eos. Although we introduced Eos as a software tool, it is by no means a mere collection of independent software modules. Eos is an engine of geometric processing focusing on origami. It performs a streamlined and verifiable creation of origami and contains a geometric reasoner of origami.

We realize the engine and the reasoner using several computation models that communicate by common structures.

We explain these computation models and their functionality by several origami examples. We take samples from geometric origami and classical origami.

11:10-11:50 Session 3: Theory of Computing Session
Towards the Complexity of Petri Nets and One Counter Machines via Coordinated Table Selective Substitution Systems

ABSTRACT. We investigate computational resources used by Turing machines (TMs) and alternating Turing machines (ATMs) to accept languages generated by coordinated table selective substitution systems with two components. We prove that the class of languages generated by real-time (RL; 0S)-systems, an alternative device to generate lambda-free labeled marked Petri nets languages, can be accepted by nondeterministic TMs in O(log n) space and O(nlog n) time. Consequently, this proper sub-class of Petri nets languages (known also as L-languages) is included in NSPACE(log n). The class of languages generated by (RL; RB)-systems for which the nonterminal alphabet of the RL-grammar is composed of only one symbol and the nonterminal alphabet of the RB-grammar is composed of two symbols, can be accepted by ATMs in O(log n) time and space. Consequently, this proper subclass of one-counter languages generated by one-counter machines with only one control state is included in U_E*-uniform NC1, hence in SPACE(log n).

Graphs hard-to-process for greedy algorithm MIN

ABSTRACT. We compare results of selected algorithms that approximate the independence number in terms of the quality of constructed solutions. Furthermore, we establish smallest hard-to-process graphs for the greedy algorithm Min.

11:50-12:30 Session 4: Symbolic Computation Session (1)
Proposal of Multivariate Polynomial Arithmetic in a Specified Width of High- or Low-Exponents
PRESENTER: Tateaki Sasaki

ABSTRACT. The truncated power-series is very useful in computer algebra, however we must control the cutoff degree very carefully when we use the power-series in actual algorithms. In this paper, we propose a much more useful multivariate polynomial arithmetic. The arithmetic reserves only the terms of high- or low-exponents in a user-specified width w.r.t. a specified variable (other terms are discarded automatically). Of course, the exponents are determined by the conventional arithmetic hence change as the computation proceeds, while the width (measured from either the highest or the lowest exponent) is fixed.

Digital Collections of Examples in Mathematical Sciences

ABSTRACT. Some aspects of Computer Algebra (notably Computation Group Theory and Computational Number Theory) have some good databases of examples, typically of the form "all the X up to size n". But most of the others, especially on the polynomial side, are lacking such, despite the utility they have demonstrated in the related fields of SAT and SMT solving. We claim that the field would be enhanced by such commuity-maintained databases, rather than each author hand-selecting a few, which are often too large or error-prone to print. NB: the full paper has been submitted elsewhere, so if accepted this would only be an abstract for the proceedings.

14:00-14:50 Session 5: SYNASC Invited Talk (2)
Mechanization of mathematics: some examples for discussion

ABSTRACT. “None of my inventions came by accident. I see a worthwhile need to be met and I make trial after trial until it comes. What it boils down to is one percent inspiration and ninety-nine percent perspiration.”

Owing to computers it increasingly has become possible to automate the perspiration phase in Edison’s statement. Recent AI developments stimulated renewed interest in the question of how far non-routine parts of mathematical work can be automated.

In this talk we present concrete examples of non-trivial applications of RISC computer algebra algorithms in enumerative combinatorics, special functions, and number theory. Related aspects of mechanization of mathematics are left for discussion.

15:10-16:00 Session 6: SYNASC Invited Talk (3)
Questioning the Assumptions Behind Symbolic Computation Systems

ABSTRACT. Software systems for symbolic computation are large-scale and complex, built on software stacks that span the gamut from machine instruction selection to web interface technology. Systems such as Maple, Mathematica and Reduce have code bases whose development can be measured in terms of person-centuries so, understandably, no-one is eager to rewrite such systems in their entirety. At the same time, these code bases have essential components that have not been significantly updated in decades. Many of the assumptions in their design are based on system characteristics that are no longer germane.

For example, memory characteristics and multiprocessing capabilities have changed significantly. Likewise, programming languages such as Rust, C++20, Julia and Typescript allow coding styles that were not possible when the large computer algebra systems were initiated. In this talk, we examine the assumptions behind the underlying layers of the computer algebra software stack, namely those of memory management and integer arithmetic. We explore the design space available today, and which choices might have the most impact in updating software systems.

16:20-18:00 Session 7A: Symbolic Computation Session (2)
On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving
PRESENTER: Gereon Kremer

ABSTRACT. We recently presented cylindrical algebraic coverings: a method based on the theory of cylindrical algebraic decomposition and suited for nonlinear real arithmetic theory reasoning in Satisfiability Modulo Theories solvers. We now present a more careful implementation within cvc5, discuss some implementation details, and highlight practical benefits compared to previous approaches, i.e., NLSAT and incremental CAD. We show how this new implementation simplifies proof generation for nonlinear real arithmetic problems in cvc5 and announce some very encouraging experimental results that position cvc5 at the very front of currently available SMT solvers for QF_NRA.

Implementing arithmetic over algebraic numbers: A tutorial for Lazard's lifting scheme in CAD
PRESENTER: Gereon Kremer

ABSTRACT. Implementing techniques from computer algebra often requires a multitude of foundational algorithms that are neither easy to understand nor to implement. Despite great interest, the difficulty to implement novel techniques from computer algebra proves to be a significant hindrance, especially, when a modern computer algebra system cannot be used. We tackle cylindrical algebraic decomposition (CAD) as one such example. CAD can be, for example, applied in satisfiability modulo theories solving for nonlinear real arithmetic. However, a recent advance in CAD, the Lazard’s lifting scheme, requires additional algebraic techniques that are neither available in these solvers, nor as stand-alone libraries. We close this gap by showing how to use the CoCoALib library to implement Lazard's lifting scheme outside of a modern computer algebra system like Maple.

Tree $T$ and Lambert $W$

ABSTRACT. The paper discusses the two cognate functions Tree $T$ and Lambert $W$. The definition of the Lambert $W$ function in the complex plane, specifically the branch structure, has been the subject of varying opinions from the time W was named. These opinions are reviewed. Until now, the cognate functions have been regarded as simple reflections of each other. Here I propose that the two functions be given independent branch structures, thus allowing users of computer algebra systems access to whichever structure is convenient for them.

Parametric Linear Algebra in Maple (Work in progress paper)

ABSTRACT. Parametric Linear Algebra refers to the analysis of matrices containing elements which are symbolic. Properties such as the rank of the matrix can change depending upon possible values later assigned to the symbols. This is an example of the specialization problem. We discuss approaches to this problem and describe a package in Maple that is being developed to handle symbolic coefficients.

Resultant-based Elimination for Skew Polynomials

ABSTRACT. We propose resultant based methods for elimination of indeterminates of skew polynomial systems. We start with defining the concept of resultant for bivariate skew polynomials by Dieudonné determinant, and then applying a modular technique to improve the efficiency of the method. We also consider the almost commutative case where the resultant becomes well defined.

16:20-18:20 Session 7B: PhD Students Session
Analysis of the Influence of Bound Constraint Handling Strategies on the Search Direction in Differential Evolution Algorithms

ABSTRACT. The aim of this paper is to analyze the influence of the boundary constraints handling methods (BHCM) on the search direction in the case of Differential Evolution (DE) optimization algorithms. An experimental analysis for 8 correction methods was conducted, its main aim being the comparison between cosine similarities corresponding to the search direction computed before the application of BHCM and the search direction computed after the application of BHCM. The results of the analysis provides information about how much of the initial search direction is conserved by applying a correction method. Some preliminary theoretical results are also presented.

Mapping the black pine trees using the integration of CNN and OBIA

ABSTRACT. Mapping forest is essential for forest sustainability and management to model species distribution. Black pine is a world - wide species, originally from Mediterranean Region and Asia Minor. Its presence northern of Danube still remains a curiosity for many researchers. Thus, main objective is to model this species distribution. The methodology consists of integrating convolutional neural network model (CNN) with object-based image analysis classification method. Data used are a high resolution Sentinel-2 image, trained and model within the CNN. The preliminary results of the convolutional neural network model were used as input for the object-based image analysis classification method. The object-based accuracy assessment approach shown an an overall accuracy more than 80%. We conclude that combining the CNN model with OBIA can be considered an efficient approach for mapping the black pine trees. Nevertheless, the model can be improved by using very high resolution image.

Preceptor: A Proposed Architecture for an On-Demand Virtual Learning Platform

ABSTRACT. In the present paper, we propose a methodology for ensuring on-demand individualized job training to a learner via a virtual organization (VO). We offer suggestions for the development of a platform supporting the lifecycle of such a job training VO. The proposed methodology addresses three stages in assisting the learner: (1) helping the learner identify his/her personalized learning path (in terms of curricular requirements, or competences) for a specific job, (2) searching for the Pareto optimal combinations of instructors to cover the identified competences, and (3) building a VO as a holonic multi-agent system (HMAS) composed of candidate resources, in an attempt to partially bridge the gap between VOs and VO environments.

On some qualitative properties of Ciric fixed point theorem

ABSTRACT. In this paper, we will present some results related to Ciric operator in complete metric spaces. Existence and uniqueness are recalled and several stability properties (data dependence and Ostrowski stability property) are proved. Using the retraction-displacement condition, we will establish the well-posedness and Ulam-Hyers stability of the fixed point equation, x = f(x).

Splitting Proximal Algorithms for Convex Optimization Problems on $\CAT(\kappa)$ spaces and Its Applications

ABSTRACT. In this paper, we consider a splitting method combined with proximal methods for minimizing the sum of convex functions, where the proximal operators are defined by the curvature-adapted regularizations. In this paper, using properties of the resolvent on complete CAT$(\kappa)$ space, we present the theorems showing strong convergence of the splitting proximal algorithm under the local compactness property on the ambient space. Finally, we also apply our main results to solve convex feasibility problems, centroid problems, and particularly the Karcher means.

Local fixed point results and applications for multivalued generalized contractions

ABSTRACT. This paper presents some local fixed point theorems related to Ciric-Reich-Rus, Chatterjea and Berinde types of multivalued generalized contractions. Additionally, as an application to this type of result we will introduce the multivalued open mapping theorem for each of the three specified multivalued contractions.