SSSC 2017

    For a bi-parametric real polynomial system with parameter values restricted to a finite rectangular region, under certain assumptions, we introduce the notion of border curve, which divides its complement in the rectangular region into connected subsets such that above them the real zero set of the system defines finitely many smooth functions with disjoint graphs. We propose a numerical method to compute the border curve, and provide a numerical error estimation. The border curve enables us to solve a parametric system efficiently by first constructing a so-called “solution map” off-line and then tracking a real homotopy on-line.
    As an application of this method, we show that for a biological system modeled by a continuous dynamical system defined by rational functions with two parameters, we can numerically compute the complete fold and Hopf bifurcation boundaries of the system restricted in a finite region in the parametric space. The bistability properties of several biological systems are successfully analyzed by our method.
    To relax some of the assumptions when computing the real witness points, we introduce the notion of full rank representation of a real algebraic set and present a proof-of-concept hybrid algorithm to compute it based on symbolic triangular decomposition approach and numerical critical point technique.
    This is a joint work with Wenyuan Wu and Yong Feng.

     计算机程序中的许多性质和常见错误（如除零错、数组越界、整数上溢、浮点上溢等），与程序中数值型变量及其上的数值运算密切相关。针对数值代码开展自动分析，检测数值相关错误，对于提高计算机软件（尤其是数值计算密集型安全攸关软件）的可信性具有重要意义。本报告将从数值相关程序错误的检测出发，介绍基于抽象解释的数值程序分析方法（包括抽象解释理论、数值抽象域、数值不变式的自动生成等），讨论基于符号计算与基于数值计算的程序分析算法的实现技术，及其面临的问题和挑战。

    The method of creative telescoping is the core of Wilf--Zeilberger's theory for computer-generated proofs of identities in combinatorics and special functions. The key concept in this method is TeLescoper, which is a linear differential or recurrence operator. For a specific function, when does a telescoper of certain type exist? And how can one construct telescopers? These are two basic problems related to the method of creative telescoping. In this talk, I will given a survey on recent work on these two problems.

    Automatic computation of surface symmetry is an active research field in computer vision, computer graphics and computational geometry. It discovers the intrinsic global features of the shapes, and can be applied for shape comparison, geometric database searching and surface registration directly.
   Surface symmetry is represented as the group of the automorphisms, which preserve special geometric properties of the shape. Extrinsic symmetry group is a subgroup of the Euclidean rigid motion constrained on the surface, and intrinsic symmetry group consists of all isometric automorphisms. Similarly, conformal symmetry group relaxes the requirement for isometries to conformal automorphisms, namely the angle-preserving diffeomorphisms. Extrinsic symmetry group is a subgroup of intrinsic symmetry group, which, in turn, is a subgroup of conformal symmetry group.
    Although numerous studies have been devoted to compute extrinsic and intrinsic symmetry groups of general surfaces, conformal symmetry group has not been systematically studied in computer vision field. This work proposes a systematic framework to compute conformal symmetry group based on Ricci flow and Riemann surface theory. The method gives the conformal symmetry for genus zero, genus one and two surfaces. We employ our algorithm for geometric database searching and registration for surfaces with complicated topologies. Experimental results demonstrate the efficiency and efficacy of our proposed method.

    Groebner基是符号计算中的重要概念. Groebner基具有良好的性质并有着广泛的应用. Groebner基方法是代数方程组求解最重要的方法之一, 同时还可以应用于解决理想成员判定问题, 消元理想计算问题, 几何定理的机器证明等等. 然而, Groebner基的计算复杂度一直限制着Groebner基的广泛应用. 在本次报告中, 我们将重点介绍几种主流的Groebner基计算算法, 帮助同学深入理解Groebner基的本质特性. 同时还会介绍Groebner基的一些重要应用.

    本报告的内容基于陈肖宇、宋丹和报告人共同完成的工作. 我们介绍一个从几何图形的电子图片中自动发现几何定理的算法框架. 该框架包括下列主要步骤：
    1. 给出选定几何领域的形式化规约和语义表示；
    2. 使用形状识别技术、数值验证方法以及几何概念的形式化定义，从图像中提取、生成有意义、可理解的几何特征信息；
    3. 引进特定的策略去除平凡的几何信息，并根据归纳原理生成候选几何命题；
    4. 调用几何定理证明器证明或者否定候选命题, 被证明的命题即为发现的定理.
    以欧氏平面几何为例, 我们具体设计、实施了上述框架中的算法，并使用工具与手工绘制、扫描、拍照等不同方式生成的几何图片测试了所提出的定理发现方法. 结果表明，这一方法行之有效，可以用来发现大量非平凡的几何定理.