文章/答案/技术大牛

发布

社区首页 >问答首页 >自动定理证明

问自动定理证明
EN

Stack Overflow用户

提问于 2013-06-25 22:27:52

回答 3查看 928关注 0票数 3

我正在寻找一个自动定理证明系统，它可以证明这一点：

鳄鱼夺走了人类的孩子。男人叫鳄鱼不要吃他的孩子。但是鳄鱼说:我会把你的孩子还给你，如果你告诉我，我该拿他怎么办。

his的解析解决方案如下所示：

X-鳄鱼会吃小孩y- men回答:鳄鱼会吃小孩

~意味着平等，！表示not，->暗示，+ OR；

((x~y)->!x) and  ((x XOR y)->x) =
(x! and y +!x and y+!x)(!x!y+x and y+x) =
(!x+!y)(x+!y) = !y;

所以，答案是，男人必须说：“你不会吃了孩子”；

现在，这里列出了大量的系统：http://en.wikipedia.org/wiki/Automated_theorem_proving

我试过其中的5-6个，但我真的不明白我在这里做什么。如何在它们内部形式化这个定理，这样我就可以进入它的第一部分：

((x~y)->!x) and ((x XOR y)->x)

并得到答案

y作为输出。

哪一个系统至少能自动地给我一些建议，并给我一些提示？

你好，康斯坦丁。

prolog

theorem-proving

回答 3

Stack Overflow用户

回答已采纳

发布于 2013-07-13 20:59:53

经过大量的研究，我发现像这样的程序还有很多，所以我的回答是:是的，这样的定理可以自动证明。在线示例：http://logik.phl.univie.ac.at/~chris/gateway/formular-uk-zentral.html

票数 1

Stack Overflow用户

发布于 2013-06-26 01:36:10

嗯，你的问题目标比平时高了很多，我不太理解你的任务来帮助……

我只是浏览了一下“tableaux in Prolog”，建议先试试simpler one，然后再深入研究something more sophisticated (但我甚至不知道这种逻辑是否适合你的任务)。

票数 1

Stack Overflow用户

发布于 2013-06-25 22:31:54

检出prolog。它对逻辑命题和诸如此类的东西很有用。从通读维基开始，看看它听起来是不是你想要的。它是一种逻辑编程语言-它将帮助您构建自己的定理证明算法。

维基：http://en.wikipedia.org/wiki/Prolog

教程：http://cs.union.edu/~striegnk/courses/esslli04prolog/index.php

票数 0

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/17300046

复制

相似问题

问自动定理证明
EN

回答 3

Stack Overflow用户

Stack Overflow用户

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问自动定理证明EN

回答 3

Stack Overflow用户

Stack Overflow用户

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问自动定理证明
EN