数学机械化与自动推理平台

Mathematics Mechanization and Automated Reasoning Platform

数学机械化就是将数学研究的主要活动——“推理与计算”实现机械化或自动化的过程。本项目研究数学机械化基础理论、信息技术若干关键问题的应用、自动推理平台开发。在微分方程求解、不等式自动证明、全局优化、组合恒定式自动证明、Clifford代数计算、几何自动作图与智能CAD、信息压缩、图像伪装、基于Stewart平台的数控技术、CAGD等方面取得一批重要成果。在软件方面,开发出有自主版权的智能软件。在图像压缩方面,提出的“多成分变换”技术为JPEG2000图像压缩国际标准所采纳。

Mathematics mechanization (MM) is the effort to mechanize or automate the main mental labor in the field of mathematics: reasoning and computation. Mathematics is the theoretical foundation for science and technology. Its mechanization will have great impact on scientific research and technology innovation. We have made major advance in the theory and method for differential and algebraic equation solving and automated reasoning in proving inequalities, combinatorial identity proving, Clifford algebra computation, and engineering design generation. The project also made essential progress in applying the MM methods to information technology, including image compression, image hiding, solid modeling, and intelligent CAD, and virtual NC machine based on Stewart platform. The 'Reversible Integer Mapping' method was adopted by the JPEG2000 standard. We developed a platform of automated reasoning based on the MM theories, which may be used to aid researchers and engineers in many aspects of reasoning and computation.