大会特邀报告:


青年学者邀请报告:

  • 甘庭(武汉大学)
    题目:Nonlinear Craig Interpolant Generation
    摘要:Interpolation-based techniques have become popularized in recent years because of their inherently modular and local reasoning, which can scale up existing formal verification techniques like theorem proving, modelchecking,abstraction interpretation, and so on, while the scalability is the bottleneck of these techniques. Craig interpolant generation plays a central role in interpolation-based techniques, and therefore has drawn increasing attentions. In the literature, there are various works done on how to automatically synthesize interpolants for decidable fragments of first-order logic, linear arithmetic, array logic, equality logic with uninterpreted functions(EUF), etc., and their combinations. But Craig interpolant generation for non-linear theory and its combination with the aforementioned theories are still in infancy, although some attempts have been done. We proven that a polynomial interpolant of the form $h(x)>0$ exists for two mutually contradictory polynomial formulas $\varphi(x, y)$ and $\psi(x, z)$, with the form $\wedge_i f_i \ge 0$ , where $f_i$ are polynomials in $x, y$ or $x, z$, and the quadratic module generated by $f_i$ is Archimedean. Then it is shown that such interpolant can be computed efficiently through solving a semi-definite programming problem (SDP).

  • 贾晓红(中国科学院数学与系统科学研究院)
    题目:How Algebra Is Used in Collision Detections
    摘要:Collision detection is a key step of many advanced industry environments such as Virtual Reality, Robotics and CNC machining, where exact and efficient collision detection algorithms are highly appreciated. Collision Detection contains two main parts: the algorithm design for the dynamic layer and relative position decision for in the static stage.
      Traditional research is mainly based on the determination of the relative position or more precisely, morphology of the intersection curve, of two geometry objects, which only indicate the relationship, but neglect the asymmetry between two different objects. Configuration analysis reveals this asymmetry. In many practical environments, interchanging the two objects can lead to qualitative change of the environment, hence providing the concrete geometric or topological behavior of each object is more important.
      We shall re-explore the collision detection problem through configuration analysis by establishing classifications, enumeration and algebraic determination law of two static bounding volumes;. We also construct connection graph for all possible configurations and provide a symbolic algorithm of computing the configuration variations of two moving objects.

  • 李念(湖北大学)
    题目:Recent Results on the Cross Correlation of $m$-Sequences
    摘要:Pseudorandom sequences have significant applications in communication systems, coding theory and cryptography. Maximum length linear feedback shift register sequences (also called $m$-sequences) are popular in sequence design due to their excellent properties. In this talk, we will focus on the cross correlation between an $m$-sequence and its decimation sequence. We will introduce our newly found technique in solving equations over finite fields and its application in solving two open problems, proposed by Niho in 1972 and by Dobbertin, Helleseth and Martinsen in 1999 respectively by estabishing a surprising connection between a combinatorial counting problem and the Zetterberg code.

  • 牟晨琪(北京航空航天大学)
    题目:Chordal Graphs in Triangular Decomposition in Top-Down Style
    摘要:In this talk we present some underlying connections between symbolic computation and graph theory. Inspired by the two papers of Cifuentes and Parrilo in 2016 and 2017, we are interested in the chordal graph structures of polynomial sets appearing in triangular decomposition in top-down style. Viewing triangular decomposition in top-down style as multivariate generalization of Gaussian elimination, we show that the associated graph of one specific triangular set computed in any algorithm for triangular decomposition in top-down style is a subgraph of the chordal graph of the input polynomial set and that all the polynomial sets, including all the computed triangular sets, appearing in one specific algorithm for triangular decomposition in top-down style (Wang’s method) have associated graphs which are subgraphs of the chordal graph of the input polynomial set. Potential applications of chordal graphs in symbolic computation are also discussed.

  • 吴文渊(中国科学院重庆绿色智能技术研究院)
    题目:Global Error Estimation for Linear ODE and its Optimal Solution
    摘要:Solving Linear Ordinary Differential Equations (ODEs) plays an important role in many applications. There are various numerical methods and solvers to obtain approximate solutions typically represented by points. However, few work about estimation of global error can be found in the literatures. In this talk, we first use Hermite cubic spline interpolation at mesh points to represent the solution, then we define the backward error obtained by substituting the interpolation solution back to ODEs. Then the global error between the exact solution and an approximate solution can be bounded by using the backward error. Moreover, solving ODEs can be transformed to an optimization problem of backward error in certain solution space which can be solved by conjugate gradient method with taking advantages of sparsity of the corresponding matrix. The examples in the talk show that our estimation works well for linear ODEs' models and the refinement can find solutions with smaller global errors than traditional methods in Matlab without additional mesh points.

  • 徐岗(杭州电子科技大学)
    题目:Hexahedral Mesh Subdivision and Simplification for Isogeometric Analysis
    摘要: With the requirement of high-precision numerical simulation in intelligent manufacturing, the generation and processing of hexahedral mesh has become a hot issue recently in the field of geometric computing and isogeometric analysis. This talk will introduce our research progress on hexahedral mesh subdivision and simplification. In the first part, the limit point formula of Catmull-Clark volume subdivision will be introduced for all the cases of singular vertex. Based on the proposed formula, the applications on the interpolating volume subdivision and parametric volume approximation of subdivision solid are also given. In the second part, an improved simplification algorithm for singularity structure in hex-mesh is introduced. Starting from an initial hexahedral mesh, the proposed approach can obtain a hexahedral mesh with a much simpler singularity structure while maintaining approximation accuracy.

  • 叶科(中国科学院数学与系统科学研究院)
    题目:Tensor Ranks with Applications to Complexity Theory
    摘要:This talk consists of two parts. In the first part, I will review various notions of tensor ranks and present some of our new results on these ranks. In the second part, I will first discuss the connection between tensor ranks and the computational complexity theory. In particular, I will concentrate on the complexity of the matrix-vector/matrix-matrix multiplication. If time permits, I will exhibit some numerical algorithms for small size matrix multiplication obtained by this method.