数学机械化自动推理平台

维基百科,自由的百科全书
跳转至: 导航搜索
数学机械化自动推理平台
原作者 中国科学院数学机械化重点实验室
開發者 中國
国家基础研究发展规划项目
"数学机械化与自动推理平台"
软件开发课题组
穩定版本 3.0 / 2006年4月1日(8年前) (2006-04-01)
網站 MMP - 数学机械化自动推理平台

数学机械化自动推理平台英语Mathematics Mechanization and Automated Reasoning Platform),又名 Mathematics-Mechanization Platform(简称 MMP,开发代号:elimino)是中国科学院数学机械化重点实验室根据吴文俊院士数学机械化理论为基础发展出来的数学机械化自动推理平台。2006年的版本为 3.0,此后停顿,再无新版本。

运行环境[编辑]

微软Windows 2000, XP, Vista.

核心功能[编辑]

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

数系[编辑]

Sqrt.jpg

整数任意大。小数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}

多元高次方程组[编辑]

三元二次方程组[编辑]

朱世杰《四元玉鉴‎》《三才运元》[1]

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],[]]

四元二次方程式[编辑]

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


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

三角形中线
Automatic geometric proof.jpg

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

参考文献[编辑]

  1. ^ 吴文俊 《数学机械化》 《朱世杰的一个例子》 第18-19页 科学出版社ISBN 7-03-010764-0
  2. ^ 朱世杰原著 李兆华校正 《四元玉鉴》 153页 ISBN 978-7-03-020112-6