作者allenlinli (allen)
看板Programming
標題[問題] 可以做"數學自動證明"的程式語言?
時間Tue Mar 27 13:55:42 2012
請問哪種程式語言可以做到"數學的自動證明"嗎?
像做到以下的事
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
)或甚至進一步數學運算的程式語言
請問有沒有人有用過可自動證明的程式語言?
謝謝
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 60.245.65.164
1F：→ MOONRAKER:機械證明的「行話」是LISP。 118.163.12.174 03/27 14:54
2F：推 yauhh:做證明的,Coq,Agda,任選一個吧 61.231.71.233 03/27 19:32
3F：→ yauhh:可是講到"自動"證明嘛...... 61.231.71.233 03/27 19:33