TSSC 2025

Recent Advance on Rational Surface Implicitization using Moving Surfaces

陈发来

中国科学技术大学

摘要: Rational surface implicitization is a fundamental problem in Computer Aided Geometric Design, and it has wide applications in surface/surface intersection, surface singularity computation, point inversion, etc. In this talk, I will present the latest development of the method of moving surfaces in implicitizing rational surfaces. Future research problems are also discussed.

Reductions in symbolic integration

陈绍示

中国科学院数学与系统科学研究院

摘要: Symbolic integration is a classic and core topic in symbolic computation. In 1969, Risch presented a complete algorithm for determining whether an elementary function is elementary integrable or not. When an elementary function is not integrable, the reduction algorithm can refine the output of the Risch algorithm, that is, it can decompose the integrand into an integrable part and a minimal remainder part. In the previous decade, the combination of the reduction algorithms and Zeilberger's method of Creative Telescoping has significantly improved the efficiency of symbolic integration and summation. In this talk, we will overview the reduction algorithms and their applications, including the cases of rational functions, hyperexponential functions, algebraic functions, D-finite functions, and elementary functions in certain logarithmic and hyperexponential extensions.

TBA

冯如勇

中国科学院数学与系统科学研究院

摘要: abstract_fengry.pdf

符号计算与Pi级数

侯庆虎

天津大学

摘要: 我们将介绍利用符号计算方法，推导和证明若干涉及Pi的级数恒等式。包括利用Gosper表示和约化算法构造Pi级数恒等式，利用符号求导证明Pi级数恒等式，以及构造WZ对证明Pi级数恒等式。

TBA

雷娜

大连理工大学

摘要: TBA.

Hermite Ring Conjecture on polynomial rings over Valuation Rings

李冬梅

湖南科技大学

摘要: Serre's conjecture, proposed by J.P. Serre in 1955, asserts that finitely generated projective modules over polynomial rings with finitely many variables over a field, are free. Quillen and Suslin independently gave an affirmative answer to this famous conjecture via completely different approaches in January of 1976. Hermite ring Conjecture is an extension of Serre's conjecture. In this talk, we mainly investigate Hermite Ring Conjecture on polynomial rings over Valuation Rings. We obtain an analogy of a theorem of Lequain-Simis. Based on this theorem, we can prove that a unimodular row v in the polynomial ring over Valuation Rings can be transformed into v(0, …, 0) by elementary transformations. Then we state that the Hermite ring conjecture holds on polynomial rings over Valuation Rings.

The Geometry of Monomials and Null Binomials in Conformal Geometric Algebra

李洪波

中国科学院数学与系统科学研究院

摘要: Conformal Geometric Algebra is a geometric algebraic language for describing and manipulating objects and transformations in conformal geometry, and has found important applications in Geometric reasoning, computer graphics and robotics. The term "Geometric Algebra" indicates that basic algebraic entities such as monomials and their multiplications in this algebra have clear geometric interpretation in conformal geometry. This talk addresses the geometric meaning of monomials and null binomials in conformal geometric algebra. A talk on similar topics was first given in the conference AGACSE 2024, with slides and video available at
https://staff.science.uva.nl/l.dorst/AGACSE2024/SLIDES/Li_slides.pdf
https://staff.science.uva.nl/l.dorst/AGACSE2024/VIDEO/Li.mp4

Motion Polynomials Admitting a Factorization with Linear Factors

李子佳

中国科学院数学与系统科学研究院

摘要: Motion polynomials (polynomials over the dual quaternions with nonzero real norm) describe rational motions. In this talk, we will present a necessary and sufficient condition for reduced bounded motion polynomials to admit factorizations into monic linear factors, and we give an algorithm to compute them. We can use those linear factors to construct mechanisms because the factorization corresponds to the decomposition of the rational motion into simple rotations or translations. Bounded motion polynomials always admit a factorization into linear factors after multiplying with a suitable real or quaternion polynomial. Our criterion for factorizability allows us to improve on earlier algorithms to compute a suitable real or quaternion polynomial co-factor.

基于可达集上下近似的混成系统安全性验证研究

佘志坤

北京航空航天大学

摘要: 信息-物理系统（CPS）是一种将计算与物理过程相结合的系统，是多学科交叉融合的产物。混成系统作为一类将离散事件系统和微分方程相结合的动力系统，被认为是研究信息-物理系统的一个非常有效的数学模型。由于混成系统安全性验证是一不可判定问题，本报告将主要围绕动力系统可达集的上下近似展开：首先，引入演化函数并借助李导数给出它的泰勒级数展开；接着，基于部分和公式，提出两种计算可达集上下近似的方法并给予实现；最后，与最近几种可达集上下近似方法的计算结果比较展示了我们方法的优越性。

TBA

孙瑶

中国科学院信息工程研究所

摘要: TBA.

Completing Parametric Unimodular Rows to Unimodular Matrices

王定康

中国科学院数学与系统科学研究院

摘要: abstract_wangdk.pdf

计算代数理论和应用

王明生

中国科学院信息工程研究所

摘要: 回顾计算代数的经典问题和目前发展现状！同时给出一些有重要研究价值的计算问题。

Computing the greatest common divisor of several parametric univariate polynomials via generalized subresultants

杨静

广西民族大学

摘要: abstract_yangj.pdf

面向组合恒等式的定理自动生成和证明

杨争峰

华东师范大学

摘要: 自动化定理证明（ATP）传统上依赖于证明搜索，近年来，随着大语言模型的快速发展，AI赋能的定理自动证明已成为一种新范式。然而，由于现有证明数据的匮乏，基于人工智能的定理自动证明仍面临诸多挑战。针对组合恒等式定理自动证明问题，我们提出了一种结合大语言模型与强化学习的定理自动生成方法；通过融合人工形式化与定理自动生成，我们开发了一个基于Lean的组合恒等式形式化数据集LeanComb，及其相应的定理自动证明器；实验结果表明，针对组合恒等式的定理自动证明问题，我们开发的证明器在准确率上优于现有的证明器，且提出的定理自动生成方法显著提高了自动证明的效率和准确率。