※ 引述《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