数学机械化自动推理平台

简 介

数学机械化的发展离不开计算机,数学机械化理论的应用更需要计算机软件的支撑。数学机械化二十余年的研究,在理论和方法上取得了创造性的发展,但在软件实现上虽然有一些成功的软件,还没有一个基于我们自己理论的,真正独立的通用软件平台。这在很大程度上影响了数学机械化理论研究特别是应用的进一步发展。数学机械化自动推理平台MMP的开发就是为了改变这一状况进行的。

MMP主要以符号计算为支撑,以我国开创的数学机械化算法为核心,以国家“973”项目“数学机械化与自动推理平台”的理论研究与应用研究成果为依托,在较成熟的分支如几何推理、方程求解、曲面造型、机器人等方面研制相应的自动推理模块,为科学研究、工程应用、教学提供一个应用数学机械化的理论与方法的强有力的软件工作平台和开发平台。

MMP主要由以下四部分组成。

l        支撑部分。这一部分是整个系统的基础。包括图形界面,支撑数据结构,内存回收。可编程语言解释环境。

l        基本运算。这一部分提供基本得符号与数值运算。包括无穷精度数的运算,多项式的运算,线性代数,基本数值计算。

l        核心部分。我们实现了代数、常微、偏微情形的吴零点分解定理与投影定理,首次完整与高效地实现了数学机械化方法。

l        应用模块。包括

1.      MMP/Geometer:几何自动推理

2.      MMP/Realroot:实根判定与不等式证明

3.      MMP/Soliton: 微分方程孤立子求解

4.      MMP/Identity: 组合恒等式证明

5.      MMP/Blending: 自动生成过渡曲面

6.      MMP/Robot: 机器人模拟

7.      MMP/Linkage: 四连杆综合与模拟模块

其中MMP/Geometer、MMP/Blending、MMP/Robot、MMP/Linkage具有独立界面。

MMP的是以国家“973”项目“数学机械化与自动推理平台”软件开发课题组为主开发,应用模块还邀请了其他课题的成员参加。在此对所有参加人表示诚挚感谢。国家科技部以及项目的挂靠单位中科学院与国家基金委对于数学机械化研究与软件开发给予了长期大力支持与鼓励。数学机械化的发展与这些支持是密不可分的。

欢迎对此软件提出宝贵的建议。问题请寄: mmsoft@mmrc.iss.ac.cn.