Re: [問題] 可以做"數學自動證明"的程式語言?
※ 引述《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
推
03/28 10:43, , 1F
03/28 10:43, 1F
討論串 (同標題文章)
本文引述了以下文章的的內容：
完整討論串 (本文為第 2 之 4 篇)：
Programming 近期熱門文章
PTT數位生活區 即時熱門文章
