Re: [問題] 可以做"數學自動證明"的程式語言?

看板Programming作者Favonia (小西風最乖了*^^*)時間13年前 (2012/04/01 03:57)推噓1(1推 0噓 2→)

留言3則, 2人參與討論串4/4 (看更多)

※ 引述《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 : )或甚至進一步數學運算的程式語言 : 請問有沒有人有用過可自動證明的程式語言? : 謝謝我摸過 Twelf, Agda, Coq 等等所以應該能夠回答你的問題 xD 一般來說全自動證明是不可能的，只能退而求其次，請你不時引導一下系統，然後確定沒問題後才讓你過關。也許有點出乎你意料之外，很多有趣的形式系統光是要寫出正確的檢查程式就非常非常難，如果用 C 這麼囉唆的語言寫可謂自討苦吃。好消息有兩個，第一個是很多簡單的形式系統都可以自動證明沒問題；像你上面只有加法和不等式，如果是整數，沒記錯的話有演算法可以判定（因為自動機可以算加法... er 我覺得我沒辦法在這篇文章介紹），而實數根據 Tarski 定理應該可以判定；如果只有用加法可能有更簡單的版本。至於我上面提的演算法現在誰有實作，或是最好的實作有多快我就不清楚了。第二個好消息就是這種軟體到處都是，關鍵字是「theorem prover」和「proof assistant」。你可能要先問自己，你需要多強的形式系統？要有整數嗎？要可以定義亂七八糟的資料（像二元樹）嗎？需要超過一階邏輯嗎？為了要能回答這些問題（加上善用這些工具），我個人覺得讀一點邏輯和型態理論（type theory）可能有一點幫助。希望有回答到你的問題 xD -- ※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 140.112.30.39 ※ 編輯: Favonia 來自: 140.112.30.39 (04/01 04:00)