数学机械化自动推理平台

数学机械化自动推理平台

原作者	中国科学院数学机械化重点实验室
開發者	中國 国家基础研究发展规划项目 "数学机械化与自动推理平台" 软件开发课题组
穩定版本	3.0/ 2006年4月1日 (2006-04-01)
網站	MMP - 数学机械化自动推理平台

数学机械化自动推理平台（英语：Mathematics Mechanization and Automated Reasoning Platform），又名 Mathematics-Mechanization Platform（简称 MMP，开发代号：elimino）是中国科学院数学机械化重点实验室根据吴文俊院士数学机械化理论为基础发展出来的数学机械化自动推理平台。最新版本为 3.0，内部版本 elimino 1.0。

运行环境

微软Windows 2000, XP, Vista.

核心功能

包括符合计算，多项式运算，符号线性代数，多项式方程，多元方程组，常微分方程系统，偏微分方程系统的吴特征列方法，几何问题的自动求解等。

数系

整数任意大。小数30位数，可以扩充到任意长度。

基本运算

(X^660-1)的因子分解

数字与多项式的四则运算。

• 3*4；

12

• expand((x+35)*(y-4)*(5*z-3/4));

5zyz-$\tfrac{3}{4}yx$-20zy+3x+175zy-$\tfrac{105}{4}$-700z+ 105;

• quo(x^2+4*x+4,x+2);

x+2; (x^2+4*x+4)/(x+2)=x+2;

或

expand((x^2+4*x+4)/(x+2)); x+2

p:=$x^3+y^3+z^3-3*x*y*z$

q:=x+y+z;

r:=quo(p,q);

$x^2+y^2+z^2-x*y-x*z-y*z$

q*r;

$x^3+y^3+z^3-3*x*y*z$

开平方

• nsqrt(3.)

1.73205080756887729352744634151

• nsqrt(3333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333334444444444444444444444444444444444444444444444444444444444444555555555555555555555555555555555555566666666666666666777777777777777);

• expand(sqrt(x^2+6*x+9));

X+3

开立方

• expand(curt(27));

3

• expand(curt(x^3+3*x^2+3*x+1));

x+1

因子

• ifactor(6)

[2,1,3,1], (2^1*3^1)

• ifactor(16)

[2,4] (2^4)

• ifactor(99);

[3,2,11,1], ( 3^2 *11^1);

• ifactor(123456789);

[3,2,3607,1,3803,1]

• ifactor(987654321);

[3,2,17,2,379721,1]

• ifactor(3333333333333333333666);

[2，1，3，1，13，1，83，1，2616941，1，196748812049，1]

• factor($18x^6+30x^5-231x^4-259x^3+210x^2-1617x-2695$)

[[1],1,[6x^2-77],1,[x^3+7],1,[3x+5],1]

factor(x^660-1)

最大公约数

• • gcd(66，88)；

22

• • gcd(x^3+3*x^2+3*x+1,x+1);

x+1

模数

• • imod(35，6)；

5

中国余数定理

• chrem([3,5,7],[2,3,2]);

23

• chrem([5,7,11],[2,1,10]);

197

• chrem([5,7],[2,1]);

22

• chrem([5,11],[2,10]);

32

• chrem([1,3,5,7,11,13,17,19,23],[1,2,3,4,5,6,7,8,9]);

77131268

多项式方程求解

polysover(x^100-9999) 的复数解

• p:=x^2+5*x+6;

polysolver(p);

[-2,-3]

• p:=29*x^11+21*x^8-77;

polysolver(p) 可以求出11项复数解。

Mrealroot([p],[x],1/100000000) 可得出一个实数解，位于

$\frac{17533885}{16777216}$，$\frac{140271081}{134217728}$ 区间之内；实数解可取为平均值即：

$x=\frac{280542161}{268435456}$

• 秦九韶 《数书九章》四次方程：

p1:=-x^4+763200*x^2-40642560000

polysolver(p1);

[[x+240],[x+840],[x-840],[x-240]];

• 秦九韶 《数书九章》十次方程：

p1:=x^10+15*x^8+72*x^6-864*x^4-11664*x^2-34992;

wsolve([p1],[x]);

[[x-3],[$x^4+12x^2+108$},[x+3],[$x^2+6$]]

• 目前最多可解100次方程（高于100次，系统悬挂）

p:=x^100-9999;

矩阵

m:=matrix(3,3,[1,2,3,4,5,6,7,8,9]);

$m= \begin{bmatrix} 1 & 2 & 3 \\ 4 & 5 & 6 \\ 7 & 8 &9 \end{bmatrix}.$

• m + m =

$\begin{bmatrix} 2 & 4 & 8 \\ 8 & 10 & 12 \\ 14& 16 & 18 \end{bmatrix}.$

联立方程

• m:=matrix(3,4,[3,2,1,39,2,3,1,34,1,2,3,26]);

m= $\begin{bmatrix} 3 & 2 &1 & 39 \\ 2 & 3 &1 & 34 \\ 1 & 2 & 3 & 26 \end{bmatrix}.$

lsolve_m(m);

$x[1] = \frac{37}{4}$

$x[2] = \frac{17}{4}$

$x[3] = \frac{11}{4}$

m:=matrix(5,6,[1,2,3,14,5,33,6,17,8,9,10,99,11,212,13,14,15,-36,16,417,28,29,-20,169,21,22,23,24,25,-77]); m= $\begin{bmatrix} 1,2,3,14,5,33\\ 6,17,8,9,10,99\\ 11,212,13,14,15,-36\\ 16,417,28,29,-20,169\\ 21,22,23,24,25,-77 \end{bmatrix}.$

$x[1]=\frac{666761}{6960}$

$x[2]=\frac{229}{580}$

$x[3]=\frac{7589}{87}$

$x[4]=\frac{1884}{145}$

$x[5]=\frac{13865}{1392}$

多元高次方程组

三元二次方程组

朱世杰《四元玉鉴‎》《三才运元》 ：

p1:=x*y*z-x*y^2-z-x-y;

p2:=x*z-x^2-z-y+x;

p3:=z^2-x^2-y^2;

朱世杰得 z=5; 用吴特征列法求解， 令

ps:=[p1,p2,p3]; vs:=[x,y,z];

wsolve(ps,vs); 得一组解， [[x,y+z],[x,y+z,2z^2+1],[x-1,y,z+1],[x-3,y-4,z-5],[x,y,z]]

其中包括 z=5,y=4,x=3; x=1,y=0,z=-1;

roots(ps,vs);

[[y,-z,x,0],[z],[z, - $\tfrac{1}{2}I\sqrt(2)$,y,$\tfrac{1}{2}I\sqrt(2)$,x,0],[],[z,$\tfrac{1}{2}I\sqrt(2)$,y,-$\tfrac{1}{2}I\sqrt(2)$,x,0],[],[z,-1,y,0,x,1],[],[z,5,y,4,x,3],[],[z,0,y,0,x,0],[]]

四元二次方程式

朱世杰《四元玉鉴》《四象会元》四元二次方程式

$0=-2*y+x+z$;

$0=-y^2*x+4*y+2*x-x^2+4*z+x*z$;

$0=x^2+y^2-z^2$;

$0=2*y-w+2*x$;

朱世杰的解 w=14;

用吴特征列法解之：

$p1:=-2*y+x+z$;

$p2:=-y^2*x+4*y+2*x-x^2+4*z+x*z$;

$p3:=x^2+y^2-z^2$;

$p4:=2*y-w+2*x$;

$ps:=[p1,p2,p3,p4]$;

$vs:=[x,y,z,w]$;

$wsolve(ps,vs)$;

四元二次方程式的解

MMP 的解为

w=$\frac{-49}{4}$;

w=14;

w=0;

w=-2;

显然包括 w=14，如图所示。

几何自动推理

三角形中线与一边平行

wprove([ [ [POINT,A,B,C], [MIDPOINT,F,A,B], [INTER,G,[LINE,A,C],[PLINE,F,B,C]] ], [ [MIDPOINT,G,A,C] ] ]);

The geometric statement is valid!

wprove([ [ [POINT,A,B,C], [MIDPOINT,F,A,B], [MIDPOINT,G,A,C] ], [[INTER,G,[LINE,A,C],[PLINE,F,B,C]] ]]);

The geometric statement is valid!

三角形面积=底高积之半

wderive([[d,k],[], [A,[d,H],B,[0,0],C,[L,0]], [ [area,k,A,B,C]],[],[]]);

Formulas 1

2k-LH

梯形面积=(底边+顶边) X高 /2

wderive( [[k],[L,H,c,d], [A,[0,0], B,[L,0], C, [c,H],D,[d,H]], [ [area, k, A,B,C,D]],[],[]]);

-2k+HL+cH-dH 1 formulas found

任意多边形面积

多边形A,B,C,D,E,F 坐标：A,[a1,a2],B,[b1,b2],C,[c1,c2],D,[d1,d2],E,[e1,e2],F,[f1,f2]

wderive( [[k],[a1,a2,b1,b2,c1,c2,d1,d2,e1,e2,f1,f2], [A,[a1,a2], B,[b1,b2], C, [c1,c2],D,[d1,d2],E,[e1,e2],F,[f1,f2]], [ [area, k, A,B,C,D,E,F]],[],[]]);

2k-c2b1+a2b1-d2c1+b2c1-b2a1+f2a1+c2d1-e2d1+e1d2-f2e1+f1e2-a2f1 1 formulas found.

五边形面积为三个三角形面积之和

wderive( [[a1,a2,b1,b2,c1,c2,d1,d2,e1,e2,k],[], [A,[a1,a2], B,[b1,b2], C, [c1,c2],D,[d1,d2],E,[e1,e2]], [ [area,J1,A,B,C], [area,J4,C,D,A], [area,J5,D,E,A], [area, k, A,B,C,D,E]],[],[]]);

k-J1-J4-J5

三角形中线

A，B，C，三点； D 为直线BC的中点， E 为 AC 的中点， F 为 AB 的 中点

直线DA与 直线 EB 相交于 G 点， 证明 F，C，G 三点在一条直线上

wprove([[[POINT,A,B,C], [MIDPOINT,D,B,C], [MIDPOINT,E,A,C], [MIDPOINT,F,A,B], [INTER,G,[LINE,D,A],[LINE,E,B]]], COLL,F,C,G]);

The geometric statement is valid !

自动推导秦九韶三斜求积公式

自动推导秦九韶三斜求积

有三点 a1,b1,c1 a1c1 的长度为 b a1b1的长度为c b1c1的长度为a 三角形面积为k

wderive( [[x2,x1,x3,k],[a,b,c], [b1,[0,0], c1,[x3,0], a1, [x1,x2]], [[dis, a1, c1, b], [dis, a1, b1, c],[dis,b1,c1,a], [area, k, a1, b1, c1]],[],[]]);

自动得到： $16k^2=2(a^2b^2+a^2C^2+b^2C^2)-(a^4+b^4+c^4)$

证明秦九韶三角形面积公式与海伦公式等效

s:=$\frac{a+b+c}{2}$

$16A^2$=expand(s*(s-a)*(s-b)*(s-c)*16);

得到 $16*A^2=2(a^2b^2+b^2c^2+a^2c^2)-(a^4+b^4+c^4)$

编写程序

刘徽割圆术

f:=proc(n) local g,p; g:=nsqrt(3.); p:=6; for i from 1 to n do g:=nsqrt(2+g); p:=p*2; od;

g:=nsqrt(2-g); g:=p*g; return(g); end:

f(25); 3.14159265358979320658867831072

参考文献

• 吴文俊著 《数学机械化》 科学出版社 ISBN 7-03-010765-0 380页
• 高小山等著 《方程求解与机器证明:基于MMP的问题求解》 ISBN 978-7-03-017862-6 278页
• 数学机械化自动推理平台
• MMP 用户手册
• Xiao-Shan Gao, Dongming Wang ed, Mathematics Mechanization and Applications ISBN 0-12-734760-7 551页