※ 引述《allenlinli (allen)》之铭言： : 请问哪种程式语言可以做到"数学的自动证明"吗? : 像做到以下的事 : 1. 6x>5x , if x>0 : 2. 5x+6y=a+2b , given a=5x, b=3y : 3. if a>b, then a+c>b+c : 因为我要做一段数学证明，它的证明的逻辑(或说原则)都 : 一样，因此照理说应该可以用程式自动证明才对。除了用C : 硬将数学规则写去之外，希望可以有本身有推里(如prolog : )或甚至进一步数学运算的程式语言 : 请问有没有人有用过可自动证明的程式语言? : 谢谢 如果有自动证明工具,其中比较吸引人的特色可能是 读入一段证明,它可以指出证明中存在一些矛盾或谬误. 不过我用Prolog写个证明,觉得证明这种东西是定义游戏, 首先根据你的定义,所以你可以讲什麽故事; 然後在讲故事过程中, 才来讨论证明句有没有写错. 而你自己写的证明,如何证明自己所写的证明句子没有错误? 至於 6x>5x, if x>0 这句,我想Prolog证明写起来,应该是先把Peano公设走一次: nat(zero). nat(succ(N)) :- nat(N). eq(zero, zero). eq(succ(M), succ(N)) :- eq(M, N). 然後照这样的感觉, 6x>5x, if x>0: gt1(succ(_), zero) :- !. gt1(succ(M), succ(N)) :- gt1(M, N). gt(x(succ(_),X), x(zero,X)) :- gt1(X, _). gt(x(succ(M),X), x(succ(N),X)) :- gt(x(M,X), x(N,X)). 然後询问句这样子写: ?- gt(x(succ(succ(succ(succ(succ(succ(zero)))))), X), x(succ(succ(succ(succ(succ(zero))))), X)). X = succ(_G376); false. 我想这就是得证. --

※ 发信站: 批踢踢实业坊(ptt.cc) ◆ From: 61.231.71.233