咋用程序做数学证明题
定理自动证明的程序很多，比如Otter：Otter 3.3 / Mace 2.2 Packages，它曾经证明过Robbins猜想。Otter主要实现等式归结，可以用于证明群伦、布尔代数等代数结构中的一介等式谓词。例如：证明Robbins猜想的代码为：set(auto).list(usable).x = x.x+y = y+x.(x+y)+z = x+y+z.n(n(x+y)+n(x+n(y))) = x. % Robbins axiomx+C = C. % hypothesis---exists a 1n(A+n(B))+n(n(A)+n(B)) != B. % denial of Huntington axiomend_of_list.得到的证明为：---------------- PROOF ----------------1 n(A+n(B))+n(n(A)+n(B))!=B.2 x=x.3 x+y=y+x.4 (x+y)+z=x+y+z.6 n(n(x+y)+n(x+n(y)))=x.9,8 x+C=C.11,10 C+x=C.13 n(A+n(B))+n(n(B)+n(A))!=B.18 n(n(C)+n(C))=C.20 n(n(C)+n(x+n(C)))=x.36 n(n(x+n(C)+n(C))+n(C))=x.62 n(n(C)+n(n(C)+x))=x.64 n(n(x+n(C))+n(C))=x.88 n(n(C)+x)=n(x+n(C)).89 n(n(n(C)+x)+n(C))=x.91 n(x+n(C))=n(n(C)+x).98 n(n(B)+A)+n(n(B)+n(A))!=B.100,99 n(n(x+y+n(C))+n(C))=x+y.102,101 x+n(C)=x.106,105 n(n(C)+x)=n(x).108,107 n(n(x))=x.120,119 n(x+y)+n(x+n(y))=n(x).121 B!=B.122 $F.------------ end of proof -------------
■网友
如何应用_Mathematica_证明几何定理
对于几何题，先代数化（建系法，三角法，复数法等）例1
【咋用程序做数学证明题】 
推荐阅读
- 招聘都要学历，何来程序员不看学历
- 银行系统的研发岗(程序员)是不是很难进(校招)推广到国企的研发岗(程序员)呢
- 坐标合肥，请问在哪里能捕捉到程序员这种生物他们大都出现在哪里呢
- 程序猿和产品汪能愉快的一起谈恋爱嘛
- 怎样成为一名合格的Python程序员?
- 我是程序猿养了条狗，取啥名字好
- 送程序员男友苹果无线耳机还是专业品牌耳机
- 女程序媛怎样追求男程序员
- 阿里程序员网上招人的情况为何如此多见
- 朋友圈权限被破解，怎样反破解