※ 引述《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)