作者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