作者Favonia (小西风最乖了*^^*)
站内Programming
标题Re: [问题] 可以做"数学自动证明"的程式语言?
时间Sun Apr 1 03:57:15 2012
※ 引述《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)
1F:推 yoco315:好文,那我也给一个关键字好了 XD182.235.170.158 04/01 17:39
2F:→ yoco315:GPS: general problem solver182.235.170.158 04/01 17:39
3F:→ yauhh:给的这个词不太好,很恐怖 59.112.225.30 04/01 17:57